58

There are claims that Scala's type system is Turing complete. My questions are:

  1. Is there a formal proof for this?

  2. How would a simple computation look like in the Scala type system?

  3. Is this of any benefit to Scala - the language? Is this making Scala more "powerful" in some way compared languages without a Turing complete type system?

I guess this applies to languages and type systems in general.

Adrian
  • 3,762
  • 2
  • 31
  • 40

2 Answers2

39

There is a blog post somewhere with a type-level implementation of the SKI combinator calculus, which is known to be Turing-complete.

Turing-complete type systems have basically the same benefits and drawbacks that Turing-complete languages have: you can do anything, but you can prove very little. In particular, you cannot prove that you will actually eventually do something.

One example of type-level computation are the new type-preserving collection transformers in Scala 2.8. In Scala 2.8, methods like map, filter and so on are guaranteed to return a collection of the same type that they were called on. So, if you filter a Set[Int], you get back a Set[Int] and if you map a List[String] you get back a List[Whatever the return type of the anonymous function is].

Now, as you can see, map can actually transform the element type. So, what happens if the new element type cannot be represented with the original collection type? Example: a BitSet can only contain fixed-width integers. So, what happens if you have a BitSet[Short] and you map each number to its string representation?

someBitSet map { _.toString() }

The result would be a BitSet[String], but that's impossible. So, Scala chooses the most derived supertype of BitSet, which can hold a String, which in this case is a Set[String].

All of this computation is going on during compile time, or more precisely during type checking time, using type-level functions. Thus, it is statically guaranteed to be type-safe, even though the types are actually computed and thus not known at design time.

Jörg W Mittag
  • 363,080
  • 75
  • 446
  • 653
  • 15
    I imagine this is the blog post you were looking for? http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ . Scala seemed like a neat language when I first looked at it; that superclass-inference is a *really* cool feature. – Antal Spector-Zabusky Oct 28 '10 at 23:34
  • 6
    Excellent answer, though the collections example falls a bit short. While the type checker is certainly doing some interesting heuristics to get the best resultant collection type at compile time, it's not a good example of a type-level computation since the type system *itself* isn't really doing any work. Unfortunately (or perhaps, fortunately), there aren't many examples of real-world code that does actual type-level programming, simply because it's so hard, clunky and unmaintainable. – Daniel Spiewak Oct 29 '10 at 00:57
  • Thanks Jörg for the great example and Daniel for clarification. Now I am afraid to ask if the type checker is Turing Complete... – Adrian Oct 29 '10 at 19:41
34

My blog post on encoding the SKI calculus in the Scala type system shows Turing completeness.

For some simple type level computations there are also some examples on how to encode the natural numbers and addition/multiplication.

Finally there is a great series of articles on type level programming over on Apocalisp's blog.

michid
  • 10,536
  • 3
  • 32
  • 59
  • michid, that looks impressive. I promise to take a better look when I grow up... This may not be a FORMAL proof, but it may belong to this list? http://en.wikipedia.org/wiki/Computer-assisted_proof#List_of_theorems_proved_with_the_help_of_computer_programs – Adrian Oct 29 '10 at 19:51
  • 2
    @Adrian, the only known formal proof of turing completeness is the ability to implement something else that is turing complete. Typically this means a universal turing machine but the theory holds even if you use something else that is known to be turing complete like SKI calculus or Perl or Javascript. Therefore I would submit that this is a formal proof. – slebetman Oct 31 '10 at 20:43
  • 2
    It should also be noted that nothing practically implementable is really turing complete since it is impossible to have infinite memory. Even if you use up all matter in the universe to construct your CPU/interpreter it would still not really be turing complete. What we practically refer to as turing complete is really turing-complete-within-limits-of-available-memory. – slebetman Oct 31 '10 at 20:46