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