Word count: 1528

**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^{1} 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: **Z**ero is a natural number, and the **s**uccessor 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^{2}

- An empty vector of
`a`

has size`Z`

.- 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`

!

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

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)
:| xs) = (x, xs) uncons (x
```

# 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`

.

``fmap` Nil = Nil f `

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

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

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.

You can read about Kind polymorphism and Type-in-Type in the GHC manual.↩︎

The TypeInType extension unifies the type and kind level, but this article still uses the word

`kind`

throughout. This is because it’s easier to reason about types, datatype promotion and type familes if you have separate type and kind levels.↩︎