haskell - 在 Haskell 中实现 Iota

Question

Iota 是一种非常小的“编程语言”，只使用一个组合器。我有兴趣了解它的工作原理，但是以我熟悉的语言查看实现会很有帮助。

我找到了一个用 Scheme 编写的 Iota 编程语言的实现。不过，我在将其翻译成 Haskell 时遇到了一些麻烦。这很简单，但我对 Haskell 和 Scheme 都比较陌生。

您将如何在 Haskell 中编写等效的 Iota 实现？

(let iota ()
  (if (eq? #\* (read-char)) ((iota)(iota))
      (lambda (c) ((c (lambda (x) (lambda (y) (lambda (z) ((x z)(y z))))))
           (lambda (x) (lambda (y) x))))))

Answer 1

我一直在自学这些东西，所以我当然希望我能做对……

作为 n.m.提到，Haskell 是打字的事实对这个问题非常重要；类型系统限制了可以形成的表达式，特别是 lambda 演算的最基本类型系统禁止自我应用，这最终为您提供了一种非图灵完备的语言。图灵完备性被添加到基本类型系统之上，作为语言的一项额外功能(fix :: (a -> a) -> a 运算符或递归类型)。

这并不意味着你不能在 Haskell 中实现它，而是这样的实现不会只有一个操作符。

方法#1:实现 second example one-point combinatory logic basis from here , 并添加 fix功能:

iota' :: ((t1 -> t2 -> t1)
          -> ((t5 -> t4 -> t3) -> (t5 -> t4) -> t5 -> t3)
          -> (t6 -> t7 -> t6)
          -> t)
         -> t
iota' x = x k s k 
    where k x y = x
          s x y z = x z (y z)

fix :: (a -> a) -> a
fix f = let result = f result in result

现在你可以用 iota' 编写任何程序和 fix .解释这是如何工作的有点复杂。 ( 编辑: 请注意，此 iota' 与原始问题中的 λx.x S K 不同；它是 λx.x K S K ，这也是图灵完备的。 iota' 程序就是这种情况将不同于 iota 程序。我在 Haskell 中尝试了 iota = λx.x S K 定义；它会进行类型检查，但是当您尝试 k = iota (iota (iota iota)) 和 s = iota (iota (iota (iota iota))) 时会出现类型错误。)

方法#2:可以使用这种递归类型将无类型的 lambda 演算表示法嵌入到 Haskell 中:

newtype D = In { out :: D -> D }

D基本上是一种类型，其元素是来自 D 的函数至 D .我们有 In :: (D -> D) -> D转换 D -> D函数变成一个普通的 D , 和 out :: D -> (D -> D)做相反的事情。所以如果我们有 x :: D , 我们可以通过 out x x :: D 自行申请.

给它，现在我们可以写:

iota :: D
iota = In $ \x -> out (out x s) k
    where k = In $ \x -> In $ \y -> x
          s = In $ \x -> In $ \y -> In $ \z -> out (out x z) (out y z)

这需要来自 In 的一些“噪音”。和 out ; Haskell 仍然禁止你申请 D到 D , 但我们可以使用 In和 out解决这个问题。你实际上不能对 D 类型的值做任何有用的事情。 ，但您可以围绕相同的模式设计一个有用的类型。

编辑: iota 基本上是 λx.x S K , 其中 K = λx.λy.x和 S = λx.λy.λz.x z (y z) .即，iota 采用两个参数的函数并将其应用于 S 和 K；因此，通过传递一个返回其第一个参数的函数，您将获得 S，并通过传递一个返回其第二个参数的函数，您将获得 K。因此，如果您可以使用 iota 编写“返回第一个参数”和“返回第二个参数”，您可以用iota写S和K。但是 S and K are enough to get Turing completeness ，因此您还可以在讨价还价中获得图灵完备性。事实证明，您可以使用 iota 编写必要的选择器函数，因此 iota 足以实现图灵完备。

因此，这将理解 iota 的问题简化为理解 SK 演算。