Let's assume that we have a list with an even number of elements. By knowing that the length is even we could do various things like extracting pairs. Odd length is not very suitable for this… no shit Sherlock!

To make this happen we first need boolean values in the type system to represent that a proposition is actually true and we need to be able to negate them.

sealed trait Bool {

type Not <: Bool

}

sealed trait True extends Bool {

type Not = False

}

sealed trait False extends Bool {

type Not = True

}

In the next step we have to extend our type-level natural numbers. Let's give them a predecessor and a property that indicates if a number is even.

sealed trait Nat {

type IsEven <: Bool

type Pred <: Nat

}

sealed trait Z extends Nat {

type IsEven = True

type Pred = Z

}

sealed trait S[A <: Nat] extends Nat {

type IsEven = A#IsEven#Not

type Pred = A

}

To make it a little nicer to read and write we will add a witness that represents that a natural number is even we check this with the

`=:=`

type constraint which witnesses that two types are equal.

sealed trait Even[A <: Nat]

object Even {

implicit def isEven[A <: Nat](implicit e: A#IsEven =:= True): Even[A] =

new Even[A]{}

}

Now the fun part. We now start building our list with a getPairs method that only works on lists with an even length. Here is our interface for this NList:

sealed trait NList[A <: Nat, +B] {

type Length = A

def getPairs(implicit e: Even[Length]): List[(B, B)]

def head: B

def tail: NList[Length#Pred, B]

}

The first case again is trivial, we are dealing with an empty list, the only thing that we can extract is an empty list.

case object NNil extends NList[Z, Nothing] {

def getPairs(implicit e: Even[Length]): List[(Nothing, Nothing)] =

Nil

def head = sys.error("empty list")

def tail = sys.error("empty list")

}

Now this one is a little more tricky, we might know that a natural number

`A`

is even but what the typesystem does not know if `A#Pred#Pred`

is also even when we call `getPairs`

recursively. We now need to to create a witness that `A#Pred#Pred`

is even when `A`

is even. We can do this with another method that generates a witness when you hand it the witness for `A`

's evenness, let's call that method `predPredEven`

.

sealed case class NCons[A <: Nat, B](h: B, t: NList[A, B])

extends NList[S[A], B] {

private def predPredEven[A](e: Even[Length]): Even[Length#Pred#Pred] =

new Even[Length#Pred#Pred]{}

def getPairs(implicit e: Even[Length]): List[(B, B)] =

(head, tail.head) :: tail.tail.getPairs(predPredEven(e))

def head: B = h

def tail: NList[Length#Pred, B] = t

}

That's all. How does this look when we put it into action?

scala> val lo = NCons(1, NNil)

lo: nlist.NCons[nlist.Z,Int] = NCons(1,NNil)

scala> le.getPairs

res0: List[(Int, Int)] = List((1,2))

scala> NNil.getPairs

res1: List[(Nothing, Nothing)] = List()

scala> lo.getPairs

:12: error: could not find implicit value for parameter e: nlist.Even[lo.Length]

lo.getPairs

^

Very nice!

`getPairs`

only works on lists with an even length, otherwise we get a compile error. Once again: If you want to play with this code check out this gist.
In future blogposts I'd like to show you how a language that bears these techniques in mind handles these problems.