## 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

## Easy to use type classes in Scala

Scala is a pretty good functional programming language, but its type class syntax is pretty ugly to use. Thankfully, there is a pattern you can use to simplify the use of your type classes, making them almost as easy to use as regular inheritance based OOP.

Type classes are a very handy concept first pioneered in Haskell, which allows polymorphism like inheritance, but without requiring the foresight of inheritance. By that I mean that type class relationships between types can be defined for any type after that type has been defined, rather than during that type’s definition.

Below, I have the definition of a type class called depth.

```trait Depth[P[_]] {
def depth(self: P[_]): Int
}
```

This type class can be implemented for any type constructor like so:

```object Depth {
implicit object ListDepth extends Depth[List] {
def depth(self: List[_]) = x.size
}
}
```

The code above basically tells Scala how Depth is implemented for the type constructor List. This is all well and good, but when we go to use our type class…

```object Main extends App {
List(1,2,3).depth //won't compile, list does not have depth defined

def fn[T[_]: Depth](t: T[_]) = {
t.depth //Also doesn't work
implicitly[Depth[T]].depth(t) //yuck
}
}
```

things get very messy very quickly. Thankfully, with just a few tweaks, our typeclass can be as easy to use as regular polymorphism!

```trait Depth[P[_]] {
def depth(self: P[_]): Int

class Ops[T](self: P[T]) {
def depth = Depth.this.depth(self)
}
}

object Depth {
implicit object ListDepth extends Depth[List] {
def depth(self: List[_]) = x.size
}

//This implicit converts anything that has an implementation of Depth into the Depth.Ops class
implicit def implicits[T, P[T]](x: P[T])(implicit ev: Depth[P]) = new ev.Ops(x)
}
```

As you can see, we added a new def to our Depth companion object called implicits and a class named Ops to our Depth trait. We simplify the depth function by making it apply itself to the depth object it belongs to. The implicit def called implicits converts any object X that has an implementation of the Depth type class into a Depth#Ops object. This makes our syntax in main easy to use and much nicer looking:

```import Depth
import Depth._

object Main extends App {
List(1,2,3).depth //now this works just like if List inherited from Depth

def fn[T[_]: Depth](t: T[_]) = {
t.depth //So does this!
}
}
```

Type classes make certain code patterns much easier to deal with. For example, earlier today I had two different datastructures with similar methods I wanted to benchmark against each other. Problem is, they shared no inheritance, so under normal polymorphism I would have to either implement some kind of shared parentage or implement multiple near copies of the same benchmarking code. With typeclasses, there was a much easier third option. Implement a typeclass with the methods signatures I was going to use, and make both types implement that typeclass. Then I just needed to pass in a datastructure to the benchmark function and it would do the rest. Code gets reused and everyone is happy.

What are the downsides to the pattern above and type classes in general? They are:

• Type classes are terrible for documentation, since any and all implementations of the type class can be defined anywhere in your code.
• Method signature collisions between type classes implemented by a type can cause weird “method not defined” compiler errors.
• Generic syntax along with implicits definitions can be finicky, and sometimes it takes work to figure out why your implicit is not triggering.
• The implicit def that enhances the typeclass implementations must have a unique name. Thanks to type erasure, Scala can’t differentiate these methods solely on type signature. Collisions in the names of these methods will generate “method not defined” compiler errors.

All in all, typeclasses are a very nice and powerful tool for polymorphism in Scala!

edit: As Nullable has brought up, this can be done with implicit classes and view bounds in a more succint way:

```trait Depth[T] extends Any {
def depth: Int
}

object Depth {
implicit class ListDepth[T](val self: List[T]) extends AnyVal with Depth[List[T]] {
def depth = self.size
}
}

object Main extends App {
List(1,2,3).depth // 3

def fn[T <% Depth[T]](t: T) = t.depth //compiles
}
```

However, Depth is no longer useable as a type class, meaning implicitly goes out the window.
—-

This post was inspired by Scala – The Flying Sandwich Parts by eed3si9n

10 Comments

Filed under Scala

## 2.10 Performance

I’ve been reading up on all the great new stuff in Scala 2.10.0-RC3, and as always, one of the features mentioned is performance improvements. I was curious today what that meant for functional style work, so I wrote up a short microbenchmark to test it. I created a Sieve of Eratosthenes using streams, and a Sieve of Sundaram, both shown below:
Sieve of Eratosthenes –

```def eratosthenes(toNum: Int) = {
def sieveHelp(r: IndexedSeq[Int]): Stream[Int] = {
if(r.isEmpty)
Stream.empty
else
r.head #:: sieveHelp(r.tail.filterNot(_ % r.head == 0))
}
sieveHelp(2 +: (3 to toNum by 2))
}
```
Sieve of Sundaram –
```def sundaram(toNum: Int) = {
val n = (toNum - 2)/2
val nonPrimes = for (i <- 1 to n; j <- i to (n - i) / (2 * i + 1)) yield i+j+(2*i*j)
2 +:((1 to n) diff nonPrimes map (2*_+1))
}
```

The Sieve of Sundaram is run 120 times, finding all primes below 3,000,000. The Sieve of Eratosthenes is run 60 times and finds all primes below 75,000. The results for both are in the chart below: As you can see, the performance improvement for Sundaram are negligible, but the the performance of the Sieve of Eratosthenes is more than doubled! All in all, I’m looking forward to the release of 2.10 and further upgrades to the speed of the fastest and most flexible non-java jvm language.

For the source of my benchmark, go here: https://github.com/markehammons/2.10.0-RC3-Benchmark

9 Comments

Filed under Uncategorized