Posted on 25.07.2017

In a previous article we saw type constructors for ADTs, and how they are not types themselves. These are `Maybe`

and `Either`

in Haskell again:

The previous declaration for `Maybe`

names a type constructor that transforms a given type `a`

into a new type `Maybe a`

, such as `Maybe Integer`

or `Maybe Char`

. We cannot ask the type of `Maybe`

by itself to the Haskell interpreter:

```
$ ghci
Prelude> :type Maybe
<interactive>:1:1: error:
• Data constructor not in scope: Maybe
• Perhaps you meant variable ‘maybe’ (imported from Prelude)
```

The error we get back from the interpreter says that a data constructor named `Maybe`

could not be found. That is because it’s a type constructor instead. But there is a different question we can ask the interpreter, we can ask for its *kind*:

```
Prelude> :kind Maybe
Maybe :: * -> *
```

Type kinds are “types of types” and partition different type constructors that share the same arity into sets, just like types are sets of values. The kind of regular types such as `Integer`

and `Char`

is just `*`

. The kind `*`

is the kind of all types that can have values, and there is not really much more to it^{1}. The kind of the type constructor `Maybe`

, on the other hand, is `* -> *`

^{2} which means that it takes any type of kind `*`

and gives back another type of kind `*`

. Why does this matter? It means that we cannot create the types `Maybe Maybe`

or `Maybe Either`

, because the kinds do not match. Kinds are how the compiler can make sure the application of the type constructors make sense:

```
Prelude> :kind Maybe Maybe
<interactive>:1:7: error:
• Expecting one more argument to ‘Maybe’
Expected a type, but ‘Maybe’ has kind ‘* -> *’
Prelude> :kind Maybe Either
<interactive>:1:7: error:
• Expecting two more arguments to ‘Either’
Expected a type, but ‘Either’ has kind ‘* -> * -> *’
```

Just as it is possible to partially apply a function in Haskell, it is also possible to partially apply a type constructor:

```
Prelude> :kind Either
Either :: * -> * -> *
Prelude> :kind Either Integer
Either Integer :: * -> *
Prelude> :kind Either Integer Char
Either Integer Char :: *
```

This means that `Maybe`

and `Either a`

have the same kind and can be used in type signatures whenever a type constructor of kind `* -> *`

is needed.

The Idris programming language is a language where types are first-class entities and therefore have types themselves. We can ask the Idris interpreter the same questions we asked the Haskell one before:

```
$ idris
Idris> :type Maybe
Maybe : Type -> Type
Idris> :type Either
Either : Type -> Type -> Type
```

As we can see Idris says that `Maybe`

is just a regular function that takes values of type `Type`

and returns other values of type `Type`

(the first type is obviously different than the second one). Therefore type kinds are not needed in Idris, because it only needs to check the function arity:

```
Idris> :type Maybe Either
Type mismatch between
Type -> Type -> Type (Type of Either)
and
Type (Expected type)
```

In Idris, all values of type `Type`

can be used as types in the traditional sense. It adds complexity to the language but it allows for powerful type constructions where the type of some values can depend on other values, instead of depending simply on other types as in Haskell. For instance, we can write a function that takes an `Integer`

or a `Double`

depending on the value of other argument to the function:

```
WantDouble : Bool -> Type
WantDouble False = Integer
WantDouble True = Double
-- the argument `number` will have either `Integer` or `Double` type,
-- depending on the value of `b`
processNumber : (b : Bool) -> WantDouble b -> String
processNumber False number = show (number + 1)
processNumber True number = show (number / 3.78)
```