Playing with types in Haskell (Part 3)

Types of Types

We’ve seen, at an observer level, how Haskell deals with types and type classes. But how does it actually formalize that so that it can get the checking right? While values have types (and expressions generate values), and we can use types to guarantee that functions which expect a type gets exactly that type. How then does Haskell guarantee that type constructors get the type it expects? The answer is elegant and beautiful – Haskell gives types, types. That means that each type, has a meta-type, and it’s called a “kind”.

:k StringString ==> StringString :: *
:k StringAnything ==> StringString :: * -> *

What this means is that StringString is going to return a concrete type all on its own (remember that constructors with no type variables create concrete types directly). StringAnything, on the other hand, is a type constructor that takes a concrete type and returns a concrete type. That means that plain old StringAnything is not a concrete type (again, similar to what we discussed earlier). Similarly, Maybe is a type constructor that takes a concrete type to produce a concrete type, and Maybe itself is not a concrete type.

We’re used to seeing functions as follows:

myFunction1 :: Int -> Bool

And also functions that take type variables that represent a concrete type

myFunction2 :: a -> Bool        (usually with class constraints added)
myFunction3 :: a -> b           (usually with class constraints added)

What if we have a function that takes a type constructor?

myFunction4 :: c a -> Bool
myFunction4 x = False

Look at this function. It takes one parameter, of type c a. Not just a, but c a. It’s obvious that c is being used as a type constructor, and in fact, it takes exactly one concrete type, a. An example for c would be Maybe. And we could apply myFunction4 as follows:

myFunction4 (Just 4)      ==> False
:t myFunction4            ==> c a -> Bool
:t myFunction4 (Just 4)   ==> Bool

What’s the kind of a and c then? We know that (c a) must produce a concrete type, because function parameters have to take a concrete type, not some airy-fairy type. Hence:

(c a) :: *

We also know that c is a type constructor that takes one concrete type, hence this follows:

c :: * -> *
a :: *

Let’s try one more:

myFunction5 :: d c a -> Bool
myFunction5 x = False

Can you derive the following?

Since      (d c a) :: *
and        a :: *

Therefore  c :: * -> *
and        d :: (* -> *) -> * -> *

Well, that’s my summary of Haskell types.