In Haskell, there are "higher type" types * really *? Or do they just mean collections of * specific * types and nothing more?

Question

Paramametically polymorphic functions

Consider the following function:

f :: a -> Int fx = (1 :: Int) 

We can say that type f is equal to a -> Int , and therefore f is of type "higher grade".

Which of the following is the most accurate way to think about f ?

• In fact, there is a single f type a -> Int . It can be used, however, as f :: Int -> Int , as f :: Double -> Int , etc.

• Literally, type f NOT a -> Int . Indeed, this is just a shorthand way of saying that there exists a family of functions f whose type is specific (i.e., There is f :: Int -> Int , an f :: Double -> Double , etc., Moreover, each of these functions are different from each other).

Higher types

Similarly, we can consider the following type declaration:

 data Maybe a = Just a | Nothing 

And ask which of the two views is more correct:

• There are no types of Maybe ; indeed, there is only a family of specific types ( Maybe Int , Maybe String , etc.) and nothing more.

• Actually there is one type Maybe . This type is taller. When we say that it is a “type”, we mean it literally (not as a shorthand for (1)). It so happened that we can also write Maybe Int , Maybe Double , etc., to generate different types (which are specific). But at the end of the day (i.e.): Maybe , Maybe Int and Maybe String denote three different types, two of which are specific, and one of which is higher.

Question Summary

In Haskell, are types of a higher type really? Or only concrete types are "real types", and when we talk about "types of a higher genus," we simply denote a family of specific types. Moreover, do paramametically polymorphic functions denote functions of the same type or simply denote functions of collecting specific types (and nothing more)?

Answer 1

It is not entirely clear what you want to ask, and what is the practical difference between 1 and 2 in both cases, but from a basic mathematical perspective:

Paramametically polymorphic functions

f is of type f :: forall aa->int

This is a completely legal type for a function in a typed lambda calculus based on Haskell. It could be something like:

 f = λa:Type.λx:a.(body for f) 

How do you get Double->Int from it? You apply it to a Double type:

 f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double) 

Haskell performs both operations (type of abstraction and type of application) behind the scene, although you can explicitly specify the forall part in the type signature with the XExplicitForAll GHC extension and explicitly create an instance of Double->Int f with the type signature:

 f_double :: Double -> Int f_double = f 

Higher types

Consider a simple type:

 data Example = IntVal Int | NoVal 

(Yes, it’s Maybe Int ).

Maybe is a type constructor, just as IntVal is a data constructor. This is exactly the same, only "one level up" in the sense that Maybe applies to Type , just as IntVal applies to Int .

In the lambda calculus, Maybe is of type:

 Maybe : Type->Type 

Haskell does not allow you to get a type from a type constructor, but it does allow you to get a view (which is just a fancy name for a type of type):

 :k Maybe Maybe :: * -> * 

No, Maybe not a type: you cannot have an object of type Maybe . Maybe is a (almost) function from types to types, for example IntVal is a function from values ​​to values.

We call the result of applying Maybe to String as Maybe String , as we call the result of applying IntVal to 4 as IntVal 4 .

Answer 2

First, the question arises: does the statement “all lists have length” have one operator or a series of operators “list1 has length”, “list2 has length”, ...?

If you specify type f with explicit forall , you get f :: forall a. a -> Int f :: forall a. a -> Int . First of all, it is not "high ranking". At GHCI, we can do the following:

 λ> :set -XRankNTypes λ> :k (forall a. a -> Int) (forall a. a -> Int) :: * 

So f has the form * .

Now, in Haskell, we can use ~ for type equality. We can set the following to check the material in GHCI:

 λ> :set -XImpredicativeTypes λ> :set -XTypeFamilies λ> :t undefined :: ((~) Int Int) => a undefined :: ((~) Int Int) => a :: a 

This shows that the GHC has figured out type equality for this example. Type inequality will give the following error:

 λ> undefined :: ((~) (Int -> Int) (Int)) => a <interactive>:22:1: Couldn't match expected type 'Int' with actual type 'Int -> Int' In the expression: undefined :: ((~) (Int -> Int) (Int)) => a In an equation for 'it': it = undefined :: ((~) (Int -> Int) (Int)) => a 

Now using this method directly will not allow us to compare the type f , but I found a small option that should work for our purposes:

 λ> :t undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a :: Int 

In other words, if f equivalent to the type g :: Int -> Int , then a must be Int. This is similar to x = y , y = 0 , so x = 0 . We do not have x = 0 , until we specify y = 0 , until we just have x = y .

Maybe different in that it has the following form:

 λ> :k Maybe Maybe :: * -> * 

Since we use DataKinds , we have :k (~) :: k -> k -> GHC.Prim.Constraint , so we can do things like:

 λ> :t undefined :: (~) Maybe Maybe => Int undefined :: (~) Maybe Maybe => Int :: Int λ> :k Either () Either () :: * -> * λ> :t undefined :: (~) Maybe (Either ()) => Int Couldn't match expected type 'Either ()' with actual type 'Maybe' 

To summarize, f :: forall a. a -> Int f :: forall a. a -> Int has the same meaning as the statement "if you give me something, I will give you Int." Could you translate the expression into a bunch of sayings "if you give me a dog ...", "if you give me a penny ..."? Yes, but it weakens the statement. In the end, decide exactly what you mean by “the same,” and get an answer.