Simple SKI Combinator Calculus in Scala’s Type System

I would like to make two claims:

  1. The Scala type system is turing complete.
  2. 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

About these ads

4 thoughts on “Simple SKI Combinator Calculus in Scala’s Type System

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s