# Intro to type-level programming in Haskell - Part 2

*This is the second part of the series of posts on this topic. You can find the first part
here.*

In the previous part of this tutorial we created a `List a empty`

for which we could tell from its
type whether it is empty or not (by `empty`

being other `Empty`

or `NonEmpty`

). This is how our
final code looked like:

The question where we left off was: can we create `safeTail`

function that would accept only
non-empty lists?

Let’s try to construct its type signature:

Everything makes sense except one thing - we don’t know in compile time what is `empty`

going
to be for a returned list.
It depends on the input list - if it has only one element, the result will be `Empty`

.
Otherwise, it will be `NonEmpty`

But the problem is that with our current type system we cannot
differentiate between them and they are both marked as `NonEmpty`

.

### [Going deeper] But what if we just put `List a smth`

as a return type?

In the previous part of the tutorial we had cases where the created list had `empty`

type param
which just stayed general and that worked. So what would happen if we tried that here?

Ok, so here is what we are trying to compile:

This looks like we are trying to leave to the compiler to determine what will `smth`

actually be,
we just say “this will be something/anything”. Plus we have a type param value `smth`

that doesn’t
appear anywhere in the function arguments, on the “left” side, but just in the result. I am not
sure if that could make sense in any case?

But interesting thing is, the following compiles:

It doesn’t say *“you have type param value smth which doesn’t appear anywhere on the left side.”*
which surprised me a bit. I still wonder why could that be valid?

But if we try to compile the original function, it fails. The error message is a bit longer as
usual with Haskell, but from what I understood it basically says the following: *“I can see from
the List constructors that any list you create will have a specific type, and you are here
trying to say it will be just anything. Tell me exactly what it is.”*

*TODO*: I am not sure if I got this completely right. Figure out what is exactly the reason this
does not compile.

The conclusion from all this is: we need a more expressive type so we can specifically say what is the type of the returned list going to be!

## Example: Length indexed lists (vectors)

*NOTE: in other tutorials often is used the term “Vector” instead of “List”,
which we used so far.*

What is the next piece of information about the list we can know, besides is it empty or not? It is
its length - and if we could knew that, we could implement `safeTail`

without problems. We wouldn’t
worry what “type” of *non-emptiness* input list has - we would just reduce the length by one.

Let’s see how we can encode length into the type of our list.

### Encoding list’s length in its type

Our list type is going to look like this:

Again we have two type parameters, `a`

is for type of elements in the list while `length`

is for
type from which we can tell the list’s length.

Before we had just two values (or “list states”) that we needed to encode with types, `Empty`

and
`NonEmpty`

, so we created two types (or one type with two data constructors when we used
`DataKinds`

). But this time we have infinite amount of values, since length of a list can be
any natural number. So how do we represent that with types?
We can do it in the same way we defined the list itself, recursively:

`Succ`

stands for *Successor*. We can see that since `Succ`

is a parametrized type constructor
we can actually from it create infinite amount of types and that solves our problem. This works,
but as in a previous example it would be better to use `DataKinds`

so we have type safety
(otherwise somebody can write nonsense such as `Succ Bool`

and it would be a valid term):

And this is it! From this, `DataKinds`

will create type constructors `'Zero`

and `'Succ nat`

. Let’s
see their kinds and compare them to types of the data constructors they originated from
(`Zero`

and `Succ`

).

The types of data constructors look exactly the same as kinds of newly created type constructors!
This is what `DataKinds`

does - promotes data into types, and types into kinds. We ended up with
a new kind `Nat`

and we can create infite amount of types with that kind:

Now let’s use this and create a type for our length-indexed list:

The main difference from the previous example is how we are managing types in `Cons`

. Instead
of just putting e.g. `NonEmpty`

, here we are building on top of the input type, length of the input
list. So if the input list had length `'Succ 'Zero`

, the new one will have `'Succ ('Succ 'Zero)`

.

And that is it! We have now defined list which will have its length contained in its type. Let’s see it in action:

Wohoo, it works! Now we can finally implement `safeTail`

:

Let’s test it out:

Everything works as expected. This time we didn’t have any trouble defining `safeTail`

’s types -
we restricted input list to have at least one element (`'Succ n`

) and then output will simply be
of length `n`

.

The basic implementation of length-index list is now done. We can create a list and we can also
operate with `safeTail`

and `safeHead`

on it. Is there anything else we might need?

### List concatenation - making it work on type level

For example, what if we wanted to concatenate two lists? Logically, we know that the resulting list will have length which is sum of lengths of the input lists. But how do we represent it on type level?

Let’s try to see what will the function signature look like. We will call this function `append`

(so we don’t confuse it with Prelude’s `concat`

) - it will take two lists and produce a new list
which is a concatenation of those two input lists:

Let’s also see a few examples of how it would work:

So we take two lists of lengths `n`

and `m`

respectively (we don’t care if
there are empty or not in this case, since there isn’t any “unsafe” scenario) and we
produce a new list of length `n + m`

. But how do we represent its
length, what do we put in place of `?`

?

Obviously, we want to sum `m`

and `n`

- but how do we do that on the type level?

### Type families - functions that operate on types

Turns out there is a special mechanism for this in Haskell and it is provided in form of another
language extension named `TypeFamilies`

.