Mittwoch, 24. August 2011

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)] =
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]

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.

Montag, 22. August 2011

A Taste of Dependent Types in Scala

One thing starts to cross my way very frequently is dependent typing. While I'm not an expert on this topic I found some very interesting things in various papers that I would like to be able to do in Scala. Dependent types help to verify that your program does what it's supposed to do by proving theorems.
Since Scala is not dependently typed we need to become a little tricky, but let's give it a try.

Think about the type signature of the following method called zap (which stands for zip-apply):

def zap[A, B](l: List[A], fs: List[A => B]): List[B]

By looking at the signature it should become obvious what the method does. You have a list l that provides elements of type A and a list fs that provides a function from A to B for each element in l. Lets look at the implementation:

def zap[A, B](l: List[A], fs: List[A => B]): List[B] =
(l, fs) match {
case (_, Nil) | (Nil, _) => Nil
case (a :: as, b :: bs) => b(a) :: zap(as, bs)

That's a pretty straight forward example, but there is a problem with this code. What if we do provide lists with different length? In one case we would not execute some functions in the other case we would lose data. So what can we do? We could throw an exception but that's already to late, our program is already in a state where things don't make sense anymore, we have to avoid this situation at all and the best thing to achieve this is that such code does not compile at all.

In a dependently typed language we could create a list that encodes it's length within the type of the list itself and write zap in a way so that it would only accept lists of the same length. But since we are not in a dependently typed language we cannot do that, this concludes this blogpost, see you in another episode… ok, just kidding. We actually CAN do that in Scala. Here is how:

The first thing we need is: natural numbers in the type system to encode the length of our list. That is easy:

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

Z is our zero here and S[A <: Nat] is the successor of the natural number A, so we can create the natural numbers recursively: Z == 0, S[Z] == 1, S[S[Z]] == 2 etc.

Now let's start with the fun part, the list itself.

The first thing we need is the trait for our NList.

trait NList[A <: Nat, +B] {
type Length = A
def zap[C](l: NList[Length, B => C]): NList[Length, C]

We can now see that the type of zap enforces that the both lists need to have the same length A. We can now create our first case where we are zapping two lists of length 0 (or Z). The implementation is rather trivial.

case object NNil extends NList[Z, Nothing] {
def zap[A](l: NList[Length, Nothing => A]): NNil.type =

The next case is not as simple (if someone has a better idea of how to implement this, I would love to see it. Please drop a comment).

case class NCons[A <: Nat, B](head: B, tail: NList[A, B])
extends NList[S[A], B] {
def zap[C](l: NList[Length, B => C]): NList[Length, C] =
l match {
case NCons(f, fs) =>
NCons(f(head), tail zap fs)

We can see that our NCons is actually a NList that is one element longer
than it's tail which has length A, the pattern match inside our zap method only has to handle the cons case since the type signature does not allow anything else.

Now let's put that little bugger to the test:

First lets define some NLists

scala> val l1 = NCons(1, NCons(2, NCons(3, NNil)))
scala> val l2 = NCons(1, NCons(2, NNil))
scala> val f = (_: Int) + 1
scala> val f1 = NCons(f, NCons(f, NCons(f, NNil)))
scala> val f2 = NCons(f, NCons(f, NNil))

Zapping lists with the same length:

scala> l1 zap f1
res1: nlist.NList[l1.Length,Int] = NCons(2,NCons(3,NCons(4,NNil)))

scala> l2 zap f2
res2: nlist.NList[l2.Length,Int] = NCons(2,NCons(3,NNil))

This works just fine, now lets see what happens if we zap two lists with a different length:

scala> l1 zap f2
:14: error: type mismatch;
found : nlist.NCons[nlist.S[nlist.Z],Int => Int]
required: nlist.NList[l1.Length,Int => ?]
l1 zap f2

Exactly what we wanted! This code does not even compile since it doesn't make any sense.
This is a very basic example of what we can do with the Scala type system. Stay tuned for more!

If you would like to play around with the code check out my gist