**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:

- First of all, people in their right mind use boring languages and by now you've seen that Scala is anything but.

- More importantly, we want to understand the magic behind Scala's type inference system.

If we understand this, few programming concepts will ever stand in our way.

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:

- Hey, that's the same as saying
`Succ[_1] < Succ[_3]`

by the names I've given to the`_2`

and the`_4`

types! - Does
`Succ[_1] < Succ[_3]`

exist? - Hm, first axiom doesn't work.
- OK, second axiom -
`Succ[_1] < Succ[_3]`

exists if`_1 < _3`

exists. OK. - Hey, that's the same as saying
`Succ[_0] < Succ[_2]`

! - Does
`Succ[_0] < Succ[_2]`

exist? - Hm, first axiom doesn't work.
- OK, second axiom -
`Succ[_0] < Succ[_2]`

exists if`_0 < _2`

exists. OK. - Hey, that's the same as saying
`_0 < Succ[_1]`

! - Does
`_0 < Succ[_1]`

exist? - First axiom - Yes!
- So
`_0 < _2`

exists, - So
`_1 < _3`

exists, - So
`_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:

- hey, this programmer's calling the apply method of the object
`<`

with the types`_0`

and`_2`

- the method takes an implicit parameter, it has the type <[
`_0, _2`

] or`<[_0, Succ[_1]]`

- well I have an implicit method which gives me an instance of exactly
`<[_0, Succ[_1]]`

- hey implicit, when the program runs, I'll call you for this one! - implicit says: no problem boss.
- well good, implicit said OK, let me link up the types and just give a green light to the programmer.

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:

- the damn programmer's calling the apply method with the types
`_1`

and`_2`

. - the apply method takes an implicit parameter, it has the type
`<[_1, _2]`

or`<[Succ[_0], Succ[_1]]`

. - well I have an implicit method which gives me an instance of exactly
`<[Succ[_0], Succ[_1]]`

, it's called`inductive`

. - hey
`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.- OK, so I'll need an instance of
`<[_0, _1]`

. - luckily I have an implicit named
`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.- well good,
`basic`

and`inductive`

said OK:- when
`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`

- everything's fine, let me link up the types and just give a green light to the damn programmer.

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:

- Need to sort a list? Fine, split it half.
- Sort the halves.
- Merge the sorted halves in a sorted fashion.

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

- I can't instantiate Aux on its own, because it's just a type name, not a class/trait declaration
- I
*have*to specify the types for`Left`

and`Right`

and they have to match - otherwise the compiler's type equalizer will fail - I'm helping the compiler actually “write” the types in the
`Split[HNil]`

instance I'm returning

We'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]`

:

- apply method - I need an implicit which gives me a 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.- All good. Linking up the types:
`Split[_2 :: HNil] { Left = _2 :: HNil, Right = HNil }`

from`basic2`

, now going back to`Split[_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`

…**such that**`merged`

satisfies`merged = Merge[SL, SR]`

…**such that**`SL`

and`SR`

satisfy`Sorted.Aux[L, SL]`

and`Sorted.Aux[R, SR]`

, respectively…**such that**`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.