[Haskell-cafe] Hello and type-level SKI

Jay Sulzberger jays at panix.com
Thu Sep 18 20:11:12 UTC 2014




On Wed, 17 Sep 2014, oleg at 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.


More information about the Haskell-Cafe mailing list