scalaturing-completedotty

Will Scala 3 not be Turing complete?


I attended the following keynote on the future of Scala by Martin Odersky:

https://skillsmatter.com/skillscasts/8866-from-dot-to-dotty

At 1:01:00 an answer to an audience question seems to say that future Scala will not be Turing complete.

Did I understand this correctly? Will Scala 3 no longer be Turing complete? If so, what practical impact will this have on someone like me who uses Scala daily at work to solve practical problems? In other words, what do industrial Scala programmers loose and what do they gain by removing Turing completeness?


Solution

  • At 1:01:00 an answer to an audience question seems to say that future Scala will not be Turing complete.

    Did I understand this correctly? Will Scala 3 no longer be Turing complete?

    No, that's neither the question being asked nor the answer being given.

    Firstly: The question being asked is not whether Scala will not be Turing-complete, the question being asked is whether the Scala Type System will not be Turing-complete.

    Secondly: The answer being given is not that the Type System of future Scala will not be Turing-complete. Martin Odersky clearly says that with implicits, the Type System will definitely be Turing-complete, and without implicits, he doesn't want to make a prediction as to whether or not it will be Turing-complete.

    So, to answer your question:

    If so, what practical impact will this have on someone like me who uses Scala daily at work to solve practical problems?

    None whatsoever. First off, again, the Type System will still be Turing-complete because of implicits. And secondly, even it weren't, AFAIK, the Turing-completeness of Scala's Type System has not been used for anything pragmatically interesting. There are libraries which do perform sophisticated type-level computations, but those computations always terminate. Nobody has written a library which performs arbitrary Turing-complete computation at the type-level. (And in fact, it isn't even possible, because even though Scala's type system is Turing-complete, all currently existing implementations of Scala (there is only one anyway) have a strict limit on the recursion depth of the type checker).

    In other words, what do industrial Scala programmers loose and what do they gain by removing Turing completeness?

    Let's first talk about the type system: they don't lose anything. What they gain is the fact that compilation is guaranteed to terminate, and the fact that this means that the compiler can prove stuff about the program it couldn't prove otherwise.

    Let's also answer the hypothetical question: what if Scala weren't Turing-complete? Well, we could no longer write infinite loops. That's pretty much it. Note, however, that lots of things that are typically modeled as infinite loops (or infinite recursion) over data can still be modeled as finite co-recursion over co-data! (For example, an event loop in an Operating System, a Web Server, or a GUI.)

    OTOH, lots of things compilers can't do are "because it's equivalent to solving the Halting Problem". Well, in a language that isn't Turing-complete, the Halting Problem doesn't exist! So, the compiler can prove many more things about programs than it could in a Turing-complete language.

    But, to re-iterate: there are no plans of making Scala not Turing-complete. There are no plans of making implicits not Turing-complete. There are restrictions to the type system which may or may not make the type system not Turing-complete.