Pagini
Workshops
Parteneri
The live demo you saw on Friday was there just so you can see what Scala's type system inferrer can do.
If less than 100% of that entire demo code made sense, it's absolutely fine. We'll go at great length here to make everything click.
At the actual demo, I followed the ideas from this quicksort article with some modifications.
For this explanation I'll cover my own mergesort version (instead of quicksort) which seems a bit easier and more gradual to build.
So what do we want?
We want to sort types (instead of values), at compile time.
Of course, nobody in their right mind would want to do that for any purely practical reason, but hey:
OK, so we're crazy and we want to make the compiler sort types by itself. Let's do this.
What we first need is an axiomatic definition of natural numbers as types, so we want to be able to define type _0
, type _1
etc as analogues to regular values.
Well we can't define all natural numbers, since there's quite a few of them, it would take us a while.
But we can define them in terms of their succession:
trait Nat class _0 extends Nat class Succ[A <: Nat] extends Nat
So in 3 lines of code we defined all natural numbers, as every number has a unique successor. In our object with the main method we can now define some type aliases:
object TypeDemo { type _1 = Succ[_0] type _2 = Succ[_1] // = Succ[Succ[_0]] type _3 = Succ[_2] // = Succ[Succ[Succ[_0]]] ... }
OK, that was easy. Now in order to be able to sort anything, we need to be able to compare things.
No Booleans here, because we just said goodbye to regular values. We'll declare the less-than relationship as a type:
trait <[A <: Nat, B <: Nat]
And of course we used the <
name, because Scala allows us to.
Important thing: _0 < _1
, which is sugar for <[_0, _1]
, is a type, not an expression.
Again, we want to define the inequality in an axiomatic way.
First of all, we know that 0 < succ(x)
for any natural x.
Secondly, for any two numbers x and y, succ(x) < succ(y)
if and only if x < y
.
For the Scala compiler, the first axiom means finding the type _0 < Succ[Something]
, where Something <: Nat
.
The second axiom means the compiler has to work. The intuitive mechanism should work like this. Let me just write
val x: _2 < _4 = ...
When the compiler sees the type _2 < _4
, it should work out the following:
Succ[_1] < Succ[_3]
by the names I've given to the _2
and the _4
types!Succ[_1] < Succ[_3]
exist?Succ[_1] < Succ[_3]
exists if _1 < _3
exists. OK.Succ[_0] < Succ[_2]
!Succ[_0] < Succ[_2]
exist?Succ[_0] < Succ[_2]
exists if _0 < _2
exists. OK._0 < Succ[_1]
!_0 < Succ[_1]
exist?_0 < _2
exists,_1 < _3
exists,_2 < _4
exists!
So the compiler infers that the type <[_2, _4]
(or _2 < _4
in sugar mode) exists, which is the same as us saying 2 < 4.
How does the compiler know how to look for axioms?
Through implicits.
We'll declare a companion for the <
trait as follows:
object < { implicit def ltbasic[B <: Nat]: <[_0, Succ[B]] = new <[_0, Succ[B]] {} }
in which this implicit method says to the compiler: hey, if you ever need an implicit value of type <[_0, Succ[B]]
for any type B
which is a natural, then let me give you an instance of the <[_0, Succ[B]]
type. We're not really concerned about the actual instance returned by the method - the compiler only relies on the fact that it exists.
So if I add an apply method to the companion:
def apply[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[A, B] = lt
and I say
val x = <[_0, _2]
the compiler fires up:
<
with the types _0
and _2
_0, _2
] or <[_0, Succ[_1]]
<[_0, Succ[_1]]
- hey implicit, when the program runs, I'll call you for this one!
So for us humans, the compiler just chose the axiom that 0 < succ(x)
for any x.
Let's add the other axiom, in the form of another implicit:
implicit def inductive[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[Succ[A], Succ[B]] = new <[Succ[A], Succ[B]] {}
which says: hey compiler, if you ever need an instance of type <[Succ[A], Succ[B]]
, just let me know; give me a value of type <[A, B]
and I'll compute an instance of <[Succ[A], Succ[B]]
for you.
So if I, programmer, say
val x = <[_1, _2]
the compiler fires up:
_1
and _2
.<[_1, _2]
or <[Succ[_0], Succ[_1]]
.<[Succ[_0], Succ[_1]]
, it's called inductive
.inductive
, when the program runs, I'll call you for this one!inductive
says: no problem boss, just give me an instance of <[_0, _1]
when you need me and I'll do that for you.<[_0, _1]
. basic
that does just that - hey basic
, when the program runs, I'll need you to give me an instance of <[_0, _1]
!basic
says: no problem, boss.basic
and inductive
said OK:basic
gives me the instance of <[_0, _1]
then I'll pass it to inductive
inductive
will give me an instance of <[_1, _2]
then I'll pass it to apply
Finally, I hope we're good. The comparison code looks like this:
trait <[A <: Nat, B <: Nat] object < { def apply[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[A, B] = lt implicit def ltbasic[B <: Nat]: <[_0, Succ[B]] = new <[_0, Succ[B]] {} implicit def inductive[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[Succ[A], Succ[B]] = new <[Succ[A], Succ[B]] {} }
and I'll finally be able to write
val x = <[_1, _2]
but instead if I try
val x = <[_2, _1]
smart compiler smacks me: could not find implicit value for parameter lt: <[_2, _1]
which is its gentle way of saying: “wtf, there's no such thing as _2 < _1, you crazy? I'm not compiling that piece of sh for you.”
We went so very granular in understanding the 5 lines of the <
definition above because this principle is at the core of the entire thing.
If you went through this and feel you got it, that's awesome. You are awesome.
You now understand how the compiler looks for implicit values and how we want exploit this mechanism with the meaning of finding mathematical axioms.
Shamelessly copying most of the stuff from the strict <
trait:
trait <=[A <: Nat, B <: Nat] object <= { def apply[A <: Nat, B <: Nat](implicit lte: <=[A, B]): <=[A, B] = lte implicit def basic[B <: Nat]: <=[_0, B] = new <=[_0, B] {} implicit def inductive[A <: Nat, B <: Nat](implicit lt: <=[A, B]): <=[Succ[A], Succ[B]] = new <=[Succ[A], Succ[B]] {} }
which has a slightly different basic axiom in that _0
is less than or equal to B
for any natural B
.
You should be able to easily read the other axiom with what you've learned so far.
Ok, cool. We defined natural numbers and a type-level comparison method.
Now in order to sort anything, we need a definition of a type-level list, which now “stores” types instead of values.
We'll define a list as
trait HList class HNil extends HList class ::[H <: Nat, T <: HList] extends HList
while again using the nice ::
name for the “cons” type, so we can later easily say H :: T
as sugar for ::[H, T]
.
Well, good. We have numbers, comparison and lists. We now need the algorithm.
You know the algorithm, but just a quick recap:
We'll do this in three parts: splitting, merging and actual sorting.
Judging by most of the code you've written so far, all your operations are composed of functions.
You've kept track so far, so you know this is unlike most code. Instead of functions, we'll use types.
The Split
type will look something like this:
trait Split[L <: HList] { type Left <: HList type Right <: HList }
Now this is a tiny bit different than comparing numbers, since this trait now “stores” types.
They will be the “results” of our computation, or rather, the compiler's computation.
As before, we'll add a companion to Split
, now with a small twist:
object Split { type Aux[HL <: HList, L <: HList, R <: HList] = Split[HL] { type Left = L type Right = R } }
Just for the sake of not expanding this code more than it's worth, read the above as the compiler would, as follows: “whenever someone gives me an instance of Aux[HL, L, R]
, I'll actually think of it as a Split[HL]
; in it, I'll store the Left
and Right
type members as L
and R
, respectively.”
Good. Now the axioms. What, you thought you were done with axioms?
One basic case is splitting the empty list, which is dead easy:
implicit def basic: Aux[HNil, HNil, HNil] = new Split[HNil] { type Left = HNil type Right = HNil }
Now look at the actual value I'm returning - I declare I'm returning an Aux
, but I'm returning a Split
with the exact Left = HNil, Right = HNil
match. I do that because
Left
and Right
and they have to match - otherwise the compiler's type equalizer will failSplit[HNil]
instance I'm returningWe'll use this principle throughout the entire mergesort algorithm.
Back to axioms. Another basic case is splitting a one-element list:
implicit def basic2[H <: Nat]: Aux[H :: HNil, H :: HNil, HNil] = new Split[H :: HNil] { type Left = H :: HNil type Right = HNil }
which keeps the one element in the Left side of the split.
OK, now the hard one. What should happen for a list with more than one element?
The trick here is not to split the list in half, at its half. That's a bit complicated.
By the definition of a list with more than one element, it has at least two elements.
So just put one in the Left side, one in the Right side, and split the rest recursively.
So axiomatically (in an ad-hoc invented language) we could say something like
split(HNil) = { Left = HNil, Right = HNil } split(H :: HNil) = { Left = H :: HNil, Right = HNil } split(H :: HH :: T) = { Left = H :: split(T).Left, Right = HH :: split(T).Right }
Hopefully the above code makes sense, as a condensed version of the above explanation.
We already have the first two axioms. The third, rewritten in Scala, looks like this:
implicit def inductive[H <: Nat, HH <: Nat, T <: HList] (implicit split: Split[T]) : Aux[H :: HH :: T, H :: split.Left, HH :: split.Right] = new Split[H :: HH :: T] { type Left = H :: split.Left type Right = HH :: split.Right }
and finally, an apply method:
def apply[L <: HList](implicit split: Split[L]): Aux[L, split.Left, split.Right] = new Split[L] { type Left = split.Left type Right = split.Right }
Try to apply the “hey implicit” logic we described in the number comparison, here. Example: Split[_0 :: _1 :: _2 :: HNil]
:
inductive
is the only one which returns a Split[_0 :: _1 :: Something]. Hey inductive
…inductive
: ok boss, give me a Split[_2 :: HNil] and I'll do whatever you need.basic2
is the only implicit which gives me a Split[_2 :: HNil]. Hey basic2
…basic2
: ok boss.Split[_2 :: HNil] { Left = _2 :: HNil, Right = HNil }
from basic2
, now going back toSplit[_0 :: _1 :: _2 :: HNil] { Left = _0 :: _2 :: HNil, Right = _1 :: HNil }
from inductive
.
By now you should be pretty familiar with the logic we (and the compiler) follow with implicits and axioms.
We'll go a tiny bit faster with the merge.
The merge “operation” will be, as before, a trait
trait Merge[LA <: HList, LB <: HList] extends HList { type Out <: HList }
which has two lists and a “result” type. Its companion has an auxiliary type which follows a similar logic as Split, for the compiler's sake:
object Merge { type Aux[LA <: HList, LB <: HList, R <: HList] = Merge[LA, LB] { type Out = R } }
Now the axioms.
First of all, any L
merged with HNil
will give us exactly L
.
Problem is, Merge[L, HNil]
is different from Merge[HNil, L]
, so we'll write two axioms:
implicit def basicleft[LA <: HList]: Aux[HNil, LA, LA] = new Merge[HNil, LA] { type Out = LA } implicit def basicright[LA <: HList]: Aux[LA, HNil, LA] = new Merge[LA, HNil] { type Out = LA }
Now the inductive ones. Both arguments are non-empty lists, so we can write them as HA :: TA
and HB :: TB
.
There are two options:
merge(HA :: TA, HB :: TB) = HA :: merge(TA, HB :: TB) if HA ⇐ HB
(forgive the ⇐, it's less than or equal - the wiki doesn't help me)
OR
merge(HA :: TA, HB :: TB) = HB :: merge(HA :: TA, TB) if HB < HA
Now those <
and ⇐
types may come in handy!
implicit def inductivelte[HA <: Nat, TA <: HList, HB <: Nat, TB <: HList] (implicit merged: Merge[TA, HB :: TB], lte: HA <= HB) : Aux[HA :: TA, HB :: TB, HA :: merged.Out] = new Merge[HA :: TA, HB :: TB] { type Out = HA :: merged.Out } implicit def inductiveg[HA <: Nat, TA <: HList, HB <: Nat, TB <: HList] (implicit merged: Merge[HA :: TA, TB], g: HB < HA) : Aux[HA :: TA, HB :: TB, HB :: merged.Out] = new Merge[HA :: TA, HB :: TB] { type Out = HB :: merged.Out }
And an apply method:
def apply[LA <: HList, LB <: HList](implicit merged: Merge[LA, LB]) : Aux[LA, LB, merged.Out] = new Merge[LA, LB] { type Out = merged.Out }
Try to follow the “hey implicit” logic on your own this time. For example: Merge[_0 :: _3 :: HNil, _1 :: _2 :: HNil]
.
We're here. The epic finale.
No surprises so far:
trait Sorted[L <: HList] extends HList { type Out <: HList } object Sorted { type Aux[L <: HList, S <: HList] = Sorted[L] { type Out = S } }
Basic axioms say sorting an empty or a one-element list will give the same list:
implicit def basicnil: Aux[HNil, HNil] = new Sorted[HNil] { type Out = HNil } implicit def basicone[H <: Nat]: Aux[H :: HNil, H :: HNil] = new Sorted[H :: HNil] { type Out = H :: HNil }
Now the crux of it. What is the axiomatic definition of sorting a list with at least two elements?
Well, you have to split, sort the halves and merge them together, right?
Let's think it backwards. Let U
be the unsorted list.
Sorted[U] = merged.Out
…merged
satisfies merged = Merge[SL, SR]
…SL
and SR
satisfy Sorted.Aux[L, SL]
and Sorted.Aux[R, SR]
, respectively…L
and R
satisfy Split.Aux[U, L, R]
.
Now read the “such that…” in the words of the compiler, which says “I need to find an implicit such that…”.
More words are worthless. The dragon-killing code is below:
implicit def inductive[U <: HList, L <: HList, R <: HList, SL <: HList, SR <: HList] (implicit split: Split.Aux[U, L, R], sl: Sorted.Aux[L, SL], sr: Sorted.Aux[R, SR], merged: Merge[SL, SR]) : Aux[U, merged.Out] = new Sorted[U] { type Out = merged.Out }
If you find the above code a bit hard to read, you passed the test - you're a normal human being seeing alien code for the first time.
Write two or three more of these and you'll start to really read them.
The above code is the exact representation of the axiom for the induction case.
If you know a bit of Prolog and constraint satisfaction, here's an equivalent Prolog code, it might help.
The compiler goes through almost the same resolution process:
sort([], []). sort([H], [H]). sort(U, M) :- split(U, L, R), sort(L, SL), sort(R, SR), merge(SL, SR, M).
Also if it helps, here's a potato.
And finally, a (very boring by now) apply method:
def apply[L <: HList](implicit sorted: Sorted[L]): Aux[L, sorted.Out] = new Sorted[L] { type Out = sorted.Out }
And that was it. You can now mergesort types, at compile time. If we make Sorted
extend HList
and put in some magic test code
def show[L <: HList](s: L)(implicit tag: TypeTag[L]) = tag def main(args: Array[String]): Unit = { val x = Sorted[_1 :: _5 :: _0 :: _3 :: _2 :: HNil] println(show(x)) }
You'll see that…
… well, test it for yourself!
Congratulations - you can now mergesort types, at compile time, with Scala.
Breathe.