Also! I did not know that Odersky & associates are working on a clean reimplementation of Scala called "Dotty" that is named after exactly this kind of type the

Also! I did not know that Odersky & associates are working on a clean reimplementation of Scala called "Dotty" that is named after exactly this kind of type theory (Dependent Object Types or DOT). They just got their compiler to self-host, see https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty and http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-boo...