Thanks to NASA for making this photo available freely on @unsplash

Fun with Typed Type-Level Programming in PureScript

As software engineers, we write programs to compute values at runtime. Sometimes, if there is an available static type system, we use types to check our code at compile time. However, is it possible to write code computing types at compile time? Does it make sense to do that? It turns out to be not only possible but also fun if we have a decent compiler.

There are many excellent introductions for type-level programming out there, e.g., the paper written by Thomas Hallgren and the article written by Brent Yorgey, but few of them are written in PureScript. I use this blog to consolidate what I have learned about type-level programming in PureScript, and I hope this post can help people not coming from Haskell learn it.

In this blog, I first present how to program at type level in PureScript by using multi-parameter type classes. Then, use functional dependencies and kinds to strengthen our code. In the end, I show a few use cases about doing matrix arithmetic without runtime dimension errors.

To learn how to do type-level programming, let’s start with a term-level example. We will see how to move this example to the type level step-by-step later.

Term-level computations

What term-level computations do is computing values at runtime dynamically. For example, if we define natural numbers as:

data Nat = Succ Nat | Zero

To use Nat to create numbers, we nest Zero into Succ:

two :: Nat
two = Succ (Succ Zero)
three :: Nat
three = Succ (Succ (Succ Zero))

We can also define functions to check a number is even or odd:

isEven :: Nat → Boolean
isEven Zero = true
isEven (Succ n) = isOdd n
isOdd :: Nat → Boolean
isOdd Zero = false
isOdd (Succ n) = isEven n

So isOdd and isEven recursively call each other to unwrap nested Succs and determine a number is odd or even when reaching Zero.

Let’s use them to create some term-level computations at runtime in PSCi:

> isEven two
true
> isEven three
false

These computations are relatively straightforward, probably dull. Please stay with me. We are going to lift them to the type level!

Type-level computations

The “values” at the type level are types, so the first thing to do to lift our computations to the type level is to lift values to types.

How do we create new types in PureScript? We use the data keyword:

data Zero
data Succ n

So type-level natural numbers are, unsurprisingly, types. We use Succ n and Zero to create numbers just like how we do in the term level:

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

Notice that Zero and Succ n do not have any value constructor because we do not care about runtime values now.

And type-level booleans can be defined in the same way:

data True
data False

Now we are done with lifting values. The next step is to lift functions.

How do we implement functions at the type level? Multi-parameter type classes provide a way to do that:

class IsEven n b
class IsOdd n b

Type classes, IsEven and IsOdd, are used to relate n and b, which are, as you can guess, placeholders for type-level natural numbers and booleans.

Type-class instances are where we implement type-level functions. Remember what we have at the term level is:

isEven Zero     = true
isEven (Succ n) = isOdd n
isOdd Zero     = false
isOdd (Succ n) = isEven n

which can be defined in the type level as:

instance isEvenZero ::             IsEven Zero True
instance isEvenSucc :: IsOdd n b ⇒ IsEven (Succ n) b
instance isOddZero  ::              IsOdd Zero False
instance isOddSucc  :: IsEven n b ⇒ IsOdd (Succ n) b

We use type constraints, IsOdd n b ⇒ and IsEven n b ⇒, to call another type-level function in a type-level function. What we do here is same as what we do at the term level: pattern matching, unwrapping Succ and determining the result when reaching Zero.

The code above is enough to express all the type-level computations we want. However, to kick off the compiler, we need some term-level help:

undefined :: ∀ a. a
undefined = unsafeCoerce unit

undefined is a value with the type ∀ a. a. We can annotate it with any type, for example: undefined :: String or undefined :: Two. undefined can be used as a bridge to convey types from the term level to the type level.

Let’s use undefined to test our code:

test1 :: True
test1 = undefined :: ∀ b. IsEven Two b => b

We assert that the type of test1 is True and the type of its value undefined is b, which is computed from IsEven Two b. During the compile time, the compiler resolves IsEven Two b and finds b should be True, and the type of test1 is indeed True, so test1 passes the type check.

In contrast, Three is not even, sotest2 cannot get compiled:

test2 :: True
test2 = (undefined :: ∀ b. IsEven Three b => b)

test2 will cause a compile-time error with the following error message:

No type class instance was found for
Main.IsOdd Zero
           True

Now we know the compiler is doing its job. It finds a bug for us!

We will make our type-level computations typed and improve the error message in the next section. Put what we have so far all together:

Now we have built a program which checks a number is even or odd at compile time. Although, the program is loose because type-class instances are open to being defined. If someone writes instance foo :: IsOdd Zero True or instance bar :: IsEven Zero Boolean somewhere, our program will end up with unexpected behavior. Can we improve it? Yes, we can! We can ensure IsEven and IsOdd are used in the way we want by making our type-level program typed.

Type-level computation with types

There are two things we can do to improve our type-level computations:

1. Use functional dependencies to make type classes work like functions.
2. Annotate our type parameters defined in type classes with kinds to make type-level functions typed.

Functional dependencies restrict one-to-many relations

What multi-parameter type classes do is just relating types, so there is nothing to stop one adding a type-class instance like:

instance isOddZero' :: IsOdd Zero True

The problem is that once a natural number is provided, the result should be determined. Given the same input, the program should return the same output. Functional dependencies let us put on this restriction to our type classes:

class IsEven n b | n → b
class IsOdd  n b | n → b

Where | n → b is the syntax of functional dependencies, which tells the compiler that knowing n determines b. With this restriction, we are only able to relate the same input with the same output, just like how functions work.

After adding functional dependencies, if we try to relate Zero to both False and True:

instance isOddZero  :: IsOdd Zero False
instance isOddZero' :: IsOdd Zero True

we will get a compile-time error:

Overlapping type class instances found for
Main.IsOdd Zero
           True

What functional dependencies do is make type classes more like functions, so no wonder the syntax is n → b same as the function syntax. We can view IsEven and IsOdd as type-level functions, which, given an n, return a b.

You may notice that we are still able to put any type into IsEven and IsOdd, e.g., instance bar :: IsEven Zero Boolean. But we are already at the type level, we can not use types to type our type-level functions. What else can we use to solve this problem? We use kinds!

Kinds type types

Kinds are the types of types. All types we have seen so far belong to the Type kind. To introduce new kinds in PureScript, we use the foreign function interface (FFI) syntax despite that we do not use any code outside PureScript.

Here is how we define new kinds:

foreign import kind Nat
foreign import kind Boolean

Nat is the kind for type-level natural numbers, and Boolean is the kind for type-level booleans. We can annotate our types with these new kinds by using FFI as well:

foreign import data Zero :: Nat
foreign import data Succ :: Nat → Nat
foreign import data True  :: Boolean
foreign import data False :: Boolean

So Zero is a Nat type, Succ is a Nat → Nat type and both True and False are Boolean types.

Notice that Nat → Nat means Succ is a unary type constructor. Because it’s a constructor awaiting a Nat type, we can’t apply it with other types anymore. In other words, Succ Int will not get compiled since now. Succ is typed with kinds!

Then, our type classes can be redefined as:

class IsEven (n :: Nat) (b :: Boolean) | n → b
class IsOdd  (n :: Nat) (b :: Boolean) | n → b

With the kind annotations, we can only use IsEven and IsOdd with a Nat type and a Boolean type now. instance bar :: IsEven Zero Boolean is no longer compiled because the type Boolean is a Type type, not a Boolean type.

That is all! We do not need to change the definitions of type-class instances.

Because only Type types can have term-level values, to kick off the compiler, we need some help like undefined. This time we use a phantom type which carries a Boolean type:

data BProxy (b :: Boolean) = BProxy

The type-level BProxy has the kind Boolean → Type. We use it to construct a Type type from a Boolean type.

Let’s play with the type BProxy in PSCi to get more familiar with the idea:

> :k True
Main.Boolean
> :k BProxy True
Type
> :k BProxy False
Type

The term-level BProxy is just a bridge, like undefined. We use it to convey types from the term level to the type level:

> :t BProxy
forall t1. BProxy t1
> :t BProxy :: BProxy True
BProxy True
> :t BProxy :: BProxy False
BProxy False

Finally, we can test our code:

test3 :: BProxy True
test3 = BProxy :: ∀ b. IsEven Two b => BProxy b

test3 passes the type check, because Two is even.

test4 :: BProxy True
test4 = BProxy :: ∀ b. IsEven Three b => BProxy b

test4 does not pass the type check, because Three is not even.

Thanks to the functional dependencies, test4 has a better error message than test2 does:

Could not match type
False
with type
True

Put it all together:

How can type-level natural numbers be useful?

Up to now, you might still wonder how we can benefit from type-level programming. Who needs type-level natural numbers after all? It turns out to be quite useful for matrix arithmetic. Let’s see some examples.

Vector addiction takes two equal-length sequences of numbers and returns a new vector:

[1, 3, -5] + [4, -2, -1] 
  = [5, 1, -6]

Without type-level natural numbers, we might define our type of vectors as:

newtype Vec a = Vec (Array a)

Using Vec to implement add, we need to check the length of two vectors first, in case that we meet two unequal-length vectors:

add :: Vec Int → Vec Int → Except String (Vec Int)
add (Vec xs) (Vec ys) 
  | Array.length xs == Array.length ys 
    = pure <<< Vec $ Array.zipWith (+) xs ys
  | otherwise = throwError "Vector lengths must match."

If Array.length xs == Array.length ys is false, we will throw an error, and the consumers of add will need to handle this error.

On the contrary, if we encode the length into Vec by using Nat:

newtype Vec (n :: Nat) a = Vec (Array a)

We can ensure that add is used with equal-length vectors only:

add :: ∀ n. Vec n Int → Vec n Int → Vec n Int
add (Vec xs) (Vec ys) = Vec $ Array.zipWith (+) xs ys

The compiler catches all unequal-length errors for us during compile time, so no one needs to handle runtime errors.

However, if we export the value constructor Vec, anyone can create vectors with false lengths:

falseLengthVector :: Vec Zero Int
falseLengthVector = Vec [1, 2, 3]

To prevent this behavior, we can export only functions which construct Vec in the way we want. Here is an example:

class Add (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c
instance addZero :: Add Zero b b
instance addSucc :: Add a b c ⇒ Add (Succ a) b (Succ c)
cons :: ∀ a b c. Add a One b ⇒ c → Vec a c → Vec b c
cons x (Vec xs) = Vec (Array.cons x xs)
infixr 6 cons as +>
empty :: ∀ a. Vec Zero a
empty = Vec []

Where the Add type class serves as a type-level function adding two Nats. cons is the function we want to export, which is a function prepending an element to a vector. Add a One b ⇒ means b = a + 1, which ensures the length of returned vector is increased by 1. empty is just an empty vector defined for our convenience.

If we export cons but do not export the value constructor Vec from our module, then the module consumers are restricted to use cons to create a vector. Now we ensures no false-length vector is created! Let’s see how it works:

test7 = add (1+>3+>(-5)+>empty) (4+>(-2)+>(-1)+>empty)

test7 passes the type check as expected, but

test8 = add empty (4+>(-2)+>(-1)+>empty)

test8 lets the compiler complains about the unmatched lengths.

Here is another use case using the Add type class:

concat :: ∀ x y z a. Add x y z => Vec x a → Vec y a → Vec z a

By using Add x y z =>, we make sure that the length of the returned vector is the sum of the lengths of two given vectors.

Let’s see another matrix arithmetic example. The dot product is also an operation which takes two equal-length vectors:

[1, 3, -5] · [4, -2, -1] 
  = 1 * 4 + 3 * (-2) + (-5) * (-1)
  = 3

The dot product can also benefit from type-level natural numbers if we define it by:

dotProduct :: ∀ n. Vec n Int → Vec n Int → Int

I leave the implementation of dotProduct here as an exercise for you :)

The compiler can catch all unmatched-length errors for us during compile time. It’s great, but can we do more? Can we use type-level natural numbers at runtime? Of course, we can!

Bring types to the term level

How did we map types to values? Type classes!

class Nat (a :: Nat) 
  where toInt :: NProxy a → Int
instance natZero :: Nat Zero 
  where toInt _ = 0
instance natSucc :: Nat n ⇒ Nat (Succ n) 
  where toInt _ = 1 + toInt (NProxy :: NProxy n)

Here we define a type class Nat (do not be confused with the kind Nat). I believe you can read it like reading a term-level function now:

toInt Zero = 0
toInt (Succ n) = 1 + (toInt n)

With toInt, we can make a function constructing vectors with lengths specified at the type level:

fill :: ∀ a n. Nat n ⇒ (Int → a) → Vec n a
fill f = Vec $ map f $ 0..(x - 1)
  where x = toInt (NProxy :: NProxy n)

To see how to use it:

> fill (\x -> x) :: Vec Zero Int
Vec []
> fill (\x -> x) :: Vec Three Int
Vec [0,1,2]

We can also let the compiler determine a length for us, which is quite convenient for the zero vector and the one vector:

zeroVector :: ∀ n. Nat n ⇒ Vec n Int
zeroVector = fill (\_ → 0)
oneVector :: ∀ n. Nat n ⇒ Vec n Int
oneVector = fill (\_ → 1)

The lengths of zeroVector and oneVector are polymorphic, such that they can be used with arbitrary-length vectors:

> dotProduct (1+>2+>empty) zeroVector
0
> dotProduct (1+>2+>3+>4+>empty) oneVector
10

Amazing, right? The compiler deduces all vector lengths and makes sure nothing go wrong for us!

We have seen enough vector examples. How about matrices?

Matrices are just nested vectors, e.g., the type of 2D matrices can be:

newtype Matrix (m :: Nat) (n :: Nat) a = Matrix (Vec m (Vec n a))

so all type-level techniques we used for vectors are also for matrices. If we build all matrix arithmetic in the same way, we will end up with a library which is free from any dimension error at runtime! In fact, there are already two: purescript-sized-vectors by @bodli and purescript-sized-matrices by @csicar.

The gist for the last two sections is here.

PureScript is capable of computing types at compile time. The result is more than just better type checking or safer runtime. Type-level programming can also eliminate manual works. We are just scratching the surface of type-level programming now. I will show you more in the future blogs. Hope this blog motivates you to find out more!

References

Thomas Hallgren. Fun with Functional Dependencies. 2001.

Brent Yorgey. Typed type-level programming in Haskell, part I: functional dependencies. 2010.

Thanks CYB, Ray Shih and Justin Woo for reviewing this blog.