Re: [Haskell-cafe] Hello and type-level SKI
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).
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.
participants (2)
-
Jay Sulzberger -
oleg＠okmij.org