Scala has a sophisticated type system that allows to catch many logic errors. Let's make it to good use.
For instance: we try to avoid getting a DivisionByZeroError. This would be doable if we had a type that represents numbers different from zero. Or we may want to zip two lists together only if we are guaranteed that they have the same length.
Dependent type systems allow to define types in term of values. We will not make this precise, but show some examples in the Scala type system.
Applications will include:
Note: in general, dependent type systems are associated with a proof system. The reason is that we may need to be able to help the compiler do its type inference.
For instance, say we have type NonZeroInt that represents integers that are not 0. We know that the function x => x^2 + 1 sends Int to NonZeroInt, but the compiler may not be able to infer this. Example of dependently-typed languages include:
Scala has some of the needed features, in particular objects can have type members, and two such types are the same exactly when they are the same members of the same value. This will be the basis for all our constructions.
We start with a few functions and types that are defined in the Scala prequel, since we will need to understand how they work.
Since we will need a few complex signatures in the sequel, a nice first step is exploiting the compiler to summon implicit instances and do some work for us.
In [ ]:
def implicitly[A](implicit a: A) = a
Let us check that this works as expected
In [ ]:
case class Foo(x: Int)
implicit val foo = Foo(5)
implicitly[Foo]
Can we use the same method to check whether some types are the same?
In [ ]:
class =:=[A, B]
implicit def equalTypeInstance[A] = new =:=[A, A]
We use this definition, together with implicitly, to check for type equality
In [ ]:
//# this does not compile
//# implicitly[Int =:= String]
implicitly[Int =:= Int]
It is a little annoying to work with stuff that does not compile. If we provide a dummy default value, we can turn this check into a value-level boolean.
In [ ]:
def type_==[A, B](implicit ev: A =:= B = null) = ev != null
In [ ]:
type_==[Int, Int]
In [ ]:
type_==[Int, String]
Great, next we do the same for subtyping
In [ ]:
class <:<[-A, +B]
implicit def subTypeInstance[A] = new <:<[A, A]
This variance trick is all that is needed to make this work, see:
In [ ]:
//# this does not compile
//# implicitly[Int <:< String]
implicitly[List[Int] <:< Seq[Int]]
In [ ]:
def type_<[A, B](implicit ev: A <:< B = null) = ev != null
In [ ]:
type_<[Int, String]
In [ ]:
type_<[List[String], Seq[String]]
It is not difficult to encode some types, and the relative operations, at the type level. We start with booleans
In [ ]:
sealed trait Bool
sealed trait True extends Bool
sealed trait False extends Bool
This is a start, but we do not have any operations yet. Let us do better
In [ ]:
sealed trait Bool {
type Not
}
sealed trait True extends Bool {
type Not = False
}
sealed trait False extends Bool {
type Not = True
}
In [ ]:
type_==[True, False#Not]
We can even encode the if operation:
In [ ]:
sealed trait Bool {
type Not
type If[T <: Up, F <: Up, Up] <: Up
}
sealed trait True extends Bool {
type Not = False
type If[T <: Up, F <: Up, Up] = T
}
sealed trait False extends Bool {
type Not = True
type If[T <: Up, F <: Up, Up] = F
}
Note that we have three parameters: Up is there to guarantee that the result of the operation is a supertype of both branch types.
We can then use If to define Not, and we will add some more operations as well
In [ ]:
sealed trait Bool {
type If[T <: Up, F <: Up, Up] <: Up
}
sealed trait True extends Bool {
type If[T <: Up, F <: Up, Up] = T
}
sealed trait False extends Bool {
type If[T <: Up, F <: Up, Up] = F
}
object Bool {
type &&[A <: Bool, B <: Bool] = A#If[B, False, Bool]
type || [A <: Bool, B <: Bool] = A#If[True, B, Bool]
type Not[A <: Bool] = A#If[False, True, Bool]
}
Let us check that everything works as expected
In [ ]:
import Bool._
type_==[True, Not[False]]
In [ ]:
implicitly[False =:= &&[True, False]]
implicitly[True =:= ||[True, False]]
We can use our type test function to convert Bool types to Boolean values
In [ ]:
def bool2val[A <: Bool]: Boolean = type_==[A, True]
In [ ]:
bool2val[True]
Ops... this does not work! The reason is that each function creates its own scope, and the implicit resolution happens there. This means that in the scope of bool2val the implicit for A =:= True is not found and the function always return false.
Let us summon the implicit instance in scope
In [ ]:
def bool2val[A <: Bool](implicit ev: A =:= True = null) = type_==[A, True]
In [ ]:
bool2val[True]
In [ ]:
bool2val[False]
Much better
We can construct naturals the Peano way
In [ ]:
sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat
and then define
In [ ]:
type _1 = Succ[_0]
and so on. Of course, we can add some operations too
In [ ]:
sealed trait Nat {
type IfZero[T <: Up, F <: Up, Up] <: Up
}
sealed trait _0 extends Nat {
type IfZero[T <: Up, F <: Up, Up] = T
}
sealed trait Succ[N <: Nat] extends Nat {
type IfZero[T <: Up, F <: Up, Up] = F
}
type _1 = Succ[_0]
We check that these work as expected
In [ ]:
type_==[_0#IfZero[True, False, Bool], True]
We can extend this to define, say, the precedessor function, which of course has to be defined so that Pred[_0] is _0
In [ ]:
sealed trait Nat {
type IfZero[T <: Up, F <: Up, Up] <: Up
type Pred <: Nat
}
sealed trait _0 extends Nat {
type IfZero[T <: Up, F <: Up, Up] = T
type Pred = _0
}
sealed trait Succ[N <: Nat] extends Nat {
type IfZero[T <: Up, F <: Up, Up] = F
type Pred = N
}
object Nat {
type Pred[N <: Nat] = N#Pred
}
type _1 = Succ[_0]
In [ ]:
import Nat._
type_==[_0, Pred[_1]]
In [ ]:
type_==[_1, Pred[_0]]
One would think this is enough to define addition recursively. Let's see
In [ ]:
object NatOps {
type Plus[A <: Nat, B <: Nat] = A#IfZero[B, Succ[Plus[Pred[A], B]], Nat]
}
The compiler will not allow recursive type definitions. We can work around this by adding one more operation to our Nat
In [ ]:
sealed trait Nat {
type IfZero[T <: Up, F <: Up, Up] <: Up
type Pred <: Nat
type Plus[B <: Nat] <: Nat
}
sealed trait _0 extends Nat {
type IfZero[T <: Up, F <: Up, Up] = T
type Pred = _0
type Plus[B <: Nat] = B
}
sealed trait Succ[N <: Nat] extends Nat {
type IfZero[T <: Up, F <: Up, Up] = F
type Pred = N
type Plus[B <: Nat] = Succ[N#Plus[B]]
}
object Nat {
type Pred[N <: Nat] = N#Pred
type Plus[A <: Nat, B <: Nat] = A#Plus[B]
}
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
Let's see this in action!
In [ ]:
import Nat._
type_==[Plus[_2, _2], _4]
In [ ]:
type_==[Plus[_2, _2], _3]
As before, we can convert these types to values.
In [ ]:
class NatConverter[N <: Nat](val n: Int)
implicit val zeroConverter: NatConverter[_0] = new NatConverter(0)
implicit def succConverter[N <: Nat](implicit ev: NatConverter[N]): NatConverter[Succ[N]] = new NatConverter(ev.n + 1)
def nat2value[N <: Nat](implicit ev: NatConverter[N]) = ev.n
In [ ]:
nat2value[_2]
Well, we now will want to add multiplication as well. But, just as above, we will need to modify our definition of Nat. What if, instead, we add a general function to do recursion?
To do so, we will define a FoldR operation on Nat. We first need the type-level analogue of a function (A, B) => B. Such a function is equivalent to the trait
In [ ]:
trait FoldOp[A, B] {
def apply(a: A, b: B): B
}
We will then define the type-level analogue
In [ ]:
trait Fold[A, B] {
type Apply[X <: A, Y <: B] <: B
}
The FoldR operation can then be defined on Nat as follows
In [ ]:
sealed trait Nat {
type Pred <: Nat
type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] <: Up
}
sealed trait _0 extends Nat {
type Pred = _0
type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] = Init
}
sealed trait Succ[N <: Nat] extends Nat {
type Pred = N
type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] = Op#Apply[Succ[N], N#FoldR[Init, Op, Up]]
}
Phew... that was quite complex! Anyway, we can now define a few operations
In [ ]:
object NatOps {
type Incr = Fold[Nat, Nat] {
type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]
}
type Plus[A <: Nat, B <: Nat] = A#FoldR[B, Incr, Nat]
}
In [ ]:
class NatConverter[N <: Nat](val n: Int)
implicit val zeroConverter: NatConverter[_0] = new NatConverter(0)
implicit def succConverter[N <: Nat](implicit ev: NatConverter[N]): NatConverter[Succ[N]] = new NatConverter(ev.n + 1)
def nat2value[N <: Nat](implicit ev: NatConverter[N]) = ev.n
In [ ]:
import NatOps._
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]
type _6 = Succ[_5]
type _7 = Succ[_6]
type _8 = Succ[_7]
type_==[Plus[_3, _4], _7]
By the same method we can add multiplication, and (bounded) difference
In [ ]:
object NatOps {
type Incr = Fold[Nat, Nat] {
type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]
}
type Plus[A <: Nat, B <: Nat] = A#FoldR[B, Incr, Nat]
type Sum[B <: Nat] = Fold[Nat, Nat] {
type Apply[N <: Nat, Acc <: Nat] = Plus[Acc, B]
}
type Times[A <: Nat, B <: Nat] = A#FoldR[_0, Sum[B], Nat]
type Decr = Fold[Nat, Nat] {
type Apply[N <: Nat, Acc <: Nat] = Acc#Pred
}
type Minus[A <: Nat, B <: Nat] = B#FoldR[A, Decr, Nat]
}
In [ ]:
import NatOps._
type_==[Plus[_2, Times[_2, _3]], _8]
In [ ]:
type_==[Minus[_5, _3], _2]
In [ ]:
type_==[Minus[_3, _5], _0]
In fact, we can define the IfZero operations as well, and use that to implement comparison
In [ ]:
object MoreNatOps {
type NonZero[Up, F <: Up] = Fold[Nat, Up] {
type Apply[N <: Nat, Acc <: Up] = F
}
type IfZero[A <: Nat, T <: Up, F <: Up, Up] = A#FoldR[T, NonZero[Up, F], Up]
type Pred[N <: Nat] = N#Pred
type Leq[A <: Nat, B <: Nat] = IfZero[Minus[A, B], True, False, Bool]
type Less[A <: Nat, B <: Nat] = Leq[Succ[A], B]
}
In [ ]:
import MoreNatOps._
type_==[IfZero[_0, True, False, Bool], True]
In [ ]:
type_==[IfZero[_3, True, False, Bool], False]
In [ ]:
type_==[Succ[Pred[_3]], _3]
In [ ]:
bool2val[_3 Leq _4]
In [ ]:
bool2val[_4 Leq _3]
Notice that we have never used N in the FoldR operation. We could use that to define, for instance, the factorial, but we will stop here
Scala is not known to be a dependently-typed language, but has a few features that allow us to simulate some structures typical of languages with dependent types, such as:
Let us see some example in action
The poster child for dependent types are range types and fixed-length lists. We shall start from the latter.
We start by recalling the usual definition of List
In [ ]:
sealed trait List[+A] {
def ::[B >: A](b: B): List[B] = Cons[B](b, this)
def head: A
def tail: List[A]
}
case object Nil extends List[Nothing] {
def head = sys.error("empty list")
def tail = sys.error("empty list")
}
case class Cons[A](val head: A, val tail: List[A]) extends List[A]
We can use it as customary
In [ ]:
val list = 1 :: 2 :: 3 :: 4 :: Nil
In [ ]:
list.tail
Of course, this definition is unsafe, as we cannot take the head or tail of an empty list. We could remove head and tail from the List interface, leaving them as operation on Cons. But we would not fare much better: the compiler does not keep track of lengths, hence we have no way to know statically whether we are dealing with a List or a Cons.
Let us parametrize lists by their length, which is a natural number
In [ ]:
sealed trait NList[N <: Nat, +A] {
def ::[B >: A](b: B) = NCons[N, B](b, this)
}
case object NNil extends NList[_0, Nothing]
case class NCons[N <: Nat, A](val head: A, val tail: NList[N, A]) extends NList[Succ[N], A]
In [ ]:
val nlist: NCons[_2, Int] = 1 :: 2 :: 3 :: NNil
In [ ]:
nlist.tail
In [ ]:
%type nlist.tail
In [ ]:
nlist.tail.tail
Too bad! The compiler keeps track of the length, but does not yet know that when we have a list of positive length, we can keep taking the tail. Let us try to write an append operation
In [ ]:
def append[M <: Nat, N <: Nat, A](xs: NList[M, A], ys: NList[N, A]): NList[Plus[M, N], A] = xs match {
case NNil => ys
case NCons(h, t) => h :: append(t, ys)
}
Looks like the naive definition we used is no good at all. The compiler is not able to prove much about our natural numbers.
We will try a different approach: wrap an unsafe data structure and only provide operations when we know they can be carried out
In [ ]:
class Sized[N <: Nat, A](underlying: Seq[A]) {
def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])
}
In [ ]:
val seq = new Sized[_3, Int](List(1, 2, 3))
seq[_1]
In [ ]:
seq[_4]
We still have the problem that the following compiles, and fails at runtime
In [ ]:
val seq1 = new Sized[_8, Int](List(1, 2, 3))
seq1[_5]
Symmetrically
In [ ]:
val seq2 = new Sized[_3, Int](List(1, 2, 3, 4, 5))
seq2[_3]
To avoid this problem, we use a package-private constructor and we expose a safe API
In [ ]:
class Sized[N <: Nat, A]private(underlying: Seq[A]) {
def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])
}
object Sized {
def sized[N <: Nat, A](xs: Seq[A])(implicit ev: NatConverter[N]): Option[Sized[N, A]] =
if (xs.length == nat2value[N]) Some(new Sized(xs)) else None
}
In [ ]:
import Sized._
val Some(s) = sized[_3, Int](List(1, 2, 3))
In [ ]:
sized[_8, Int](List(1, 2, 3))
In [ ]:
new Sized[_8, Int](List(1, 2, 3))
In [ ]:
s[_2]
We can also add some other convenience methods. In all cases, we ask the compiler for a check that what we are doing is well-typed. For simplicity, we omit variance in the A parameter
In [ ]:
class Sized[N <: Nat, A]private(val underlying: Seq[A])(implicit ev: NatConverter[N]) {
def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])
def +:(x: A)(implicit ev: NatConverter[Succ[N]]) = new Sized[Succ[N], A](x +: underlying)
def :+(x: A)(implicit ev: NatConverter[Succ[N]]) = new Sized[Succ[N], A](underlying :+ x)
def ++[M <: Nat](xs: Sized[M, A])(implicit ev: NatConverter[Plus[N, M]]) = new Sized[Plus[N, M], A](underlying ++ xs.underlying)
def head(implicit ev: Less[_0, N] =:= True) = underlying.head
def tail(implicit ev: Less[_0, N] =:= True, ev1: NatConverter[Pred[N]]) = new Sized[Pred[N], A](underlying.tail)
override def toString = s"Sized[${ nat2value[N] }]: ${ underlying }"
}
object Sized {
def sized[N <: Nat, A](xs: Seq[A])(implicit ev: NatConverter[N]): Option[Sized[N, A]] =
if (xs.length == nat2value[N]) Some(new Sized(xs)) else None
def single[A](x: A) = new Sized[_1, A](List(x))
def SNil[A] = new Sized[_0, A](Seq.empty[A])
}
In [ ]:
import Sized._
val Some(s) = sized[_3, Int](List(1, 2, 3))
In [ ]:
s :+ 5
In [ ]:
s ++ s
In [ ]:
s.head
In [ ]:
s.tail
So far, everything is going on as expected. Will the compiler prevent us to take too many tails?
In [ ]:
s.tail.tail.tail.tail
Some more operations show that this is quite a simple to use data structure
In [ ]:
single(1) :+ 2 :+ 3
In [ ]:
1 +: 2 +: 3 +: SNil[Int]
Another nice example of type-level encoding is to use Nat to define classes of integers modulo N, and implement their operations in a type-safe way.
We will implement modular reduction for a natural N greater than _0.
In [ ]:
type IsLeq[A <: Nat, B <: Nat] = Leq[A, B] =:= True
In [ ]:
class Mod[N <: Nat](x: Int)(implicit ev: _1 IsLeq N, ev1: NatConverter[N]) {
lazy val n = x % nat2value[N]
def +(y: Mod[N]) = new Mod[N](n + y.n)
def -(y: Mod[N]) = new Mod[N](n - y.n)
def *(y: Mod[N]) = new Mod[N](n * y.n)
override def toString = s"$n mod ${ nat2value[N] }"
}
object Mod {
def apply[N <: Nat](x: Int)(implicit ev: _1 IsLeq N, ev1: NatConverter[N]) = new Mod[N](x)
}
In [ ]:
val a = Mod[_4](10)
In [ ]:
a * a
Notice that every operation is defined in terms of the lazy val n, which is a reduced representative of the class of x modulo N. This guarantees that we can keep performing operations without overflowing
In [ ]:
def power[N <: Nat](x: Mod[N], y: Int): Mod[N] = if (y == 1) x else x * power(x, y - 1)
In [ ]:
val b = Mod[_7](6)
In [ ]:
power(b, 1000)
In [ ]:
b + Mod[_5](3)
Another neat application of dependent types allows us to choose one of two branches based on which one compiles. Let us define a trait
In [ ]:
trait Application[A, F, G]{
type Out
def apply(a: A, f: F, g: G): Out
}
This represent the application of either the function f or g to the value a, with a result of type Out. None of the types is determined yet. We now define our choice method
In [ ]:
def choose[A, F, G](a: A, f: F, g: G)(implicit app: Application[A, F, G]): app.Out = app(a, f, g)
This does nothing but let the compiler summon an appropriate implicit. Notice that the return type is app.Out, hence it depends on the implicit chosen.
We will need to provide suitable implicits to make the above work. The trick is that we will provide two implicits: the first one will need F to be a function of A, and the second one will require G to be a function of A. Whichever compiles will be chosen
In [ ]:
implicit def applyf[A, B, G] = new Application[A, A => B, G] {
type Out = B
def apply(a: A, f: A => B, g: G) = f(a)
}
implicit def applyg[A, B, F] = new Application[A, F, A => B] {
type Out = B
def apply(a: A, f: F, g: A => B) = g(a)
}
See it in action:
In [ ]:
choose(3, { x: Int => x * x }, { x: String => "hello " + x })
In [ ]:
choose("world", { x: Int => x * x }, { x: String => "hello " + x })
As a final example, we will build a balanced binary tree type, so that unbalanced trees will be a compile time error.
Since binary trees with a number of leaves that is not a power of two cannot be perfectly balanced, we will require that for each subtree, starting from the root:
We will do so by adding a type member that represents the tree height, and providing tree constructors only when we have implicits that certify that the height conditions are satisfied
In [ ]:
sealed trait Tree[+T]{
type N <: Nat
}
object Leaf extends Tree[Nothing]{
type N = _0
}
trait Branch[T] extends Tree[T]{
def value: T
def left: Tree[T]
def right: Tree[T]
}
In [ ]:
object Branch {
type HBranch[T, N0 <: Nat] = Branch[T] { type N = N0 }
def apply[T, D <: Nat](value0: T, left0: Tree[T], right0: Tree[T])
(implicit ev: right0.N IsLeq left0.N, ev1: left0.N IsLeq Succ[right0.N]): HBranch[T, Succ[left0.N]] =
new Branch[T] {
val value = value0
val left = left0
val right = right0
type N = Succ[left0.N]
}
}
In [ ]:
val b1 = Branch(1, Leaf, Leaf) //# N = 1
val b2 = Branch(2, Leaf, Leaf) //# N = 1
val b3 = Branch(3, b1, Leaf) //# N = 2
val b4 = Branch(4, b2, b1) //# N = 2
Let us check that the height are as expected
In [ ]:
type_==[b1.N, _1]
In [ ]:
type_==[b3.N, _2]
In [ ]:
val b5 = Branch(5, b3, b4)
Look what happens as soon as we try to define unbalanced trees..
In [ ]:
Branch(5, b1, b3) //# left branch too small
In [ ]:
Branch(5, b4, Leaf) //# left branch too high
In [ ]:
Branch(5, b5, b1) //# left branch too high