unendlich - Home About Archive

Type kindness

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:

data Maybe a = Nothing | Just a
data Either a b = Left a | Right b

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
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
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.

First-class types

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)

  1. Unless some compiler-specific language extensions are used, such as DataKinds.

  2. Here we see how the function syntax was reused to talk about type kinds.