Re: [Haskell-cafe] Hello and type-level SKI

On Wed, 17 Sep 2014, oleg@okmij.org wrote:

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).

Oleg, thanks! I have run my eyes over the code, but not yet run it. Heaven forwarding, I will within a few days. Of course, it would be good to have translators between all three Turing machine implementations ;) oo--JS.