17 Sep
2014
17 Sep
'14
6:43 a.m.
Yet another demonstration of Turing completeness of the type checker (given the unrestricted context reduction stack) was lambda-calculator in types, posted back in 2006. http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level The examples included the Fibonacci function (encoded using the fix-point combinator) and the SKI calculator (expressing combinators as lambda-terms).