Functions don't just have types: They ARE Types. And Kinds. And Sorts. Help put a blown mind back together

Question

I was doing my usual "Read a chapter of LYAH before bed" routine, feeling like my brain was expanding with every code sample. At this point I was convinced that I understood the core awesomeness of Haskell, and now just had to understand the standard libraries and type classes so that I could start writing real software.

So I was reading the chapter about applicative functors when all of a sudden the book claimed that functions don't merely have types, they are types, and can be treated as such (For example, by making them instances of type classes). (->) is a type constructor like any other.

My mind was blown yet again, and I immediately jumped out of bed, booted up the computer, went to GHCi and discovered the following:

Prelude> :k (->) (->) :: ?? -> ? -> * 

• What on earth does it mean?
• If (->) is a type constructor, what are the value constructors? I can take a guess, but would have no idea how define it in traditional data (->) ... = ... | ... | ... format. It's easy enough to do this with any other type constructor: data Either a b = Left a | Right b. I suspect my inability to express it in this form is related to the extremly weird type signature.
• What have I just stumbled upon? Higher kinded types have kind signatures like * -> * -> *. Come to think of it... (->) appears in kind signatures too! Does this mean that not only is it a type constructor, but also a kind constructor? Is this related to the question marks in the type signature?

I have read somewhere (wish I could find it again, Google fails me) about being able to extend type systems arbitrarily by going from Values, to Types of Values, to Kinds of Types, to Sorts of Kinds, to something else of Sorts, to something else of something elses, and so on forever. Is this reflected in the kind signature for (->)? Because I've also run into the notion of the Lambda cube and the calculus of constructions without taking the time to really investigate them, and if I remember correctly it is possible to define functions that take types and return types, take values and return values, take types and return values, and take values which return types.

If I had to take a guess at the type signature for a function which takes a value and returns a type, I would probably express it like this:

a -> ? 

or possibly

a -> * 

Although I see no fundamental immutable reason why the second example couldn't easily be interpreted as a function from a value of type a to a value of type *, where * is just a type synonym for string or something.

The first example better expresses a function whose type transcends a type signature in my mind: "a function which takes a value of type a and returns something which cannot be expressed as a type."

Answer 1

You touch so many interesting points in your question, so I am afraid this is going to be a long answer :)

Kind of (->)

The kind of (->) is * -> * -> *, if we disregard the boxity GHC inserts. But there is no circularity going on, the ->s in the kind of (->) are kind arrows, not function arrows. Indeed, to distinguish them kind arrows could be written as (=>), and then the kind of (->) is * => * => *.

We can regard (->) as a type constructor, or maybe rather a type operator. Similarly, (=>) could be seen as a kind operator, and as you suggest in your question we need to go one 'level' up. We return to this later in the section Beyond Kinds, but first:

How the situation looks in a dependently typed language

You ask how the type signature would look for a function that takes a value and returns a type. This is impossible to do in Haskell: functions cannot return types! You can simulate this behaviour using type classes and type families, but let us for illustration change language to the dependently typed language Agda. This is a language with similar syntax as Haskell where juggling types together with values is second nature.

To have something to work with, we define a data type of natural numbers, for convenience in unary representation as in Peano Arithmetic. Data types are written in GADT style:

data Nat : Set where     Zero : Nat     Succ : Nat -> Nat 

Set is equivalent to * in Haskell, the "type" of all (small) types, such as Natural numbers. This tells us that the type of Nat is Set, whereas in Haskell, Nat would not have a type, it would have a kind, namely *. In Agda there are no kinds, but everything has a type.

We can now write a function that takes a value and returns a type. Below is a the function which takes a natural number n and a type, and makes iterates the List constructor n applied to this type. (In Agda, [a] is usually written List a)

listOfLists : Nat -> Set -> Set listOfLists Zero     a = a listOfLists (Succ n) a = List (listOfLists n a) 

Some examples:

listOfLists Zero               Bool = Bool listOfLists (Succ Zero)        Bool = List Bool listOfLists (Succ (Succ Zero)) Bool = List (List Bool) 

We can now make a map function that operates on listsOfLists. We need to take a natural number that is the number of iterations of the list constructor. The base cases are when the number is Zero, then listOfList is just the identity and we apply the function. The other is the empty list, and the empty list is returned. The step case is a bit move involving: we apply mapN to the head of the list, but this has one layer less of nesting, and mapN to the rest of the list.

mapN : {a b : Set} -> (a -> b) -> (n : Nat) ->        listOfLists n a -> listOfLists n b mapN f Zero     x         = f x mapN f (Succ n) []        = [] mapN f (Succ n) (x :: xs) = mapN f n x :: mapN f (Succ n) xs 

In the type of mapN, the Nat argument is named n, so the rest of the type can depend on it. So this is an example of a type that depends on a value.

_{As a side note, there are also two other named variables here, namely the first arguments, a and b, of type Set. Type variables are implicitly universally quantified in Haskell, but here we need to spell them out, and specify their type, namely Set. The brackets are there to make them invisible in the definition, as they are always inferable from the other arguments.}

Set is abstract

You ask what the constructors of (->) are. One thing to point out is that Set (as well as * in Haskell) is abstract: you cannot pattern match on it. So this is illegal Agda:

cheating : Set -> Bool cheating Nat = True cheating _   = False 

Again, you can simulate pattern matching on types constructors in Haskell using type families, one canoical example is given on Brent Yorgey's blog. Can we define -> in the Agda? Since we can return types from functions, we can define an own version of -> as follows:

_=>_ : Set -> Set -> Set a => b = a -> b 

(infix operators are written _=>_ rather than (=>)) This definition has very little content, and is very similar to doing a type synonym in Haskell:

type Fun a b = a -> b 

Beyond kinds: Turtles all the way down

As promised above, everything in Agda has a type, but then the type of _=>_ must have a type! This touches your point about sorts, which is, so to speak, one layer above Set (the kinds). In Agda this is called Set1:

FunType : Set1 FunType = Set -> Set -> Set 

And in fact, there is a whole hierarchy of them! Set is the type of "small" types: data types in haskell. But then we have Set1, Set2, Set3, and so on. Set1 is the type of types which mentions Set. This hierarchy is to avoid inconsistencies such as Girard's paradox.

As noticed in your question, -> is used for types and kinds in Haskell, and the same notation is used for function space at all levels in Agda. This must be regarded as a built in type operator, and the constructors are lambda abstraction (or function definitions). This hierarchy of types is similar to the setting in System F omega, and more information can be found in the later chapters of Pierce's Types and Programming Languages.

Pure type systems

In Agda, types can depend on values, and functions can return types, as illustrated above, and we also had an hierarchy of types. Systematic investigation of different systems of the lambda calculi is investigated in more detail in Pure Type Systems. A good reference is Lambda Calculi with Types by Barendregt, where PTS are introduced on page 96, and many examples on page 99 and onwards. You can also read more about the lambda cube there.