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