### Introduction

Lets try and write a typed list in Scala: a list whose size is known at compile time.

(all the source code available at gitHub)

While the idea is not exactly new, there aren’t so many tutorials on how to go about this. Above all though, it is a great excuse to practice with the type system, implicits and recursion.

So, a typed list, besides being parameterized by the type of elements it holds, like the common `List[+A]`

, it is also parameterized by its size as in `TypedList[+A, Size]`

.

This means there are some verifications that can be transferred from run-time to compile-time – basically, everything related with list size. Some examples:

Normal List | Typed List | |

EmptyList.head along with max, min, last | Run-time exception | Does not compile |

ListA(index)i.e get element at index | Run-time IndexOutOfBoundsException if index > than list size (or index < 0) | Does not compile |

listA zip listB | Drops extra elements of bigger list List(1, 2, 3) zip List(10, 20) // res: List( (1, 10), (2, 20) ) | Does not compile if lists are of ≠ size |

listA splitAt index | Returns an empty list when index is out of bounds List(1, 2, 3).splitAt(4) // res: ( List(1, 2, 3) , List() ) | Does not compile if index is > then the list size |

listA filter predicate | Possible | Impossible (unless we return a normal list) |

Notice there are some operations impossible to construct on typed lists, or rather, which will invariably have a different "api". For example, we can not expect to return a typed list on the filter method as the filtering is done at run-time and there is no information at compile-time of how many elements would satisfy the predicate. The signature on filter must therefore return a normal list.

At the end the api should be something along:

```
val foo: TypedList[Int, Nat5] = 11 :: 20 :: 34 :: 49 :: 54 :: TypedNil
foo.split[Nat2]
// res: (TypedList[Int, Nat2], TypedList[Int, Nat3]) = (TypedList(11, 20), TypedList(34, 49, 54) )
foo.get[Nat4]
// res: Int = 49
val bar: TypedList[Int, Nat2] = 1000 :: 2000 :: TypedNil
foo concat bar
// res: TypedList[Int, Nat7] = TypedList(11, 20, 34, 49, 54, 1000, 2000)
foo.map(elem => s"Foo-" + elem)
// res: TypedList[String, Nat5] = TypedList(Foo-11,Foo-20,Foo-34,Foo-49,Foo-54)
```

### The Natural numbers

As the size of the list, it being the number of elements it holds, can only be 0 or greater and since we want to parameterize a list on its size, then the 1st step is to encode the natural numbers at the type level; such that there is a type for every natural number.

The following is a pivotal step of the whole process. The baseline was the encoding of natural numbers as presented here and here. It starts with:

```
sealed trait Natural
case object Zero extends Natural
case class Suc[N <: Natural]() extends Natural
```

The following diagram captures the type hierarchy.

This encoding is recursive. `Suc`

(as in successor) is a type constructor that must take a concrete **natural** type to "construct" yet another **natural** type.

This infinite loop can only start at `Zero`

as `Zero.type`

is the only **concrete** natural (and so it can be passed to `Suc`

) that is not build from a previous one.

Throughout the post we will be using aliases for the natural types:

```
type Nat0 = Zero.type
type Nat1 = Suc[Nat0]
type Nat2 = Suc[Nat1]
type Nat3 = Suc[Nat2]
...
```

This is cleaner and more intelligible than using `Suc[Suc[Suc[Suc[Suc[Suc[Suc[.....`

to represent some number.

One might wonder then, the advantage of using such a fancy formulation if we need to manually type every single number.

I simpler formulation would be just:

```
sealed trait Natural
case object Zero extends Natural
case object One extends Natural
case object Two extends Natural
case object Three extends Natural
....
```

But notice that in this formulation the numbers have no relation between themselves. We would be unable to sum, subtract or multiply two numbers together as we will see further down. These operations with naturals being essential for a generic formulation.

## Raw signature of the TypedList

With the above we now have:

```
sealed trait TypedList[+Element, Size <: Natural]
```

Where we have co-variance with `Element`

as in a normal list.

Having co-variance on `Size`

as well was my first approach, but it lead to an array of problems downstream as discussed on this SO post . I settled with invariance as Joe Barnes (minute 24:40).

```
sealed trait TypedList[+Element, Size <: Natural]{
def head: Element
}
case object TypedNil extends TypedList[Nothing, Zero.type] {
override val head: Nothing = throw new Exception("Boom!")
}
case class TypedCons[Element, N <: Natural](
head: Element,
tail: TypedList[Element, N]
) extends TypedList[Element, Suc[N]]
```

The following is another **fundamental** concept:

`TypedCons[_, N]`

extends `TypedList[_, Suc[N]]`

.

Why ?

Wouldn’t it be more intuitive to extend `TypedList[_, N]`

instead ?

Because the tail’s size must be one less than the current list!

With the current formulation, a `TypedCons[_, Nat4]`

is a `TypedList[_, Nat5/*(= Suc[Nat4])*/]`

with a tail of size `Nat4`

. Very smart !
If the extension was on `TypedList[_, N]`

how would we encode that property?

Continuing, notice we are still able to access the head of an empty list:

```
val emptyList = TypedNil
val foo = emptyList.head // compiles and
java.lang.Exception: Boom! // blows-up at compile time
```

But now we are powerful enough to solve this; with the help of phantom types:

```
sealed trait TypedList[+Element, Size <: Natural]{
def head[PhantomType >: Size <: Suc[_ <: Natural]: Element
}
```

`PhatomType`

(name irrelevant, could be `BlaBla`

) above exists for a single purpose: To encode a type constraint.

We demand the compiler to find a type (the `PhatomType`

) such that it must have `Size`

( of the list) as lower-bound and `Suc[_ <: Natural]`

as upper-bound. With the help of figure 1 you will conclude this is impossible if `Size`

is `Zero.type`

as in the `TypedNil`

case; Now the compiler fails:

```
val emptyList = TypedNil
val foo = emptyList.head // Does not compile with error:
error: type arguments [Zero.type] do not conform to method head's type parameter bounds [PhantomType >: Zero.type <: Suc[_ <: Natural]]
TypedNil.head
^
```

## The .map and .zip operations

This are the simplest methods to implement and do not require any reasoning more advanced than their counterparts in a normal list.

#### The .map

We are interested in developing a `.map`

method that should have the same meaning as in a normal list: apply the same function to every element. In our case, the returning list should have the same length as the original:

```
sealed trait TypedList[+Element, Size <: Natural] {
def map[OtherType](f: Element => OtherType): TypedList[OtherType, Size]
}
```

```
case object TypedNil extends TypedList[Nothing, Zero.type] {
override def map[OtherType](f: Nothing => OtherType): TypedList[Nothing, Zero.type] = this
}
```

```
case class TypedCons[Element, Size <: Natural](
override val _head: Element,
tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def map[OtherType](f: Element => OtherType): TypedList[OtherElement, Suc[Size]] = TypedCons(f(head), tail.map(f))
}
```

#### The .zip

This case is a slightly more interesting.

So, you have two lists and you want to perform an operation on every pair – each element (of the pair) being provided by a different list but at the same index.*

On a normal list you cannot enforce the two lists to have the same size; when one is longer, its additional elements are ignored:

```
val foo = List(1, 2, 3, 4)
val bar = List(1, 2, 3)
foo.zip(bar)
//res: List((1,1), (2,2), (3,3))
```

Now, not only can we enforce that, it comes out as very natural.

On the signature at `TypedList`

, `zip`

must receive another list whose size must be the same as the current list:

```
sealed trait TypedList[+Element, Size <: Natural]{
def zip[OtherType, C](that: TypedList[OtherType, Size], f: (Element, OtherType) => C): TypedList[C, Size]
}
```

```
case object TypedNil extends TypedList[Nothing, Zero.type]{
override def zip[OtherType, C](that: TypedList[OtherType, Zero.type], f: (Nothing, OtherType) => C): TypedList[C, Zero.type] = this
}
```

```
case class TypedCons[Element, Size <: Natural](
override val _head: Element,
tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def zip[OtherType, C](that: TypedList[OtherType, Suc[Size]], f: (Element, OtherType) => C): TypedList[C, Suc[Size]] = that match {
case TypedCons(thatHead, thatTail) => TypedCons(f(head, thatHead), tail.zip(thatTail, f))
}
}
```

**An interesting detour**

Above, we must pattern match the `that`

list on the `TypedCons`

implementation. Not only that, but that match has only 1 case which is exhaustive! How come ?

We must pattern match because the list `that`

is a `TypedList`

and there is no `tail`

defined there; only on `TypedCons`

. At the same time, we need to have access to the `tail`

in order to achieve the semantics of `zip`

via recursion.

One would think that we would then have to specify logic for the 2 cases (`TypedNil`

and `TypedCons`

). Not necessary! since the compiler knows that a `TypedList[OtherType, Suc[Size]]`

can never be `TypedNil`

for any given `Size <: Natural`

.
This is kinda funny behavior from the compiler.

But could we take out the pattern match? Yes.

The difficulty is in defining a tail on the trait `TypedList`

since we must restrict it (the tail) to have size 1 less than the `TypedList`

.
Recall for the `TypedCons`

case this was embedded in the definition of `TypedCons`

itself and the way it extended `TypedList`

.

In other words, what should we substitute `???`

below for ?

```
sealed trait TypedList[+Element, Size <: Natural] {
def head: Element
def tail: TypedList[Element, ???]
}
```

The answer lies in defining a type `Previous`

for every `Natural`

type.

```
sealed trait Natural {
type Previous <: Natural
}
case object Zero extends Natural {
override type Previous = Zero.type
}
case class Suc[N <: Natural]() extends Natural {
override type Previous = N
}
```

Which allows us then to do:

```
sealed trait TypedList[+Element, Size <: Natural]{
protected def _tail: TypedList[Element, Size#Previous]
def tail[PhantomType >: Size <: Suc[_ <: Natural]] = _tail
}
```

With now a tail on the super trait, we don’t need the annoying pattern match on `that`

:

```
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def zip[OtherType, C](that: TypedList[OtherType, Suc[Size]], f: (Element, OtherType) => C): TypedList[C, Suc[Size]] =
TypedCons(f(head, that.head), tail.zip(that.tail, f))
}
```

### The .concat method

This is where things get more interesting.

The `.concat`

should give us a new list with the elements from the left followed by the elements of the right. Something like

```
val foo: TypedList[String, Nat2] = "Foo" :: "Bar" :: TypedNil
val bar: TypedList[String, Nat2] = "Baz" :: "Qux" :: TypedNil
foo.concat(bar)
// res: TypedList[String, Nat4] = TypedList(Foo, Bar, Baz, Qux)
```

The resulting list should naturally also be typed and so the compiler must know how to sum two natural numbers:

```
sealed trait Natural {
type Plus[That <: Natural] <: Natural
}
```

which is trivial for `Zero.type`

:

```
case object Zero extends Natural {
override type Plus[That <: Natural] = That
}
```

It took me a few minutes and pen and paper to convince myself that the recursive formulation embodies summation:

```
case class Suc[N <: Natural]() extends Natural {
override type Plus[That <: Natural] = Suc[N#Plus[That]]
}
```

The recursive loop (at the tyle level) eventually hits Zero.type, ending and returning the desired type.

With this we can define the signature:

```
sealed trait TypedList[+Element, Size <: Natural]{
def concat[OtherElement >: Element, OtherSize <: Natural](that: TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Size#Plus[OtherSize]]
}
```

With the following implementations:

```
case object TypedNil extends TypedList[Nothing, Zero.type]{
override def concat[OtherElement >: Nothing, OtherSize <: Natural](that: TypedList[OtherElement, OtherSize]): TypedList[OtherElement, OtherSize] = that
}
```

```
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def concat[OtherElement >: Element, OtherSize <: Natural](that: TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Suc[Size#Plus[OtherSize]]] =
TypedCons(head, tail.concat(that))
}
```

### The .flatMap

This method is useful to explain another operation on natural numbers: multiplication.

On a `.flatMap`

, we apply a function to every element of the left list, such that the result (for each element) is another list, flattening everything at the end.

```
val foo: List[Int] = List(1, 2, 3)
def bar(i: Int): List[String] = i match {
case 1 => List("Foo")
case 2 => List("Bar", "Baz")
case 3 => List("Qux", "Quux", "FooBar", "BarBaz")
case _ => List()
}
foo.flatMap(bar)
//res: List[String] = List(Foo, Bar, Baz, Qux, Quux, FooBar, BarBaz)
```

The above cannot be achieved on our typed list. The size of the lists being returned for each case depends on values! Therefore the resulting list’ size could not be known at compile time.

We can however, formulate a `.flatMap`

such that each returned list is of a constant/pre-determined size. Whether or not that is useful for anything is another question.

Before spoiling with the signature, understand that we need multiplication of naturals: If the original list has **n** elements, each of which is mapped to a list of **m** elements, the result after flattening shall have **n*m** elements.

```
sealed trait Natural {
type Plus[That <: Natural] <: Natural
type Mult[That <: Natural] <: Natural
}
```

Again the trivial case for Zero:

```
case object Zero extends Natural {
override type Plus[That <: Natural] = That
override type Mult[That <: Natural] = Zero.type
}
```

and the more elaborate

```
case class Suc[N <: Natural]() extends Natural {
override type Plus[That <: Natural] = Suc[N#Plus[That]]
override type Mult[That <: Natural] = (N#Mult[That])#Plus[That]
}
```

which leverages the distributive property of multiplication; note that at every iterative step one uses `(N + 1) x M = N x M + M`

(where `N + 1`

is to be interpreted as `Suc[N]`

).

Again, the formulation is recursive. It stops when, on a step, `N`

corresponds to `Zero.type`

.

We are now capable of knowing at the type level the result of the multiplication of two natural numbers. This is essential and enables us to easily come up with a signature to `.flatMap`

:

```
sealed trait TypedList[+Element, Size <: Natural] {
def flatMap[OtherElement, OtherSize](f: Element => TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Size#Mult[OtherSize]
}
```

```
case object TypedNil extends TypedList[Nothing, Zero.type]{
override def flatMap[OtherElement, OtherSize <: Natural](f: Nothing => TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Zero.type] = this
}
```

But it remains a challenge to come up with the actual implementation for the `TypedCons`

case. After some thinking I came up with:

```
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def concat[OtherElement >: Element, OtherSize <: Natural](that: TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Suc[Size#Plus[OtherSize]]] =
TypedCons(head, tail.concat(that))
override def flatMap[OtherElement, OtherSize <: Natural](f: Element => TypedList[OtherElement, OtherSize]): TypedList[OtherElement, (Size#Mult[OtherSize])#Plus[OtherSize]] =
f(head) concat tail.flatMap(f)
}
```

This recursive formulation is simple and elegant. It takes advantage of `.concat`

and would do exactly what we want. Would! To my initial surprise, the compiler rejects it :

```
[error] type mismatch;
[error] found : TypedList[OtherElement,OtherSize#Plus[Suc[Size]#Previous#Mult[OtherSize]]]
[error] (which expands to) TypedList[OtherElement,OtherSize#Plus[Size#Mult[OtherSize]]]
[error] required: TypedList[OtherElement,Size#Mult[OtherSize]#Plus[OtherSize]]
[error] f(head) concat tail.flatMap(f)
[error] ^
```

All this chained types might be a too convoluted for someone scrolling down.

Using more legible syntax, the compiler complains that it expects something of type `(Size x OtherSize) + OtherSize`

but `f(head) concat tail.flatMap(f)`

actually resolves to type `OtherSize + (Size x OtherSize)`

.

Summation is commutative. Because we are sure we coded summation of Nats correctly, this too should end up, for any `Size`

and `OtherSize`

, to the same type. Well, it turns out the compiler doesn’t know that !

## I found two ways to solve this

### 1. Acceptable trick

While `f(head) concat tail.flatMap(f)`

above resolves to `OtherSize + (Size x OtherSize)`

, if we revert the order to `tail.flatMap(f) concat f(head)`

we get the type the compiler expects: `(Size x OtherSize) + OtherSize`

.

But `tail.flatMap(f) concat f(head)`

does not do solely what we want; it also reverts the order of the elements on the list – as is apparent from the tail appearing first:

```
val foo: TypedList[Int, Nat3] = 1 :: 2 :: 3 :: TypedNil
def bar(i: Int): TypedList[Int, Nat2] = TypedCons(i*1, TypedCons(i*10))
foo.flatMap(bar)
// res: TypedList[Int, Nat6] = TypedList(30, 30, 20, 20, 10, 10)
```

The trick, therefor, consists in reverting the list either before or after that `.flatMap`

operation. Inefficient but effective.

```
package foo
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def concat[OtherType >: Element, OtherSize <: Natural](that: TypedList[OtherType, OtherSize]): TypedList[OtherType, Suc[Size#Plus[OtherSize]]] =
TypedCons(head, tail.concat(that))
override def flatMap[OtherType, OtherSize <: Natural](f: Element => TypedList[OtherType, OtherSize]): TypedList[OtherType, Size#Mult2[OtherSize]#Plus[OtherSize]] =
_flatMapInternal(f).reverse
override private [foo] def _flatMapInternal[OtherType, OtherSize <: Natural](f: Element => TypedList[OtherType, OtherSize]): TypedList[OtherType, Size#Mult2[OtherSize]#Plus[OtherSize]] =
tail._flatMapInternal(f) concat f(head)
override def reverse: TypedList[Element, Suc[Size]] = tail.reverse :+ head
override def :+[A1 >: Element](elem: A1): TypedCons[A1, Suc[Size]] = TypedCons(head, tail.:+(elem))
}
```

Notice it was necessary to develop a `reverse`

operation which in turn required the append operation `:+`

as well.

More importantly, the actual "flatMapping" is done at `_flatMapInternal`

. Being the responsibility of the api method `flatMap`

just to call it and then reverse the result it gets. Now we obtain:

```
val foo: TypedList = 1 :: 2 :: 3 :: TypedNil
def bar(i: Int): TypedList[Int, Nat2] = TypedCons(i*1, TypedCons(i*10))
foo.flatMap(bar)
// res: TypedList[Int, Nat6] = TypedList(10, 10, 20, 20, 30, 30)
```

### 2. Formulate multiplication at the type level differently

The formulation of multiplication above is correct. In fact, it is the same as the one from these guys on slide 27, which do appear to know a lot about the issue.

To solve our problem however, I just tried to change the order of the operands:

```
case class Suc[N]() extends Natural {
override type Mult[M <: Natural] = M#Plus[N#Mult[M]]
// instead of
// override type Mult[M <: Natural] = (N#Mult[M])#Plus[M]
}
```

The question is whether this formulation is equivalent. Does it also embody multiplication as required ? Yes, it does. All the below compile:

```
implicitly[Nat3#Mult[Nat2] =:= Nat6]
implicitly[Nat5#Mult[Nat2] =:= Nat10]
implicitly[Nat2#Mult[Nat9] =:= Nat2#Mult2[Nat9]]
implicitly[Nat3#Mult[Nat8] =:= Nat3#Mult2[Nat8]]
```

Where `Mult2`

corresponds to the initial "encoding" of multiplication.

With this new formulation for the type contructor field `Mult`

, the compiller will glady accept:

```
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def concat[OtherElement >: Element, OtherSize <: Natural](that: TypedList[OtherElement, OtherSize]): TypedList[OtherElement, Suc[Size#Plus[OtherSize]]] =
TypedCons(head, tail.concat(that))
override def flatMap[OtherType, OtherSize <: Natural](f: Element => TypedList[OtherType, OtherSize]): TypedList[OtherType, OtherSize#Plus[Size#Mult[OtherSize]]] =
f(head) concat tail.flatMap(f)
}
```

Without the need for that internal flatMap function and without the need for the reverse operation. This approach is not only more elegant, but also more efficient.

### The .split

At last the `.split`

operation. The most difficult to implement.

We are interested in the following behaviour:

```
val foo: TypedList[String, Nat5] = "Foo" :: "Bar" :: "Baz" :: "Qux" :: "Quux" :: TypedNil
val (left, right) = foo.split[Nat2]
// res (left): TypedList[String, Nat2] = TypedList(Foo, Bar)
// res (right): TypedList[String, Nat3] = TypedList(Baz, Qux, Quux)
```

If we want the resulting lists to be typed, then we need to encode subtraction of natural numbers. Above, the compiler needed to know how to subtract 2 from 5.

Encoding multiplication is easy once you read how to encode summation.

Subtraction was trickier. With the help of @Alexey Romanov in these SO question, we have:

```
package foo
sealed trait Natural {
type Previous <: Natural
private [foo] type _Minus[M <: Natural] <: Natural
type Minus[M <: Natural] = M#_Minus[Suc[Previous]]
}
```

This encoding might feel confusing. Reading the SO thread might shed some light.

This hack is very much the same as the "1st solution" for the flatMap problem discussed previously, where we had an internal `_flatMap`

. This is the type-level counterpart.

The type constructor to be exposed is `Minus[M <: Natural]`

. `_Minus`

is internal and a way to achieve the semantics of subtraction.

```
case object Zero extends Natural {
override type Previous = Zero.type
override private [foo] type _Minus[M <: Natural] = M
}
```

```
case class Suc[N <: Natural]() extends Natural {
override type Previous = N
override private [foo] type _Minus[M <: Natural] = Previous#_Minus[M#Previous]
}
```

Notice that `_Minus`

above, on its own, would only work if `M`

was greater than `Suc[N]`

:

```
Nat2#_Minus[Nat3] =
Nat1#_Minus[Nat2] =
Nat0#_Minus[Nat1] = Nat1
// Good
```

But

```
Nat3#_Minus[Nat2] =
Nat2#_Minus[Nat1] =
Nat1#_Minus[Nat0] =
Nat0#_Minus[Nat0] = Nat0
// Bad
```

Therefore, we hide `_Minus`

and wrap it within `Minus`

, which, before calling `_Minus`

inverts the operands (swap the the n and m in `n - m`

)

```
We then obtain the desired behaviour:
// Subtracting n-m:
// Works when n>m
implicitly[Nat9#Minus[Nat5] =:= Nat4] // compiles
// Gives 0 when n<m (more than fine. We are not interested nor model the negative numbers)
implicitly[Nat0#Minus[Nat5] =:= Nat0] // compiles
implicitly[Nat2#Minus[Nat5] =:= Nat0] // compiles
```

We have defined the types to be returned by the `split`

method. Proceeding to defining the methods themselves.

```
sealed trait TypedList[+Element, Size <: Natural] {
def split[At <: Suc[_ <: Natural]]: (TypedList[Element, At], TypedList[Element, Size#Minus[At])
}
```

For `TypedNil`

case we will just thrown an exception because we will be protecting, further down, the method from access.

For `TypedCons`

, my idea was:

To split `TypedList("Foo", "Bar", "Baz", "Qux", "Quux")`

at index `Nat3`

:

- Construct a
`TypedList[Natural, Nat3](nat1, nat2, nat3)`

. - Construct a
`TypedList[Natural, Nat2](nat4, nat5)`

. - Develop a
`get(index: Natural)`

method, on our`TypedList`

, such that it will retrieve the element of the list at said index. - Map lists 1. and 2. passing them function
`get`

.

```
case class TypedCons[Element, Size <: Natural](
override protected val _head: Element,
override protected val _tail: TypedList[Element, Size]
) extends TypedList[Element, Suc[Size]] {
override def split[At <: Suc[_ <: Natural]](
implicit n: At,
leftList: TypedList[Natural, At],
rightList: TypedList[Natural, Suc[Size]#Minus[At]]
): (TypedList[Element, At], TypedList[Element, Suc[Size]#Minus[At]]) =
(
leftList.map(_get),
rightList.map(i => _get(i.plus(n)))
)
}
```

Requiring 3 implicits, this signature seems daunting.

Why are `leftList`

and `rightList`

relevant ?

- Because they provide typed lists of the the same size of the ones the function has to return! – half the job is done right here.

And why are they implicit variables?- Is a way to have the compiler recursively build something as we will see below ( is there any other way even ?)

- Because their elements are the sequence of natural numbers starting at nat1.

And why is this relevant?- because we also have a function
`_get`

that retrieves an element from a typed list if given an index!

- because we also have a function

Where we don’t show the implementation of `_get`

– which is not difficult to formulate.

But how is the compiler able to find these implicits? Because we defined, on the implicit search scope, and for this usage only, specifically "engineered" implicits:

```
implicit def typedListOfNats[N <: Natural](implicit previousNatTypedList: TypedList[Natural, N], thisNat: Suc[N]): TypedList[Natural, Suc[N]] =
previousNatTypedList :+ thisNat
implicit def emptyList[A]: TypedList[A, Zero.type] = TypedNil
```

It is hopefully not difficult to understand the above implicits allow for the behaviour:

```
implicitly[TypedList[Nat4]]
//res: TypedList[Natural, Nat4] = TypedList(nat1, nat2, nat3, nat4)
```

In retrospective, maybe I should have wrapped the 3 implicits within something like `SplittableOps[At <: Natural, Size <: Natural]`

for more control. Imagine someone provided implicit instances of `TypedList[Natural, Suc[N]]`

with a different usage in mind. I guess we would then be under the risk of a faulty implementation of `split`

since the wrong `leftList`

and `rightList`

might be being injected.

Lastly, notice that we are still able to split a TypedList by an index greater than the list’s size:

```
val foo: TypedList[String, Nat5] = "Foo" :: "Bar" :: "Baz" :: "Qux" :: "Quux" :: TypedNil
foo.split[Nat6]
// res: java.lang.Exception: Boom!
```

Restraining calls to method `split`

for indexes greater than the list’s size is more demanding than using a phatom type as done for protecting calls to `head`

and `tail`

on an empty list. Instead, we need to protect this calls with an implicit evidence.

```
def split[At <: Suc[_ <: Natural]](implicit ev: LowerOrEqual[At, Size])
```

The rationale goes as follows:
Every time `split[At]`

(from within given `TypedList[Element, Size]`

) is called, the compiler must be able to find an instance for the concrete type `LowerOrEqual[At, Size]`

, where `At`

is the concrete type with which `split`

was called and `Size`

is the concrete type of the list. If it is not able, it will fail with a compilation error.

Our job is therefore to come up with `LowerOrEqual[N <: Natural, M <: Natural]`

and corresponding implicits such that they (the implicits), can only be found if `N <= M`

.

```
import scala.annotation.implicitNotFound
@implicitNotFound("${N} is not lower or equal to ${M}")
sealed trait LowerOrEqual[N <: Natural, M <: Natural]
object LowerOrEqual {
implicit def foo[N <: Natural, M <: Natural](implicit ev: LowerOrEqual[N, M]): LowerOrEqual[Suc[N], Suc[M]] = new LowerOrEqual[Suc[N], Suc[M]] {}
implicit def bar[M <: Natural]: LowerOrEqual[Zero.type, M] = new LowerOrEqual[Zero.type, M] {}
}
```

Notice that:

- trait
`LowerOrEqual`

doesn’t need to have any fields (vals, vars, defs, ….) . It is the type itself (in this case a type constructor), represented by`LowerOrEqual`

, and the implicit defs that matter for what we want to achieve. - The names
`foo`

and`bar`

are also pretty irrelevant.

We can "unit test" that the above encapsulates the constraint we want:

```
implicitly[LowerOrEqual[Nat5, Nat6]] // compiles (i.e. implicit found)
implicitly[LowerOrEqual[Nat2, Nat2]] // compiles (i.e. implicit found)
implicitly[LowerOrEqual[Nat6, Nat5]] // does not compile (i.e. implicit not found)
// error: Nat6 is not lower or equal to Nat5
```

How exactly do those two `foo`

and `bar`

implicit defs achieve this behavior ? Via implicit recursion and clever engineering of the return types of the two functions. Lets study the possible cases:

**case 1**. `LowerOrEqual[Nat0, NatY]`

(for some `NatY`

)

The compiler realizes function `bar`

can return the desired type (for the appropriate `M`

in `bar[M <: Natural]`

. Problem solved.

**case 2**. `LowerOrEqual[NatX, Nat0]`

(for some `NatX`

not `Nat0`

)

The compiler realizes neither function `bar`

or `foo`

may ever return the necessary type. Compiler error.

**case 3**. `LowerOrEqual[NatX, NatY]`

(where `NatX`

and `NatY`

are not `Nat0`

)

The compiler understands function `foo`

may potentially return the desired type. For that however, it needs to find yet another implicit: the argument `ev`

in `foo`

. And so this gives origin to a recursive implicit resolution by the compiler, which ultimately leads to either **case 1**, thus compiling, or **case 2**, thus not compiling.

You should be able to notice, by looking at the return type of function `foo`

and the type of `ev`

that:

a. **Case 1** is reached if and only if `N < M`

b. **Case 2** is reached if and only if `N > M`

The annotation `implicitNotFound`

‘s purpose is for more informative errors for clients of library. We would get otherwise: `could not find implicit value for parameter e: LowerOrEqual[Nat6,Nat5]`

. Which actually sheds more light on the internals of what is going on.

The above methods are the most interesting to develop and explain.

On the code on github, there are a couple more. But there was no attempt to recreate all methods on the normal List.

If you have any questions or comments about the post, I would be happy to hear. Just write on the comment section

### Footnotes

- Here I extend the behavior of
`zip`

to applying any given function to a pair of elements, instead of just joining the two elements in a tuple. - The motivation for developing this typed list and blog post was a very nice talk by Joe Barnes.

Another essential source knowledge was this blog post from Yao Li, which I highly recommend. That said, I have derived everything on the lib on my own and added several new features, most important of these being the`split`

operation and type constructor`Minus`

on naturals.

### References

1. Barnes, Joe. Typelevel Programming 101: The Subspace of Scala.

https://www.youtube.com/watch?v=_-J4YRI1rAw&t=5s

2. Li, Yao. Dependent Types in Scala.

https://lastland.github.io/pl-blog/posts/2017-09-03-dtscala.html

3. Zeiger, Stefan. Type-Level Computations in Scala.

http://slick.lightbend.com/talks/scalaio2014/Type-Level_Computations.pdf