What are some examples of type-level programming?

Question

I do not understand what "type-level programming" means, nor can I find a suitable explanation using Google.

Could someone please provide an example that demonstrates type-level programming? Explanations and/or definitions of the paradigm would be useful and appreciated.

Answer 1

You're already familiar with "value-level" programming, whereby you manipulate values such as42 :: Int or 'a' :: Char. In languages like Haskell, Scala, and many others, type-level programming allows you to manipulate types like Int :: * or Char :: * where * is the kind of a concrete type (Maybe a or [a] are concrete types, but not Maybe or [] which have kind * -> *).

Consider this function

foo :: Char -> Int
foo x = fromEnum x

Here foo takes a value of type Char and returns a new value of type Int using the Enum instance for Char. This function manipulates values.

Now compare foo to this type family, enabled with the TypeFamilies language extension.

type family Foo (x :: *)
type instance Foo Char = Int

Here Foo takes a type of kind * and returns a new type of kind * using the simple mapping Char -> Int. This is a type level function that manipulates types.

This is a very simple example and you might wonder how this could possibly be useful. Using more powerful language tools, we can begin to encode proofs of the correctness of our code at the type level (for more on this, see the Curry-Howard correspondence).

A practical example is a red-black tree that uses type level programming to statically guarantee that the invariants of the tree hold.

A red-black tree has the following simple properties:

1. A node is either red or black.
2. The root is black.
3. All leaves are black. (All leaves are same colour as the root.)
4. Every red node must have two black child nodes. Every path from a given node to any of its descendant leaves contains the same number of black nodes.

We'll use DataKinds and GADTs, a very powerful type level programming combination.

{-# LANGUAGE DataKinds, GADTS, KindSignatures #-}

import GHC.TypeLits

First, some types to represent the colours.

data Colour = Red | Black -- promoted to types via DataKinds

this defines a new kind Colour inhabited by two types: Red and Black. Note that there are no values (ignoring bottoms) inhabiting these types, but we aren't going to need them anyways.

The red-black tree nodes are represented by the following GADT

-- 'c' is the Colour of the node, either Red or Black
-- 'n' is the number of black child nodes, a type level Natural number
-- 'a' is the type of the values this node contains
data Node (c :: Colour) (n :: Nat) a where
    -- all leaves are black
    Leaf :: Node Black 1 a
    -- black nodes can have children of either colour
    B    :: Node l     n a -> a -> Node r     n a -> Node Black (n + 1) a
    -- red nodes can only have black children
    R    :: Node Black n a -> a -> Node Black n a -> Node Red n a

GADT lets us express the Colour of the R and B constructors directly in the types.

The root of the tree looks like this

data RedBlackTree a where
    RBTree :: Node Black n a -> RedBlackTree a

Now it is impossible to create a well-typed RedBlackTree that violates any of the 4 properties mentioned above.

1. The first constraint is obviously true, there are only 2 types inhabiting Colour.
2. From the definition of RedBlackTree the root is black.
3. From the definition of the Leaf constructor, all leaves are black.
4. From the definition of the R constructor, both it's children must be Black nodes. As well, the number of black child nodes of each subtree are equal (the same n is used in the type of both left and right subtrees)

All these conditions are checked at compile time by GHC, meaning that we will never get a runtime exception from some misbehaving code invalidating our assumptions about a red-black tree. Importantly, there is no runtime cost associated with these extra benefits, all the work is done at compile time.

Answer 2

In most statically typed languages you have two "domains" the value-level and the type-level (some languages have even more). Type-level programming involves encoding logic ( often function abstraction ) in the type-system which is evaluated at compile-time. Some examples would be template metaprogramming or Haskell type-families.

A few languages extensions are needed to do this example in Haskell but you kind of ignore them for now and just look at the type-family as being a function but over type-level numbers (Nat).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

-- value-level
odd :: Integer -> Bool
odd 0 = False
odd 1 = True
odd n = odd (n-2)

-- type-level
type family Odd (n :: Nat) :: Bool where
    Odd 0 = False
    Odd 1 = True
    Odd n = Odd (n - 2)

test1 = Proxy :: Proxy (Odd 10)
test2 = Proxy :: Proxy (Odd 11)

Here instead of testing whether a natural number value is an odd number, we're testing whether a natural number type is an odd number and reducing it to a type-level Boolean at compile-time. If you evaluate this program the types of test1 and test2 are computed at compile-time to:

λ: :type test1
test1 :: Proxy 'False
λ: :type test2
test2 :: Proxy 'True

That's the essence of type-level programming, depending on the language you may be able to encode complex logic at the type-level which have a variety of uses. For example to restrict certain behavior at the value-level, manage resource finalization, or store more information about data-structures.

Answer 3

The other answers are very nice, but I want to emphasize one point. Our programming language theory of terms is based strongly on the Lambda Calculus. A "pure" Lisp corresponds (more or less) to a heavily-sugared untyped Lambda Calculus. The meaning of programs is defined by the evaluation rules that say how the Lambda Calculus terms are reduced as the program runs.

In a typed language, we assign types to terms. For every evaluation rule, we have a corresponding type rule that shows how the types are preserved by evaluation. Depending on the type system, there are also other rules defining how types relate to one another. It turns out that once you get a sufficiently interesting type system, the types and their system of rules also correspond to a variant of the Lambda Calculus!

Although it's common to think of Lambda Calculus as a programming language now, it was originally designed as a system of logic. This is why it is useful for reasoning about the types of terms in a programming language. But the programming language aspect of Lambda Calculus allows one to write programs that are evaluated by the type checker.

Hopefully you can see now that "type-level programming" is not a substantially different thing than "term-level programming", it's just that it's not very common now to have a language in a type system that's powerful enough that you'd have a reason to write programs in it.