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.

  • 1
    \$\begingroup\$ 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? \$\endgroup\$ – ceased to turn counterclockwis Mar 30 '12 at 10:26
  • 1
    \$\begingroup\$ 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? \$\endgroup\$ – Jeff Burdges Mar 30 '12 at 12:08
  • 1
    \$\begingroup\$ Allright (for me), though it highly depends on many people participating. \$\endgroup\$ – ceased to turn counterclockwis Mar 30 '12 at 12:13
  • 1
    \$\begingroup\$ could you just give an example of a valid submission? \$\endgroup\$ – Ali1S232 Mar 31 '12 at 5:13
  • 1
    \$\begingroup\$ @JeffBurdges, the link you provide does not satisfy the challenge: arithmetic and logic are provided by the language and not the type system. \$\endgroup\$ – boothby Apr 4 '12 at 7:48

My limited Haskell-fu has come up with this implementation of SK-calculus in Haskell's type system:

data S = S
data K = K
data A l r = A l r

class C i o | i -> o
instance C (A (A K a) b) a
instance C (A (A (A S a) b) c) (A (A a c) (A b c))
  • \$\begingroup\$ 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) \$\endgroup\$ – Warbo Jun 29 '12 at 18:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.