Scala type level encoding of the SKI calculus

29 01 2010

In one of my posts on type level meta programming in Scala the question of Turing completeness came up already. The question is whether Scala’s type system can be used to force the Scala compiler to carry out any calculation which a Turing machine is capable of. Various of my older posts show how Scala’s type system can be used to encode addition and multiplication on natural numbers and how to encode conditions and bounded loops.

Motivated by the blog post More Scala Typehackery which shows how to encode a version of the Lambda calculus which is limited to abstraction over a single variable in Scala’s type system I set out to further explore the topic.

The SKI combinator calculus


Looking for a calculus which is relatively small, easily encoded in Scala’s type system and known to be Turing complete I came across the SKI combinator calculus. The SKI combinators are defined as follows:

Ix \rightarrow x ,
Kxy \rightarrow x ,
Sxyz \rightarrow xz(yz) .

They can be used to encode arbitrary calculations. For example reversal of arguments. Let R \equiv S(K(SI))K . Then

R x y \equiv
S(K(SI))K x y \rightarrow
K(SI)x(Kx)y \rightarrow
SI(Kx)y \rightarrow
Iy(Kxy) \rightarrow
Iyx \rightarrow yx .

Self application is used to find fixed points. Let \beta \equiv S(K\alpha)(SII) for some combinator \alpha . Then \beta\beta \rightarrow \alpha(\beta \beta) . That is, \beta\beta is a fixed point of \alpha . This can be used to achieve recursion. Let R be the reversal combinator from above. Further define

A_0 x \equiv c for some combinator c and
A_n x \equiv x A_{n-1} .

That is, combinator A_n is the combinator obtained by applying its argument to the combinator A_{n-1}. (There is a bit of cheating here: I should actually show that such combinators exist. However since the SKI calculus is Turing complete, I take this for granted.) Now let \alpha be R in \beta from above (That is we have \beta \equiv S(KR)(SII) now). Then

\beta\beta A_0 \rightarrow c

and by induction

\beta\beta A_n \rightarrow \beta\beta A_{n-1} \rightarrow c.

Type level SKI in Scala


Encoding the SKI combinator calculus in Scala’s type system seems not too difficult at first. It turns out however that some care has to be taken regarding the order of evaluation. To guarantee that for all terms which have a normal form, that normal form is actually found, a lazy evaluation order has to be employed.

Here is a Scala type level encoding of the SKI calculus:

trait Term {
  type ap[x <: Term] <: Term
  type eval <: Term
}
  
// The S combinator
trait S extends Term {
  type ap[x <: Term] = S1[x] 
  type eval = S
}
trait S1[x <: Term] extends Term {
  type ap[y <: Term] = S2[x, y]
  type eval = S1[x]
}
trait S2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = S3[x, y, z]
  type eval = S2[x, y]
}
trait S3[x <: Term, y <: Term, z <: Term] extends Term {
  type ap[v <: Term] = eval#ap[v]
  type eval = x#ap[z]#ap[y#ap[z]]#eval
}

// The K combinator
trait K extends Term {
  type ap[x <: Term] = K1[x]
  type eval = K
}
trait K1[x <: Term] extends Term {
  type ap[y <: Term] = K2[x, y]
  type eval = K1[x]
}
trait K2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = eval#ap[z]
  type eval = x#eval
}
  
// The I combinator
trait I extends Term {
  type ap[x <: Term] = I1[x]
  type eval = I
}
trait I1[x <: Term] extends Term {
  type ap[y <: Term] = eval#ap[y]
  type eval = x#eval
}

Further lets define some constants to act upon. These are used to test whether the calculus actually works.

trait c extends Term {
  type ap[x <: Term] = c
  type eval = c
}
trait d extends Term {
  type ap[x <: Term] = d
  type eval = d
}
trait e extends Term {
  type ap[x <: Term] = e
  type eval = e
}

Eventually the following definition of Equals lets us check types for equality:

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

Equals[Int, Int]     // compiles fine
Equals[String, Int] // won't compile

Now lets see whether we can evaluate some combinators.

  // Ic -> c
  Equals[I#ap[c]#eval, c]
  
  // Kcd -> c
  Equals[K#ap[c]#ap[d]#eval, c]

  // KKcde -> d
  Equals[K#ap[K]#ap[c]#ap[d]#ap[e]#eval, d]
  
  // SIIIc -> Ic
  Equals[S#ap[I]#ap[I]#ap[I]#ap[c]#eval, c]

  // SKKc -> Ic
  Equals[S#ap[K]#ap[K]#ap[c]#eval, c]

  // SIIKc -> KKc
  Equals[S#ap[I]#ap[I]#ap[K]#ap[c]#eval, K#ap[K]#ap[c]#eval]

  // SIKKc -> K(KK)c
  Equals[S#ap[I]#ap[K]#ap[K]#ap[c]#eval, K#ap[K#ap[K]]#ap[c]#eval]

  // SIKIc -> KIc
  Equals[S#ap[I]#ap[K]#ap[I]#ap[c]#eval, K#ap[I]#ap[c]#eval]

  // SKIc -> Ic
  Equals[S#ap[K]#ap[I]#ap[c]#eval, c]
  
  // R = S(K(SI))K  (reverse)
  type R = S#ap[K#ap[S#ap[I]]]#ap[K]
  Equals[R#ap[c]#ap[d]#eval, d#ap[c]#eval]

Finally lets check whether we can do recursion using the fixed point operator from above. First lets define \beta .

  // b(a) = S(Ka)(SII)
  type b[a <: Term] = S#ap[K#ap[a]]#ap[S#ap[I]#ap[I]]

Further lets define some of the A_ns from above.

trait A0 extends Term {
  type ap[x <: Term] = c
  type eval = A0
}
trait A1 extends Term {
  type ap[x <: Term] = x#ap[A0]#eval
  type eval = A1
}
trait A2 extends Term {
  type ap[x <: Term] = x#ap[A1]#eval
  type eval = A2
}

Now we can do iteration on the type level using a fixed point combinator:

  // Single iteration
  type NN1 = b[R]#ap[b[R]]#ap[A0]
  Equals[NN1#eval, c]

  // Double iteration
  type NN2 = b[R]#ap[b[R]]#ap[A1]
  Equals[NN2#eval, c]

  // Triple iteration
  type NN3 = b[R]#ap[b[R]]#ap[A2]
  Equals[NN3#eval, c]

Finally lets check whether we can do ‘unbounded’ iteration.

trait An extends Term {
  type ap[x <: Term] = x#ap[An]#eval
  type eval = An
}
// Infinite iteration: Smashes scalac's stack
  type NNn = b[R]#ap[b[R]]#ap[An]
  Equals[NNn#eval, c]

Well, we can ;-)

$ scalac SKI.scala
Exception in thread "main" java.lang.StackOverflowError
        at scala.tools.nsc.symtab.Types$SubstMap.apply(Types.scala:3165)
        at scala.tools.nsc.symtab.Types$SubstMap.apply(Types.scala:3136)
        at scala.tools.nsc.symtab.Types$TypeMap.mapOver(Types.scala:2735)
About these ads

Actions

Information

15 responses

29 01 2010
Henry Ware

Well done! Very cool.

29 01 2010
Rúnar

Magnificent.

30 01 2010
Daniel Spiewak

Wow. That’s very impressive! Did you have to use the -Yrecursion switch?

30 01 2010
michid

No, that’s without -Yrecursion.

30 01 2010
Daniel Spiewak

Words fail me.

1 02 2010
michid

AFAICS some things have changed with 2.8 regarding -Yrecursion. In many situation where I needed -Yrecursion before, the code compiles fine without it now.

31 01 2010
Tweets that mention Scala type level encoding of the SKI calculus « Michid’s Weblog -- Topsy.com

[…] This post was mentioned on Twitter by Daniel Spiewak, Daniel Spiewak, Daniel Spiewak, Planet Scala, Bubbl Scala Feed and others. Bubbl Scala Feed said: Scala type level encoding of the SKI calculus « Michid’s Weblog http://ff.im/-f9cFI […]

1 02 2010
Adriaan Moors

Cool! Didn’t know that was possible, actually :-)
Looks like syntax for anonymous type functions and/or partial type application could make this a little more pleasant… bumped them a little higher on my TODO list ;-)

2 02 2010
michid

Great, some syntax for partial type application would definitely help!

18 06 2010
Type Level Programming: Equality « Michid’s Weblog

[…] Level Programming: Equality 18 06 2010 Apocalisp has a great series on Type Level Programming with Scala. At some point the question came up whether it is possible to […]

5 12 2010
Schauderhaft » Is it Bad to Use Scala as Java with a More Concise Syntax?

[…] is cool you can prove the Scala type system is turing complete. I’m sure Monads are cool and useful thing, but I haven’t grasped them, and I know many […]

12 06 2011
Union types « Michid’s Weblog

[…] all types for which there is a corresponding type level acceptor function are expressible. Since type level calculations in Scala are Turing complete, it should be possible to find an acceptor for any recursive function. This means that – in […]

21 01 2013
Types Gone Wild! SKI at Compile-Time | Good Math, Bad Math

[…] seen this before, and it absolutely blew my mind. So I asked Jorge for a link to the proof. The link he sent me is a really beautiful blog post. It doesn't just prove that Scala type inference is Turing […]

28 02 2013
Artificial Intelligence Blog · Type Inference in Scala is Turing Complete

[…] “Scala type level encoding of the SKI calculus” at Michid’s Weblog; and […]

26 06 2013
Mixed-Site Variance in Kotlin | Project Kotlin

[…] too). In other words, subtyping is undecidable for Scala (in fact, Scala’s type system is Turing-complete, i.e. you can make Scala’s type checker perform any computation, including an infinite […]

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




Follow

Get every new post delivered to your Inbox.

%d bloggers like this: