Warning: An intermediate level of type-fu is necessary for understanding *this post.

The glorious Glasgow Haskell Compilation system, since around version 6.10 has had support for indexed type familes, which let us represent functional relationships between types. Since around version 7, it has also supported datatype-kind promotion, which lifts arbitrary data declarations to types. Since version 8, it has supported an extension called TypeInType, which unifies the kind and type level.

With this in mind, we can implement the classical dependently-typed example: Length-indexed lists, also called Vectors.

{-# LANGUAGE TypeInType #-}

TypeInType also implies DataKinds, which enables datatype promotion, and PolyKinds, which enables kind polymorphism.

TypeOperators is needed for expressing type-level relationships infixly, and TypeFamilies actually lets us define these type-level functions.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

Since these are not simple-kinded types, we’ll need a way to set their kind signatures¹ explicitly. We’ll also need Generalized Algebraic Data Types (or GADTs, for short) for defining these types.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

Since GADTs which couldn’t normally be defined with regular ADT syntax can’t have deriving clauses, we also need StandaloneDeriving.

{-# LANGUAGE StandaloneDeriving #-}

module Vector where
import Data.Kind

Natural numbers

We could use the natural numbers (and singletons) implemented in GHC.TypeLits, but since those are not defined inductively, they’re painful to use for our purposes.

Recall the definition of natural numbers proposed by Giuseppe Peano in his axioms: Zero is a natural number, and the successor of a natural number is also a natural number.

If you noticed the bold characters at the start of the words zero and successor, you might have already assumed the definition of naturals to be given by the following GADT:

data Nat where
  Z :: Nat
  S :: Nat -> Nat

This is fine if all you need are natural numbers at the value level, but since we’ll be parametrising the Vector type with these, they have to exist at the type level. The beauty of datatype promotion is that any promoted type will exist at both levels: A kind with constructors as its inhabitant types, and a type with constructors as its… constructors.

Since we have TypeInType, this declaration was automatically lifted, but we’ll use explicit kind signatures for clarity.

data Nat :: Type where
  Z :: Nat
  S :: Nat -> Nat

The Type kind, imported from Data.Kind, is a synonym for the * (which will eventually replace the latter).

Vectors

Vectors, in dependently-typed languages, are lists that apart from their content encode their size along with their type.

If we assume that lists can not have negative length, and an empty vector has length 0, this gives us a nice inductive definition using the natural number type kind²

1. An empty vector of a has size Z.
2. Adding an element to the front of a vector of a and length n makes it have length S n.

We’ll represent this in Haskell as a datatype with a kind signature of Nat -> Type -> Type - That is, it takes a natural number (remember, these were automatically lifted to kinds), a regular type, and produces a regular type. Note that, -> still means a function at the kind level.

data Vector :: Nat -> Type -> Type where

Or, without use of Type,

data Vector :: Nat -> * -> * where

We’ll call the empty vector Nil. Remember, it has size Z.

 Nil :: Vector Z a

Also note that type variables are implicit in the presence of kind signatures: They are assigned names in order of appearance.

Consing onto a vector, represented by the infix constructor :|, sets its length to the successor of the existing length, and keeps the type of elements intact.

 (:|) :: a -> Vector x a -> Vector (S x) a

Since this constructor is infix, we also need a fixidity declaration. For consistency with (:), cons for regular lists, we’ll make it right-associative with a precedence of 5.

infixr 5 :|

We’ll use derived Show and Eq instances for Vector, for clarity reasons. While the derived Eq is fine, one would prefer a nicer Show instance for a production-quality library.

deriving instance Show a => Show (Vector n a)
deriving instance   Eq a =>   Eq (Vector n a)

Slicing up Vectors

Now that we have a vector type, we’ll start out by implementing the 4 basic operations for slicing up lists: head, tail, init and last.

Since we’re working with complicated types here, it’s best to always use type signatures.

Head and Tail

Head is easy - It takes a vector with length >1, and returns its first element. This could be represented in two ways.

head :: (S Z >= x) ~ True => Vector x a -> a

This type signature means that, if the type-expression S Z >= x unifies with the type True (remember - datakind promotion at work), then head takes a Vector x a and returns an a.

There is, however, a much simpler way of doing the above.

head :: Vector (S x) a -> a

That is, head takes a vector whose length is the successor of a natural number x and returns its first element.

The implementation is just as concise as the one for lists:

head (x :| _) = x

That’s it. That’ll type-check and compile.

Trying, however, to use that function on an empty vector will result in a big scary type error:

Vector> Vector.head Nil

<interactive>:1:13: error:
    • Couldn't match type ‘'Z’ with ‘'S x0’
      Expected type: Vector ('S x0) a
        Actual type: Vector 'Z a
    • In the first argument of ‘Vector.head’, namely ‘Nil’
      In the expression: Vector.head Nil
      In an equation for ‘it’: it = Vector.head Nil

Simplified, it means that while it was expecting the successor of a natural number, it got zero instead. This function is total, unlike the one in Data.List, which fails on the empty list.

head []    = error "Prelude.head: empty list"
head (x:_) = x

Tail is just as easy, except in this case, instead of discarding the predecessor of the vector’s length, we’ll use it as the length of the resulting vector.

This makes sense, as, logically, getting the tail of a vector removes its first length, thus “unwrapping” a level of S.

tail :: Vector (S x) a -> Vector x a
tail (_ :| xs) = xs

Notice how neither of these have a base case for empty vectors. In fact, adding one will not typecheck (with the same type of error - Can’t unify Z with S x, no matter how hard you try.)

Init

What does it mean to take the initial of an empty vector? That’s obviously undefined, much like taking the tail of an empty vector. That is, init and tail have the same type signature.

init :: Vector (S x) a -> Vector x a

The init of a singleton list is nil. This type-checks, as the list would have had length S Z (that is - 1), and now has length Z.

init (x :| Nil) = Nil

To take the init of a vector with more than one element, all we do is recur on the tail of the list.

init (x :| y :| ys) = x :| Vector.init (y :| ys)

That pattern is a bit weird - it’s logically equivalent to (x :| xs). But, for some reason, that doesn’t make the typechecker happy, so we use the long form.

Last

Last can, much like the list version, be implemented in terms of a left fold. The type signature is like the one for head, and the fold is the same as that for lists. The foldable instance for vectors is given here.

last :: Vector (S x) a -> a
last = foldl (\_ x -> x) impossible where

Wait - what’s impossible? Since this is a fold, we do still need an initial element - We could use a pointful fold with the head as the starting point, but I feel like this helps us to understand the power of dependently-typed vectors: That error will never happen. Ever. That’s why it’s impossible!

  impossible = error "Type checker, you have failed me!"

That’s it for the basic vector operations. We can now slice a vector anywhere that makes sense - Though, there’s one thing missing: uncons.

Uncons

Uncons splits a list (here, a vector) into a pair of first element and rest. With lists, this is generally implemented as returning a Maybe type, but since we can encode the type of a vector in it’s type, there’s no need for that here.

uncons :: Vector (S x) a -> (a, Vector x a)
uncons (x :| xs) = (x, xs)

Mapping over Vectors

We’d like a map function that, much like the list equivalent, applies a function to all elements of a vector, and returns a vector with the same length. This operation should hopefully be homomorphic: That is, it keeps the structure of the list intact.

The base package has a typeclass for this kind of morphism, can you guess what it is? If you guessed Functor, then you’re right! If you didn’t, you might aswell close the article now - Heavy type-fu inbound, though not right now.

The functor instance is as simple as can be:

instance Functor (Vector x) where

The fact that functor expects something of kind * -> *, we need to give the length in the instance head - And since we do that, the type checker guarantees that this is, in fact, a homomorphic relationship.

Mapping over Nil just returns Nil.

 f `fmap` Nil = Nil

Mapping over a list is equivalent to applying the function to the first element, then recurring over the tail of the vector.

 f `fmap` (x :| xs) = f x :| (fmap f xs)

We didn’t really need an instance of Functor, but I think standalone map is silly.

Folding Vectors

The Foldable class head has the same kind signature as the Functor class head: (* -> *) -> Constraint (where Constraint is the kind of type classes), that is, it’s defined by the class head

class Foldable (t :: Type -> Type) where

So, again, the length is given in the instance head.

instance Foldable (Vector x) where
   foldr f z Nil = z
   foldr f z (x :| xs) = f x $ foldr f z xs

This is exactly the Foldable instance for [a], except the constructors are different. Hopefully, by now you’ve noticed that Vectors have the same expressive power as lists, but with more safety enforced by the type checker.

Conclusion

Two thousand words in, we have an implementation of functorial, foldable vectors with implementations of head, tail, init, last and uncons. Since going further (implementing ++, since a Monoid instance is impossible) would require implementing closed type familes, we’ll leave that for next time.

Next time, we’ll tackle the implementation of drop, take, index (!!, but for vectors), append, length, and many other useful list functions. Eventually, you’d want an implementation of all functions in Data.List. We shall tackle filter in a later issue.