在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演算的问题。