Type Level Programming

At its core, a type is a way of classifying things. We can assign types to our functions and use them to compare a function's declared type and its values.

The Higher Kinds

A value constructor accepts a value and yields a value. So a type constructor accepts a type and yields a type.

data Maybe a
  = Just a
  | Nothing

Above we declare a type Maybe with two data constructors. Just, which accepts a value of type a, and Nothing, which does not accept any values at all.

ghci> :t Just
Just :: a -> Maybe a
ghci> :t Nothing
Nothing :: Maybe a

Just has a function type. This means that any value we give Just becomes a Maybe of that type. Nothing however, can conjure up whatever type it wants, without needing a value at all. This pattern is fairly common, and when we declare a type Nothing :: Maybe a, it really means that Nothing is a value of Maybe a, for any and all types a that you might provide to it.

So, then what is the type of Maybe?

ghci> :t Maybe

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

Does this mean that types don't have types of their own? Sort of. Types have kinds.

ghci> :Kind Maybe
Maybe :: * -> *

What is *? * is is the kind of types which have values. This means that the Kind of Maybe accpets a type that has values. This leads to higher kinded polymorphism.

data HigherKinded f a
  = Bare a
  | Wrapped (f a)

Haskell's kind inference is fairly simple and straightforward. This is because when we declare a type that applies f to a, Haskell knows that f must have the kind * -> * and a type of kind *, and returns a type of kind *. In other terms, this means that this kind accepts two types: the first of which is a function that does not have values itself, but when given a type that does have values, it can have values. The second being a type that has values. Finally, it returns a type that can have ordinary values.

Dynamically Kinded Programming

ghci> data Void
ghci> :kind Void
Void :: *

If we declare a type Void and subsequently check for that type's kind, are we surprised by the result? Void has a kind of *. In the same way that one can productively program at the value level with dynamic types, you can program at the type level with dynamic kinds.

At it's core, that's what * represents.

We can now begin to start encoding our first type level numbers. We'll start with the Peano natural numbers, where numbers are inductively defined as either Zero or the Successor of some natural number.

data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ (Succ (Succ (Succ Zero)))

Data Kinds

{-# LANGUAGE DataKinds #-}

The DataKinds extension allows us to promote data constructors into type constructors, which also promotes their type constructors into kind constructors.

To promote something a level up, we prefex the name with an apostrophe: '

data Nat = Zero | Succ Nat

In plain Haskell, this definition introduces a new type Nat with two value constructors, Zero and Succ. With the DataKinds extension, this also defines a new kind Nat, which exists in a separate namespace. We also get two new types 'Zero, which has the kind Nat, and a type constructor 'Succ, which accepts a type of kind Nat.

ghci> :kind 'Zero
'Zero :: Nat
ghci> :kind 'Succ
'Succ :: Nat -> Nat

GADTs

{-# LANGUAGE GADTs #-}

data Maybe a where
  Just :: a -> Maybe a
  Nothing :: Maybe

Generalized Algebraic Data Types

Above we define a GADT for Maybe. The GADT syntax lists the constructors line-by-line, and instead of providing the fields of the constructor, we provide the type signature of the constructor.'

Video notes: A Practical Introduction to Haskell GADTs

Source: http://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html
Current position in document: Vectors