The type system in Scala is Turing complete. Proof? Example? Benefits?
Language AgnosticScalaType SystemsTuring CompleteLanguage Agnostic Problem Overview
There are claims that Scala's type system is Turing complete. My questions are:

Is there a formal proof for this?

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

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.
Language Agnostic Solutions
Solution 1  Language Agnostic
There is a blog post somewhere with a typelevel implementation of the SKI combinator calculus, which is known to be Turingcomplete.
Turingcomplete type systems have basically the same benefits and drawbacks that Turingcomplete 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 typelevel computation are the new typepreserving 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 fixedwidth 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 typelevel functions. Thus, it is statically guaranteed to be typesafe, even though the types are actually computed and thus not known at design time.
Solution 2  Language Agnostic
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.