Dependent Types in Scala

After reading a post by Miles Sabin on StackOverflow about dependent types, and looking at some of the source of the Shapeless library, I thought I’d give dependent typing in Scala a shot myself. Dependent types are types that depend on a value. So far I’m focusing mainly on Π-types, which as Miles’ StackOverflow post says, are very similar to functions that take values and return types based on those values. I’ll start explaining how this works by analysing modified versions of the types Nat, Succ, Pred, and PredAux from Shapeless’ nat.scala.

Nat.scala in Shapeless describes natural numbers as a function of types. The two most important definitions in it are Nat and Succ, defined like so:

trait Nat

trait Succ[P <: Nat] extends Nat

object Nat { 
  trait _0 extends Nat
  implicit object _0 extends _0

  type _1 = Succ[_0]
  implicit val _1 = new _1 {}

  type _2 = Succ[Succ[_0]]
  implicit val _2 = new _2 {}
}

Nat is a trait indicating a natural number, and Succ is a subtype of it that takes a Nat as a type parameter. _0 is defined inside Nat’s companion object as an implicit singleton, and as a type it serves as the base of our set of Natural numbers. Succ is used to indicate a natural number that is one greater than Succ’s type parameter. Therefore, Succ[Succ[_0]] is the representation of 2 in this system.

Those familiar with Martin Odersky’s “Functional Programming Principles in Scala” course will recognize this as a form of Peano numbers. Of course, we are missing operations for our Nats, but we won’t define them as methods on our types, but rather as types themselves. Dependent types that is!

trait Pred[A <: Nat] {
  type Out <: Nat
}

trait PredAux[A <: Nat, B <: Nat]

object Pred {
  implicit def pred[A <: Nat, B <: Nat](implicit p: PredAux[A,B]) = new Pred[A] {     
    type Out = B
  }
}

object PredAux {
  implicit def pred[B <: Nat] = new PredAux[Succ[B],B] {}
}

Above is the definition of the dependent type Pred, which takes a Num and returns it’s predecessor as that number decremented by one. It is a type class, and it depends on another type class called PredAux that defines it’s behaviour. It’s used with the style implicitly[Pred[_2]], which returns a Pred trait with an out type of _1. But how does it go from an implicit definition that takes two generic parameters to determining the predecessor of our number? Lets start with PredAux to find the answer.

trait PredAux[A <: Nat, B <: Nat]

object PredAux {
  implicit def pred[B <: Nat] = new PredAux[Succ[B],B]
}

PredAux is a type class that takes two type parameters A and B. If you’re not familiar with type classes, when you pass a typeclass with type arguments to implicit, it searches for an implicit in the companion object that has the same type as the type passed into implicit. In this case, if I do implicitly[PredAux[_1, _0]], the compiler will use the implicit definition pred to instantiate our typeclass because the return type of pred is PredAux[Succ[B],B]. If I try implicitly[PredAux[_2,_0]], the compiler will complain about not being able to find an implicit value for the parameter, because there is no implicit definition in PredAux with a type of PredAux[Succ[Succ[_0]],_0].

So, how PredAux works is pretty easy to understand, but what about Pred?

trait Pred[A <: Nat] {
  type Out <: Nat
}

object Pred {
  implicit def pred[A <: Nat, B <: Nat](implicit p: PredAux[A,B]) = new Pred[A] {     
    type Out = B
  }
}

It all looks pretty simple, but what is with the type parameter B? When we use Pred, we want to pass it one type parameter, and have it work what the type of Out is. It turns out that the type B in our implicit definition pred does not need to be passed in. The compiler when given implicitly[Pred[_1]] will try to match on pred because it’s type is Pred[A]. So where does the type parameter B come from and how is it assigned to Out?

It turns out B will be calculated by the compiler thanks to the implicit evidence p we give our definition pred. Since the compiler knows type A is _1, which is Succ[_0], it can then infer that B is _0, since the implicit evidence p constrains what kind of relationship A and B can have. Likewise, the compiler will infer that B is _1 when A is _2. It will throw an error if A is _0, because _0 is not defined in terms of Succ.

So, if you haven’t noticed, Pred is a Π-type. It takes a type A =:= Succ[_ <: Num], and returns a type B that is type A’s predecessor. All in all though it’s a pretty underwhelming example of Π-types, so I constructed my own in order to better learn about how to create them in Scala…

trait Num

object Num {
  def apply[N <: Num](implicit n: N) = n

  def pred[T <: Num](implicit p: Pred[T]) = new Check[p.Out] {}
  def succ[T <: Num](implicit s: Succ[T]) = new Check[s.Out] {}
  def flatten[T <: Num](implicit flat: Flatten[T]) = new Check[flat.Out] {}
  def check[T <: Num](c: => Check[T]) {}


  trait _0 extends Num
  implicit object _0 extends _0

  type _1 = Up[_0]
  implicit object _1 extends _1

  type _2 = Up[Up[_0]]
  implicit object _2 extends _2
}

trait Up[N <: Num] extends Num

trait Down[N <: Num] extends Num

trait Pred[N <: Num] {
  type Out <: Num
}

trait PredAux[A <: Num, B <: Num]

object Pred {
  implicit def pred[A <: Num, B <: Num, C <: Num](implicit pred: PredAux[A,B], flat: Flatten[B]) = new Pred[A] {
    type Out = flat.Out
  }
}

object PredAux {
  implicit def pred[A <: Num] = new PredAux[A, Down[A]] {}
}

trait Succ[N <: Num] {
  type Out <: Num
}

trait SuccAux[A <: Num, B <: Num]

object Succ {
  implicit def succ[A <: Num, B <: Num](implicit succ: SuccAux[A,B], flat: Flatten[B]) = new Succ[A] {
    type Out = flat.Out
  }
}

object SuccAux {
  implicit def succ[A <: Num] = new SuccAux[A, Up[A]] {}
}

trait Flatten[T <: Num] {
  type Out <: Num
}

trait FlattenAux[A <: Num, B <: Num]

object Flatten {
  import Num._
  implicit def induct[A <: Num, B <: Num](implicit flatten: FlattenAux[A,B]) = new Flatten[A] {
    type Out = B
  }

  implicit def base = new Flatten[_0] {
    type Out = _0
  }
}

object FlattenAux {
  import Num._0

  //base case: when A in FlattenAux[A,B] is of the form C[_0], B is of the form C[_0]
  implicit def base[C[_ <: Num] <: Num] = new FlattenAux[C[_0], C[_0]] {}

  //inductive case
  implicit def induct[C[_ <: Num] <: Num,A <: Num, B <: Num](implicit flat: FlattenAux[A,B], red: Reduce[C[B]]) = {
    new FlattenAux[C[A], red.Out] {}
  }
}

trait Reduce[A <: Num] {
  type Out <: Num
}

object Reduce {
  implicit def reduce[A <: Num, R <: Num](implicit red: ReduceAux[A,R]) = new Reduce[A] {
    type Out = R
  }
}

trait ReduceAux[A <: Num, R <: Num]

object ReduceAux {
  import Num._0

  //if A in ReduceAux[A,B] is of the form Down[Up[C]], B == C
  implicit def reduce[C[_ <: Up[_]] <: Down[_], D[_ <: Num] <: Up[_], A <: Num] = new ReduceAux[C[D[A]], A] {}

  //if A in ReduceAux[A,B] is of the form Up[Down[C]], B == C
  implicit def reduce2[C[_ <: Down[_]] <: Up[_], D[_ <: Num] <: Down[_], A <: Num] = new ReduceAux[C[D[A]], A] {}

  //if A in ReduceAux[A,B] is of the form C[D[_]] and C == D, B == A
  implicit def reduce3[C[_ <: Num] <: Num, D[_ <: Num] <: Num, A <: Num](implicit ev: C[_] =:= D[_]) = {
    new ReduceAux[C[D[A]], C[D[A]]] {}
  }

  //if A in ReduceAux[A,B] is of the form C[_0], B == A
  implicit def reduce4[C[_ <: Num] <: Num] = new ReduceAux[C[_0],C[_0]] {}

}

trait Check[T]

I’ve made the following changes to the original shapeless code:

  • a new trait Num, which represents any number in the set of all integers
  • Succ has been renamed to Up
  • A new Π-type called Succ has been created. It returns the successor of the Num passed into it.
  • A new type called Down has been added. Down[_0] == -1
  • Both Succ and Pred are defined in terms of Flatten
  • Two new Π-types have been added, Reduce and Flatten

My new code allows for the definition of negative numbers by encasing _0 in any number of Downs. Pred has also been simplified in that it wraps the type passed in in a Down. Of course, that simplification wouldn’t make much sense to the type-system if that was all Pred did, since Down[Up[Up[_0]] is not Up[_0]. In order to deal with that issue, I added two new Π-types, Reduce and Flatten. Flatten, when given a Num type, returns a new type with all conflicting Ups and Downs removed. That means if I do implicitly[Flatten[Up[Down[Up[Down[_0]]]]]], Flatten.out will be the type _0. Reduce is used by flatten to look at the two highest first order type constructors, and sees if they cancel out. If we have a type A, and it is of the form Up[Down[B]] or Down[Up[B]], Reduce will return B. If A is of the form C[C[B]] or C[_0], where C is any first order type constructor, Reduce will return the input.

We can check that this code is working as expected with the check, succ, flatten, and pred methods in Num.

check[_2](succ[_1]) //does a compile time check that _2 is the successor of _1
check[_0](flatten[Up[Down[Up[Down[_0]]]]]) //does a compile time check that Up[Down[Up[Down[_0]]]] == _0 once the Flatten Π-type is done with it.
check[Down[_0]](pred[_0]) //does a compile time check that -1 is the predecessor of 0.
check[Down[Down[_0]]](pred[_0]) //doesn't compile, -2 is not the predecessor of 0.

I’ll go over how Flatten works in a later blogpost.

edit: If you decide to develop your own dependent types, the -Xlog-implicits compiler flag is very handy for debugging the expansion of your implicits.

Advertisements

Leave a comment

Filed under Dependent Types, Functional Programming, Scala

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 )

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s