# Implement a model of computation using a type system

Implement any model of computation as powerful as a Turing machine using any existing language's type system.

Your solution should handle the computation using the language's type system, not the language's regular Turing complete features, nor a macro system. It is however acceptable to use the language's regular features for IO, typical boilerplate, etc. so long as your program's Turing completeness hangs on the type system.

You are certainly welcome to use optional type system features that require compiler options to activate.

Please specify how to program and run your machine, ala "edit these numbers/constructs in the source, compile it and run it."

As an example, there is an implementation of brainfuck in C++ template meta-programming. In fact, brainfuck is more complex than necessary because it offers user IO separate from its tape. A few simpler models of computation include Brainfuck's ancestor P", λ-calculus, the (2,3) Turing Machine, and Conway's Game of Life.

We'll declare the winner to be whoever minimizes : their code's length plus 10 times the number of commenters who assert they already knew the language had a turing complete type system.

• I like the task, but the criteria don't seem very objective. Could you explain a bit more detailed how you intend to do the rating? – ceased to turn counterclockwis Mar 30 '12 at 10:26
• How about minimum of length plus 10 times the number of commenters who assert they already knew the language had a turing complete type system? Is that objective enough? – Jeff Burdges Mar 30 '12 at 12:08
• Allright (for me), though it highly depends on many people participating. – ceased to turn counterclockwis Mar 30 '12 at 12:13
• could you just give an example of a valid submission? – Ali1S232 Mar 31 '12 at 5:13
• @JeffBurdges, the link you provide does not satisfy the challenge: arithmetic and logic are provided by the language and not the type system. – boothby Apr 4 '12 at 7:48

• With these type declarations in place, we can define an identity function for pairs of combinator reductions: x :: C a b => (a, b) -> (a, b) x = id If we add "deriving Show" to the end of those "data" lines, then this works (ie. "((K S) K) reduces to S"): main = print $x ((A (A K S) K), S) Whilst this fails to compile, due to a type mismatch ("((K S) K) reduces to K", which is false): main = print$ x ((A (A K S) K), K) – Warbo Jun 29 '12 at 18:45