25

Scala uses a type-system based on System F ω, which is normally said to be strongly normalizing. Strongly normalizing implies non-Turing completeness.

Nevertheless, Scala's type-system is Turing-complete.

Which changes/additions/modifications make Scala's type-system Turing-complete compared to the formal algorithms and systems?

soc
  • 27,983
  • 20
  • 111
  • 215
  • 4
    Have links/references? (For spectators, like me :-) –  Dec 13 '11 at 23:42
  • 7
    The fact that System F is strongly normalizing implies that System F is not Turing complete. It does not imply that its type system isn't. And in fact it has been shown that [typechecking an unrestricted System F is undecidable](http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483) – sepp2k Dec 14 '11 at 00:20
  • @sepp2k -- yikes, the worst thing about Turing-completeness and it's got that. – Michael Lorton Dec 14 '11 at 01:52
  • 3
    @sepp2k, the result you cite holds only for undecorated lambda terms. If explicit types are given for lambda-abstracted type variables, and if type abstraction is explicit in the source code, then type checking System F is a snap---my students do it as a homework assignment. – Norman Ramsey Dec 14 '11 at 02:43
  • 2
    @pst http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ ; [messages 6,7](http://groups.google.com/group/scala-debate/browse_thread/thread/7a4c67fc76da4d1f/) ; http://www.scala-lang.org/node/7698 http://apocalisp.wordpress.com/2011/01/13/simple-ski-combinator-calculus-in-scalas-type-system/ – Gene T Dec 14 '11 at 05:17

1 Answers1

4

It's not a comprehensive answer but the reason is that you can define recursive types.

I've asked similar questions before (about what a non-Turing complete language might look like). The answers were of the form: a Turing complete language must support either arbitrary looping or recursion. Scala's type system supports the latter

Community
  • 1
  • 1
oxbow_lakes
  • 133,303
  • 56
  • 317
  • 449
  • 3
    Recursive types exist in most languages, including Java and Pascal. Any type that refers to itself (like a linked list) is recursive. You need a way to perform computation at the type level, such as type application. In Scala, you have type members and partial type application in type aliases. – Iulian Dragos Dec 14 '11 at 13:41
  • 2
    I meant recursive types in the sense of the peano encoding: http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/ using `type`, not `class` or `trait`. I thought that was reasonably obvious given the context. Like I said, I am echoing here, what I have been told about turing completeness. – oxbow_lakes Dec 14 '11 at 15:26
  • 1
    [Recursive types](http://en.wikipedia.org/wiki/Recursive_data_type) can be used to encode numbers like you say, but they're not enough for Turing completeness. What you want is a way to compute, in this case using type application (which in turn uses substitution). Scala's type members make it somewhat easy, though Java performs similar substitutions for generics. – Iulian Dragos Dec 15 '11 at 12:26