4
\$\begingroup\$

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.

Improve this question
\$\endgroup\$
10
  • 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
    Commented Mar 30, 2012 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
    Commented Mar 30, 2012 at 12:08
  • 1
    \$\begingroup\$ Allright (for me), though it highly depends on many people participating. \$\endgroup\$
    – ceased to turn counterclockwis
    Commented Mar 30, 2012 at 12:13
  • 1
    \$\begingroup\$ could you just give an example of a valid submission? \$\endgroup\$
    – Ali1S232
    Commented Mar 31, 2012 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
    Commented Apr 4, 2012 at 7:48

1 Answer 1

Reset to default
4
\$\begingroup\$

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))
Improve this answer
\$\endgroup\$
1
  • \$\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
    Commented Jun 29, 2012 at 18:45

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