A TypedList in Scala

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 ListTyped List
EmptyList.head along with
max, min, last
Run-time exceptionDoes 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 listBDrops 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 indexReturns 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 predicatePossibleImpossible (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.

Fig.1 – Type hierarchy of the encoding of natural numbers

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?

Fig.2 – TypedCons[A, Size] is a (subtype of) TypedList[A, Suc[Size]] with a tail: TypedList[A, Size]

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:

  1. Construct a TypedList[Natural, Nat3](nat1, nat2, nat3).
  2. Construct a TypedList[Natural, Nat2](nat4, nat5).
  3. Develop a get(index: Natural) method, on our TypedList, such that it will retrieve the element of the list at said index.
  4. 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 ?

  1. 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 ?)
  2. 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!

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:

  1. 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.
  2. 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

  1. 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.
  2. 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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s