I would like to make two claims:

- The Scala type system is turing complete.
- This is not a bug.

The SKI combinator calculus is known to be turing equivalent:

trait λ { type ap[_<:λ]<:λ }
type I = λ{type ap[X<:λ] = X }
type K = λ{type ap[X<:λ] = λ{type ap[Y<:λ] = X }}
type S = λ{type ap[X<:λ] = λ{type ap[Y<:λ] = λ{type ap[Z<:λ] = X#ap[Z]#ap[Y#ap[Z]] }}}

And we can blow up the compiler with unbounded recursion, without resorting to circular definitions:

type Y = S#ap[I]#ap[I]#ap[S#ap[I]#ap[I]]

The latter should crash the compiler with a stack overflow error.

Hat tip: Edward Kmett

### Like this:

Like Loading...

*Related*

That’s a very nice encoding of the SKI calculus. However there seems to be a problem with the order of evaluation

case class Equals[A >: B <:B , B]()

Equals[S#ap[K]#ap[K]#ap[I], I]

fails to compile.

I had quite a hard time sorting these things out in my implementation. See http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

You’re absolutely right. It won’t actually unify types that appear to be equivalent.

Runar, could you do me a favour and actually implement a turing machine in your SKI calculus?

I’m just curious as to how difficult that would be.

Not on your life.