More Fun with Scala "Dependent" Types

In my last post I wrote about lists that encode their length within their type and the possibilities that gives us to ensure correctness of our code. In this post I want to expand these ideas.

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.