def implicitly[A](implicit a: A) = a case class Foo(x: Int) implicit val foo = Foo(5) implicitly[Foo] class =:=[A, B] implicit def equalTypeInstance[A] = new =:=[A, A] //# this does not compile //# implicitly[Int =:= String] implicitly[Int =:= Int] def type_==[A, B](implicit ev: A =:= B = null) = ev != null type_==[Int, Int] type_==[Int, String] class <:<[-A, +B] implicit def subTypeInstance[A] = new <:<[A, A] //# this does not compile //# implicitly[Int <:< String] implicitly[List[Int] <:< Seq[Int]] def type_<[A, B](implicit ev: A <:< B = null) = ev != null type_<[Int, String] type_<[List[String], Seq[String]] sealed trait Bool sealed trait True extends Bool sealed trait False extends Bool sealed trait Bool { type Not } sealed trait True extends Bool { type Not = False } sealed trait False extends Bool { type Not = True } type_==[True, False#Not] 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 } 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] } import Bool._ type_==[True, Not[False]] implicitly[False =:= &&[True, False]] implicitly[True =:= ||[True, False]] def bool2val[A <: Bool]: Boolean = type_==[A, True] bool2val[True] def bool2val[A <: Bool](implicit ev: A =:= True = null) = type_==[A, True] bool2val[True] bool2val[False] sealed trait Nat sealed trait _0 extends Nat sealed trait Succ[N <: Nat] extends Nat type _1 = Succ[_0] 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] type_==[_0#IfZero[True, False, Bool], True] 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] import Nat._ type_==[_0, Pred[_1]] type_==[_1, Pred[_0]] object NatOps { type Plus[A <: Nat, B <: Nat] = A#IfZero[B, Succ[Plus[Pred[A], B]], Nat] } 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] import Nat._ type_==[Plus[_2, _2], _4] type_==[Plus[_2, _2], _3] 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 nat2value[_2] trait FoldOp[A, B] { def apply(a: A, b: B): B } trait Fold[A, B] { type Apply[X <: A, Y <: B] <: B } 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]] } 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] } 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 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] 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] } import NatOps._ type_==[Plus[_2, Times[_2, _3]], _8] type_==[Minus[_5, _3], _2] type_==[Minus[_3, _5], _0] 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] } import MoreNatOps._ type_==[IfZero[_0, True, False, Bool], True] type_==[IfZero[_3, True, False, Bool], False] type_==[Succ[Pred[_3]], _3] bool2val[_3 Leq _4] bool2val[_4 Leq _3] 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] val list = 1 :: 2 :: 3 :: 4 :: Nil list.tail 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] val nlist: NCons[_2, Int] = 1 :: 2 :: 3 :: NNil nlist.tail %type nlist.tail nlist.tail.tail 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) } class Sized[N <: Nat, A](underlying: Seq[A]) { def apply[M <: Nat](implicit ev: Less[M, N] =:= True, ev1: NatConverter[M]) = underlying(nat2value[M]) } val seq = new Sized[_3, Int](List(1, 2, 3)) seq[_1] seq[_4] val seq1 = new Sized[_8, Int](List(1, 2, 3)) seq1[_5] val seq2 = new Sized[_3, Int](List(1, 2, 3, 4, 5)) seq2[_3] 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 } import Sized._ val Some(s) = sized[_3, Int](List(1, 2, 3)) sized[_8, Int](List(1, 2, 3)) new Sized[_8, Int](List(1, 2, 3)) s[_2] 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]) } import Sized._ val Some(s) = sized[_3, Int](List(1, 2, 3)) s :+ 5 s ++ s s.head s.tail s.tail.tail.tail.tail single(1) :+ 2 :+ 3 1 +: 2 +: 3 +: SNil[Int] type IsLeq[A <: Nat, B <: Nat] = Leq[A, B] =:= True 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) } val a = Mod[_4](10) a * a def power[N <: Nat](x: Mod[N], y: Int): Mod[N] = if (y == 1) x else x * power(x, y - 1) val b = Mod[_7](6) power(b, 1000) b + Mod[_5](3) trait Application[A, F, G]{ type Out def apply(a: A, f: F, g: G): Out } def choose[A, F, G](a: A, f: F, g: G)(implicit app: Application[A, F, G]): app.Out = app(a, f, g) 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) } choose(3, { x: Int => x * x }, { x: String => "hello " + x }) choose("world", { x: Int => x * x }, { x: String => "hello " + x }) 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] } 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] } } 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 type_==[b1.N, _1] type_==[b3.N, _2] val b5 = Branch(5, b3, b4) Branch(5, b1, b3) //# left branch too small Branch(5, b4, Leaf) //# left branch too high Branch(5, b5, b1) //# left branch too high