使用类型系统实现计算模型

Question

使用任何现有的语言类型系统实现任何像图灵机那样强大的计算模型。

您的解决方案应该使用语言的类型系统来处理计算，而不是使用语言的常规图灵完整特性，也不应该使用宏系统。不过，只要程序的图灵完整性挂在类型系统上，就可以将语言的常规特性用于IO、典型样板等。

当然欢迎您使用需要编译器选项才能激活的可选类型系统特性。

请指定如何编程和运行您的机器，ala“在源代码中编辑这些数字/构造，编译它并运行它。”

例如，在实现脑盘中有一个C++模板元编程。事实上，brainfuck比需要的更复杂，因为它提供了与磁带分离的用户IO。一些简单的计算模型包括Brainfuck的祖先P“、λ-微积分、(2,3)图灵机和康威的生命游戏。

我们将宣布获胜者是最小化的人:他们的代码长度加上10倍的评论者声称他们已经知道该语言有一个图灵完整的类型系统。

Answer 1

我有限的Haskell-fu已经在Haskell的类型系统中实现了SK-微积分：

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))