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

Solution 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.

Solution 2:

Firstly, the ?? -> ? -> * kind is a GHC-specific extension. The ? and ?? are just there to deal with unboxed types, which behave differently from just * (which has to be boxed, as far as I know). So ?? can be any normal type or an unboxed type (e.g. Int#); ? can be either of those or an unboxed tuple. There is more information here: Haskell Weird Kinds: Kind of (->) is ?? -> ? -> *

I think a function can't return an unboxed type because functions are lazy. Since a lazy value is either a value or a thunk, it has to be boxed. Boxed just means it is a pointer rather than just a value: it's like Integer() vs int in Java.

Since you are probably not going to be using unboxed types in LYAH-level code, you can imagine that the kind of -> is just * -> * -> *.

Since the ? and ?? are basically just more general version of *, they do not have anything to do with sorts or anything like that.

However, since -> is just a type constructor, you can actually partially apply it; for example, (->) e is an instance of Functor and Monad. Figuring out how to write these instances is a good mind-stretching exercise.

As far as value constructors go, they would have to just be lambdas (\ x ->) or function declarations. Since functions are so fundamental to the language, they get their own syntax.