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