The Ceylon type system is Turing complete

[Lucas Werkmeister]

Hi all!

I wanted to inform y’all that the Ceylon type system is Turing complete. If you’re not familiar with CS theory, this essentially means that in theory, you can do any computation in the Ceylon type system; everything that your computer can do – add two integers, render the Mandelbrot set, verify a digital signature, encrypt data, play Doom – can in principle also be done by the Ceylon type system: It’s possible to produce a huge program where an initial value is formed from some representation of your input, and in the end you have a value where if you let the IDE insert the type inferred by the typechecker, that’s a representation of the output. (In practice, larger calculations will crash the typechecker – in my experience with an OutOfMemoryException.)

For example, I can create a program that is well-typed if and only if the input length is a power of two: I assign the final (output) value to a value of type Assign, and this value and everything else is defined in such a way that this assignment is valid if and only if the input is valid. That program is generated using ceylon.ast here (the Turing machine generator is here), and fed directly into the typechecker here. If I stick it into the formatter instead, we can see the Ceylon code: gist

How does this work? I’ve made several attempts at explaining it; the most recent one is in this package documentation (copy+pasted into a Markdown processor here); earlier attempts are here and here. I really hope this is understandable, because in my opinion this is awesome, and I want other people to understand it :)
In a nutshell, it uses a combination of Ceylon features: first class union and intersection types, the fact that the Nothing type is really empty (i. e. null safety), parametric polymorphism (i. e. generics), and full type inference (including type arguments). I don’t think it’s possible to emulate a Turing machine like this in any other language (although it’s probably possible in some other way in some other languages).

This is kind of a continuation of this post from about ¾ of a year ago; back then I demonstrated that the Ceylon type system is Chomsky-3 complete (Turing completeness is Chomsky-0, much more powerful).

If you have any questions, please ask away :)

Best regards,
Lucas

[Enrique Zamudio]

Well supposedly the Scala typesystem is also Turing-complete, which I had taken to mean you could write undecidable statements in it, which I consider a Bad Thing™... so does this mean we can now write undecidable statements within the type system? I thought Gavin worked hard to avoid precisely that...

[Lucas Werkmeister]

No, it’s not undecidable… the generated code contains one statement per Turing machine iteration, so the complexity is linear to the program size. (I’ve also argued that a more powerful type system would be bad here.)

[Enrique Zamudio]

Ah, I hadn't read this other link, very interesting.

[Emmanuel Bernard]

Out of curiosity, what are the list of know turing complete type systems?

Emmanuel

--
You received this message because you are subscribed to the Google Groups "ceylon-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/c3ed0168-45a1-4232-b6e1-ead62815c3ae%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Lucas Werkmeister]

 I found these with Google (probably incomplete):

• Scala: Type level encoding of the SKI calculus
• Haskell: Embedding the SK combinator calculus; Direct implementation of a Turing machine
• C++: C++ Templates are Turing Complete

As far as I can tell (I haven’t looked into it too much), these all feature constant-size programs, demonstrating that compilation of these languages is undecidable. This is significantly more powerful than what I’m doing here (too powerful in my opinion, but that’s a question of personal taste).

This seems a lot more similar to what I’m doing: Is the C99 preprocessor Turing complete? Apparently, it is if you supply an external loop to feed the preprocessor back into itself, or if you define that loop in the program via additional statements.

Any other examples?

[Ross Tate]

So, generally the statement "Ceylon's type system is Turing complete" is interpreted to mean that there is a function from Turing machines to Ceylon programs such that a Turing machine answers yes (on the empty input) if and only if the corresponding program type checks. The corollary of this is that type checking is undecidable. So, this effort is pretty snazzy, but you're misrepresenting it, which needlessly set off a bunch of alarms and made me take a while to figure out what you were doing because I was expecting something very different. I'd be interested to understand the terminology for what you've actually proved. That is, what is the computational power you've demonstrated Ceylon's type system has?

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/61737937-4a1b-4777-a80f-1689963c62aa%40googlegroups.com.

[Lucas Werkmeister]

There is a pair of functions:
One from a Turing machine to a Ceylon program, and one from the input to the Turing machine plus the number of desired iterations to another Ceylon program.
The two functions operate independently (else we could obviously cheat by doing the work in the functions). The second program uses declarations from the first, and will be well-typed iff the Turing machine from the first program accepts the input from the second program after the desired number of iterations.

(I suppose you can skip the input by encoding it into n initial states of the Turing machine that just fill the tape with the input.)

So the difference is that the number of iterations the typechecker performs is strictly limited, and is linear in the size of the second program (the “driver”, perhaps). (If you simplify them, the involved types don’t grow, so I don’t think the typechecker uses more than a linear amount of memory either.)

I’m not sure what to call that. In analogy to a real machine, you could perhaps call the first program a Turing machine without a power supply or clock or something. Perhaps the best characterization is “you can store the entire state (including tape) of a Turing machine in a type, and define a function that performs a single iteration”, because that’s pretty much what I’m doing.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CABnofR5M7qQ_wu%3DePq_3kas-3v4%3Dy4DiFV%3DL7HUBF-77Pd71vQ%40mail.gmail.com.