{
 "metadata": {
  "name": "",
  "signature": "sha256:67dcefedc77e92ed8e009963a9230eaa3909bc1531684b9f06f7e53ebb9fba72"
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "heading",
     "level": 1,
     "metadata": {},
     "source": [
      "Working on the type level"
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "0. Introduction"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Scala has a sophisticated type system that allows to catch many logic errors. Let's make it to good use.\n",
      "\n",
      "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.\n",
      "\n",
      "**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.\n",
      "\n",
      "Applications will include:\n",
      "\n",
      "* fixed-size sequences\n",
      "* modular arithmetic\n",
      "* balanced trees"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "**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.\n",
      "\n",
      "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:\n",
      "\n",
      "* Coq\n",
      "* Agda\n",
      "* Idris\n",
      "* ATS\n",
      "\n",
      "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."
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "1. Preliminaries"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We start with a few functions and types that are defined in the Scala prequel, since we will need to understand how they work.\n",
      "\n",
      "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.\n",
      "\n"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def implicitly[A](implicit a: A) = a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Let us check that this works as expected"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "case class Foo(x: Int)\n",
      "\n",
      "implicit val foo = Foo(5)\n",
      "implicitly[Foo]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Can we use the same method to check whether some types are the same?"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class =:=[A, B]\n",
      "    \n",
      "implicit def equalTypeInstance[A] = new =:=[A, A]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We use this definition, together with `implicitly`, to check for type equality"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "//# this does not compile\n",
      "//# implicitly[Int =:= String]\n",
      "implicitly[Int =:= Int]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def type_==[A, B](implicit ev: A =:= B = null) = ev != null"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Int, Int]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Int, String]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Great, next we do the same for subtyping"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class <:<[-A, +B]\n",
      "    \n",
      "implicit def subTypeInstance[A] = new <:<[A, A]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "This variance trick is all that is needed to make this work, see:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "//# this does not compile\n",
      "//# implicitly[Int <:< String]\n",
      "implicitly[List[Int] <:< Seq[Int]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def type_<[A, B](implicit ev: A <:< B = null) = ev != null"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_<[Int, String]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_<[List[String], Seq[String]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "2. Encoding some values as types"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Booleans"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "It is not difficult to encode some types, and the relative operations, at the type level. We start with booleans"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Bool\n",
      "sealed trait True extends Bool\n",
      "sealed trait False extends Bool"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "This is a start, but we do not have any operations yet. Let us do better"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Bool {\n",
      "    type Not\n",
      "}\n",
      "sealed trait True extends Bool {\n",
      "    type Not = False\n",
      "}\n",
      "sealed trait False extends Bool {\n",
      "    type Not = True\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[True, False#Not]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can even encode the `if` operation:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Bool {\n",
      "    type Not\n",
      "    type If[T <: Up, F <: Up, Up] <: Up\n",
      "}\n",
      "sealed trait True extends Bool {\n",
      "    type Not = False\n",
      "    type If[T <: Up, F <: Up, Up] = T\n",
      "}\n",
      "sealed trait False extends Bool {\n",
      "    type Not = True\n",
      "    type If[T <: Up, F <: Up, Up] = F\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Note that we have three parameters: `Up` is there to guarantee that the result of the operation is a supertype of both branch types.\n",
      "\n",
      "We can then use `If` to define `Not`, and we will add some more operations as well"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Bool {\n",
      "    type If[T <: Up, F <: Up, Up] <: Up\n",
      "}\n",
      "sealed trait True extends Bool {\n",
      "    type If[T <: Up, F <: Up, Up] = T\n",
      "}\n",
      "sealed trait False extends Bool {\n",
      "    type If[T <: Up, F <: Up, Up] = F\n",
      "}\n",
      "\n",
      "object Bool {\n",
      "    type &&[A <: Bool, B <: Bool] = A#If[B, False, Bool]\n",
      "    type || [A <: Bool, B <: Bool] = A#If[True, B, Bool]\n",
      "    type Not[A <: Bool] = A#If[False, True, Bool]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Let us check that everything works as expected"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import Bool._\n",
      "\n",
      "type_==[True, Not[False]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "implicitly[False =:= &&[True, False]]\n",
      "implicitly[True =:= ||[True, False]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can use our type test function to convert `Bool` types to `Boolean` values"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def bool2val[A <: Bool]: Boolean = type_==[A, True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "bool2val[True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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.\n",
      "\n",
      "Let us summon the implicit instance in scope"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def bool2val[A <: Bool](implicit ev: A =:= True = null) = type_==[A, True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "bool2val[True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "bool2val[False]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Much better"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Natural numbers"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can construct naturals the Peano way"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Nat\n",
      "sealed trait _0 extends Nat\n",
      "sealed trait Succ[N <: Nat] extends Nat"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "and then define"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type _1 = Succ[_0]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "and so on. Of course, we can add some operations too"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] <: Up\n",
      "}\n",
      "sealed trait _0 extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = T\n",
      "}\n",
      "sealed trait Succ[N <: Nat] extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = F\n",
      "}\n",
      "type _1 = Succ[_0]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We check that these work as expected"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[_0#IfZero[True, False, Bool], True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can extend this to define, say, the precedessor function, which of course has to be defined so that `Pred[_0]` is `_0`"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] <: Up\n",
      "    type Pred <: Nat\n",
      "}\n",
      "sealed trait _0 extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = T\n",
      "    type Pred = _0\n",
      "}\n",
      "sealed trait Succ[N <: Nat] extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = F\n",
      "    type Pred = N\n",
      "}\n",
      "\n",
      "object Nat {\n",
      "    type Pred[N <: Nat] = N#Pred\n",
      "}\n",
      "type _1 = Succ[_0]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import Nat._\n",
      "\n",
      "type_==[_0, Pred[_1]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[_1, Pred[_0]]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "One would think this is enough to define addition recursively. Let's see"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "object NatOps {\n",
      "    type Plus[A <: Nat, B <: Nat] = A#IfZero[B, Succ[Plus[Pred[A], B]], Nat]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The compiler will not allow recursive type definitions. We can work around this by adding one more operation to our `Nat`"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] <: Up\n",
      "    type Pred <: Nat\n",
      "    type Plus[B <: Nat] <: Nat\n",
      "}\n",
      "sealed trait _0 extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = T\n",
      "    type Pred = _0\n",
      "    type Plus[B <: Nat] = B\n",
      "}\n",
      "sealed trait Succ[N <: Nat] extends Nat {\n",
      "    type IfZero[T <: Up, F <: Up, Up] = F\n",
      "    type Pred = N\n",
      "    type Plus[B <: Nat] = Succ[N#Plus[B]]\n",
      "}\n",
      "\n",
      "object Nat {\n",
      "    type Pred[N <: Nat] = N#Pred\n",
      "    type Plus[A <: Nat, B <: Nat] = A#Plus[B]\n",
      "}\n",
      "type _1 = Succ[_0]\n",
      "type _2 = Succ[_1]\n",
      "type _3 = Succ[_2]\n",
      "type _4 = Succ[_3]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Let's see this in action!"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import Nat._\n",
      "type_==[Plus[_2, _2], _4]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Plus[_2, _2], _3]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "As before, we can convert these types to values."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class NatConverter[N <: Nat](val n: Int)\n",
      "\n",
      "implicit val zeroConverter: NatConverter[_0] = new NatConverter(0)\n",
      "implicit def succConverter[N <: Nat](implicit ev: NatConverter[N]): NatConverter[Succ[N]] = new NatConverter(ev.n + 1)\n",
      "\n",
      "def nat2value[N <: Nat](implicit ev: NatConverter[N]) = ev.n"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "nat2value[_2]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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?\n",
      "\n",
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "trait FoldOp[A, B] {\n",
      "    def apply(a: A, b: B): B\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We will then define the type-level analogue"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "trait Fold[A, B] {\n",
      "    type Apply[X <: A, Y <: B] <: B\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `FoldR` operation can then be defined on `Nat` as follows"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Nat {\n",
      "    type Pred <: Nat\n",
      "    type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] <: Up\n",
      "}\n",
      "sealed trait _0 extends Nat {\n",
      "    type Pred = _0\n",
      "    type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] = Init\n",
      "}\n",
      "sealed trait Succ[N <: Nat] extends Nat {\n",
      "    type Pred = N\n",
      "    type FoldR[Init <: Up, Op <: Fold[Nat, Up], Up] = Op#Apply[Succ[N], N#FoldR[Init, Op, Up]]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Phew... that was quite complex! Anyway, we can now define a few operations"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "object NatOps {\n",
      "    type Incr = Fold[Nat, Nat] {\n",
      "       type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]\n",
      "    }\n",
      "    type Plus[A <: Nat, B <: Nat] = A#FoldR[B, Incr, Nat]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class NatConverter[N <: Nat](val n: Int)\n",
      "\n",
      "implicit val zeroConverter: NatConverter[_0] = new NatConverter(0)\n",
      "implicit def succConverter[N <: Nat](implicit ev: NatConverter[N]): NatConverter[Succ[N]] = new NatConverter(ev.n + 1)\n",
      "\n",
      "def nat2value[N <: Nat](implicit ev: NatConverter[N]) = ev.n"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import NatOps._\n",
      "type _1 = Succ[_0]\n",
      "type _2 = Succ[_1]\n",
      "type _3 = Succ[_2]\n",
      "type _4 = Succ[_3]\n",
      "type _5 = Succ[_4]\n",
      "type _6 = Succ[_5]\n",
      "type _7 = Succ[_6]\n",
      "type _8 = Succ[_7]\n",
      "\n",
      "type_==[Plus[_3, _4], _7]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "By the same method we can add multiplication, and (bounded) difference"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "object NatOps {\n",
      "    type Incr = Fold[Nat, Nat] {\n",
      "       type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]\n",
      "    }\n",
      "    type Plus[A <: Nat, B <: Nat] = A#FoldR[B, Incr, Nat]\n",
      "    type Sum[B <: Nat] = Fold[Nat, Nat] {\n",
      "       type Apply[N <: Nat, Acc <: Nat] = Plus[Acc, B]\n",
      "    }\n",
      "    type Times[A <: Nat, B <: Nat] = A#FoldR[_0, Sum[B], Nat]\n",
      "    type Decr = Fold[Nat, Nat] {\n",
      "       type Apply[N <: Nat, Acc <: Nat] = Acc#Pred\n",
      "    }\n",
      "    type Minus[A <: Nat, B <: Nat] = B#FoldR[A, Decr, Nat]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import NatOps._\n",
      "\n",
      "type_==[Plus[_2, Times[_2, _3]], _8]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Minus[_5, _3], _2]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Minus[_3, _5], _0]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "In fact, we can define the `IfZero` operations as well, and use that to implement comparison"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "object MoreNatOps {\n",
      "    type NonZero[Up, F <: Up] = Fold[Nat, Up] {\n",
      "        type Apply[N <: Nat, Acc <: Up] = F\n",
      "    }\n",
      "    type IfZero[A <: Nat, T <: Up, F <: Up, Up] = A#FoldR[T, NonZero[Up, F], Up]\n",
      "    type Pred[N <: Nat] = N#Pred\n",
      "    type Leq[A <: Nat, B <: Nat] = IfZero[Minus[A, B], True, False, Bool]\n",
      "    type Less[A <: Nat, B <: Nat] = Leq[Succ[A], B]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import MoreNatOps._\n",
      "type_==[IfZero[_0, True, False, Bool], True]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[IfZero[_3, True, False, Bool], False]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[Succ[Pred[_3]], _3]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "bool2val[_3 Leq _4]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "bool2val[_4 Leq _3]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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"
     ]
    },
    {
     "cell_type": "heading",
     "level": 1,
     "metadata": {},
     "source": [
      "Dependent types"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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:\n",
      "\n",
      "* path-dependent types - encoded as type members;\n",
      "* value-dependent return types in methods;\n",
      "* implicits, to make all the necessary wiring less verbose.\n",
      "\n",
      "Let us see some example in action"
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Fixed-length lists"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The poster child for dependent types are range types and fixed-length lists. We shall start from the latter.\n",
      "\n",
      "We start by recalling the usual definition of `List`"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait List[+A] {\n",
      "    def ::[B >: A](b: B): List[B] = Cons[B](b, this)\n",
      "    def head: A\n",
      "    def tail: List[A]\n",
      "}\n",
      "case object Nil extends List[Nothing] {\n",
      "    def head = sys.error(\"empty list\")\n",
      "    def tail = sys.error(\"empty list\")\n",
      "}\n",
      "case class Cons[A](val head: A, val tail: List[A]) extends List[A]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can use it as customary"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val list = 1 :: 2 :: 3 :: 4 :: Nil"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "list.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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`.\n",
      "\n",
      "Let us parametrize lists by their length, which is a natural number"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait NList[N <: Nat, +A] {\n",
      "    def ::[B >: A](b: B) = NCons[N, B](b, this)\n",
      "}\n",
      "case object NNil extends NList[_0, Nothing]\n",
      "case class NCons[N <: Nat, A](val head: A, val tail: NList[N, A]) extends NList[Succ[N], A]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val nlist: NCons[_2, Int] = 1 :: 2 :: 3 :: NNil"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "nlist.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "%type nlist.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "nlist.tail.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def append[M <: Nat, N <: Nat, A](xs: NList[M, A], ys: NList[N, A]): NList[Plus[M, N], A] = xs match {\n",
      "    case NNil => ys\n",
      "    case NCons(h, t) => h :: append(t, ys)\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Looks like the naive definition we used is no good at all. The compiler is not able to prove much about our natural numbers.\n",
      "\n",
      "We will try a different approach: wrap an unsafe data structure and only provide operations when **we** know they can be carried out"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class Sized[N <: Nat, A](underlying: Seq[A]) {\n",
      "    def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val seq = new Sized[_3, Int](List(1, 2, 3))\n",
      "\n",
      "seq[_1]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "seq[_4]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We still have the problem that the following compiles, and fails at runtime"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val seq1 = new Sized[_8, Int](List(1, 2, 3))\n",
      "\n",
      "seq1[_5]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Symmetrically"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val seq2 = new Sized[_3, Int](List(1, 2, 3, 4, 5))\n",
      "\n",
      "seq2[_3]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To avoid this problem, we use a package-private constructor and we expose a safe API"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class Sized[N <: Nat, A]private(underlying: Seq[A]) {\n",
      "    def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])\n",
      "}\n",
      "object Sized {\n",
      "    def sized[N <: Nat, A](xs: Seq[A])(implicit ev: NatConverter[N]): Option[Sized[N, A]] =\n",
      "        if (xs.length == nat2value[N]) Some(new Sized(xs)) else None\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import Sized._\n",
      "\n",
      "val Some(s) = sized[_3, Int](List(1, 2, 3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sized[_8, Int](List(1, 2, 3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "new Sized[_8, Int](List(1, 2, 3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s[_2]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class Sized[N <: Nat, A]private(val underlying: Seq[A])(implicit ev: NatConverter[N]) {\n",
      "    def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M])\n",
      "\n",
      "    def +:(x: A)(implicit ev: NatConverter[Succ[N]]) = new Sized[Succ[N], A](x +: underlying)\n",
      "    def :+(x: A)(implicit ev: NatConverter[Succ[N]]) = new Sized[Succ[N], A](underlying :+ x)\n",
      "    def ++[M <: Nat](xs: Sized[M, A])(implicit ev: NatConverter[Plus[N, M]]) = new Sized[Plus[N, M], A](underlying ++ xs.underlying)\n",
      "    def head(implicit ev: Less[_0, N] =:= True) = underlying.head\n",
      "    def tail(implicit ev: Less[_0, N] =:= True, ev1: NatConverter[Pred[N]]) = new Sized[Pred[N], A](underlying.tail)\n",
      "\n",
      "    override def toString = s\"Sized[${ nat2value[N] }]: ${ underlying }\"\n",
      "}\n",
      "object Sized {\n",
      "    def sized[N <: Nat, A](xs: Seq[A])(implicit ev: NatConverter[N]): Option[Sized[N, A]] =\n",
      "        if (xs.length == nat2value[N]) Some(new Sized(xs)) else None\n",
      "    def single[A](x: A) = new Sized[_1, A](List(x))\n",
      "    def SNil[A] = new Sized[_0, A](Seq.empty[A])\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import Sized._\n",
      "\n",
      "val Some(s) = sized[_3, Int](List(1, 2, 3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s :+ 5"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s ++ s"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s.head"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "So far, everything is going on as expected. Will the compiler prevent us to take too many tails?"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "s.tail.tail.tail.tail"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Some more operations show that this is quite a simple to use data structure"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "single(1) :+ 2 :+ 3"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "1 +: 2 +: 3 +: SNil[Int]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Modular arithmetic"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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.\n",
      "\n",
      "We will implement modular reduction for a natural `N` greater than `_0`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type IsLeq[A <: Nat, B <: Nat] = Leq[A, B] =:= True"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "class Mod[N <: Nat](x: Int)(implicit ev: _1 IsLeq N, ev1: NatConverter[N]) {\n",
      "    lazy val n = x % nat2value[N]\n",
      "\n",
      "    def +(y: Mod[N]) = new Mod[N](n + y.n)\n",
      "    def -(y: Mod[N]) = new Mod[N](n - y.n)\n",
      "    def *(y: Mod[N]) = new Mod[N](n * y.n)\n",
      "    override def toString = s\"$n mod ${ nat2value[N] }\"\n",
      "}\n",
      "object Mod {\n",
      "    def apply[N <: Nat](x: Int)(implicit ev: _1 IsLeq N, ev1: NatConverter[N]) = new Mod[N](x)\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val a = Mod[_4](10)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a * a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def power[N <: Nat](x: Mod[N], y: Int): Mod[N] = if (y == 1) x else x * power(x, y - 1)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val b = Mod[_7](6)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "power(b, 1000)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "b + Mod[_5](3)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Compile guards"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Another neat application of dependent types allows us to choose one of two branches based on which one compiles. Let us define a trait"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "trait Application[A, F, G]{\n",
      "  type Out\n",
      "\n",
      "  def apply(a: A, f: F, g: G): Out\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def choose[A, F, G](a: A, f: F, g: G)(implicit app: Application[A, F, G]): app.Out = app(a, f, g)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "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.\n",
      "\n",
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "implicit def applyf[A, B, G] = new Application[A, A => B, G] {\n",
      "    type Out = B\n",
      "    def apply(a: A, f: A => B, g: G) = f(a)\n",
      "}\n",
      "implicit def applyg[A, B, F] = new Application[A, F, A => B] {\n",
      "    type Out = B\n",
      "    def apply(a: A, f: F, g: A => B) = g(a)\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "See it in action:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "choose(3, { x: Int => x * x }, { x: String => \"hello \" + x })"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "choose(\"world\", { x: Int => x * x }, { x: String => \"hello \" + x })"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Balanced trees"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "As a final example, we will build a balanced binary tree type, so that unbalanced trees will be a compile time error.\n",
      "\n",
      "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:\n",
      "\n",
      "* the left branch is at least as high as the right one\n",
      "* the left branch is at most high one more than the right one\n",
      "\n",
      "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"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sealed trait Tree[+T]{\n",
      "  type N <: Nat\n",
      "}\n",
      "object Leaf extends Tree[Nothing]{\n",
      "  type N = _0\n",
      "}\n",
      "trait Branch[T] extends Tree[T]{\n",
      "  def value: T\n",
      "  def left: Tree[T]\n",
      "  def right: Tree[T]\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "object Branch {\n",
      "  type HBranch[T, N0 <: Nat] = Branch[T] { type N = N0 }\n",
      "\n",
      "  def apply[T, D <: Nat](value0: T, left0: Tree[T], right0: Tree[T])\n",
      "    (implicit ev: right0.N IsLeq left0.N, ev1: left0.N IsLeq Succ[right0.N]): HBranch[T, Succ[left0.N]] =\n",
      "      new Branch[T] {\n",
      "        val value = value0\n",
      "        val left = left0\n",
      "        val right = right0\n",
      "        type N = Succ[left0.N]\n",
      "      }\n",
      "}"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val b1 = Branch(1, Leaf, Leaf) //# N = 1\n",
      "val b2 = Branch(2, Leaf, Leaf) //# N = 1\n",
      "val b3 = Branch(3, b1, Leaf) //# N = 2\n",
      "val b4 = Branch(4, b2, b1) //# N = 2"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Let us check that the height are as expected"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[b1.N, _1]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "type_==[b3.N, _2]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "val b5 = Branch(5, b3, b4)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Look what happens as soon as we try to define unbalanced trees.."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "Branch(5, b1, b3) //# left branch too small"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "Branch(5, b4, Leaf) //# left branch too high"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "Branch(5, b5, b1) //# left branch too high"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "heading",
     "level": 1,
     "metadata": {},
     "source": [
      "References"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "* [Type-level programming in Scala](https://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/)\n",
      "* [Any reason why Scala does not explicitly support dependent types?](http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types)\n",
      "* [Shapeless](https://github.com/milessabin/shapeless)\n",
      "* [Dependent types in Scala](http://wheaties.github.io/Presentations/Scala-Dep-Types/dependent-types.html#/)\n",
      "* [Type programming](http://proseand.co.nz/2014/02/17/type-programming-shifting-from-values-to-types/)\n",
      "* [There's a Prolog in your Scala](https://skillsmatter.com/skillscasts/4905-theres-a-prolog-in-your-scala)"
     ]
    }
   ],
   "metadata": {}
  }
 ]
}