haskell - 在Haskell中实现Iota

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

最佳答案

我一直在自学这些东西，所以我希望我能正确地做到以下几点...

下午提到，Haskell打字的事实对这个问题极为重要；类型系统限制可以形成哪些表达式，尤其是用于lambda演算的最基本的类型系统禁止自我应用，这最终给了您非图灵完整的语言。 Turing完整性作为语言的附加功能(在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编写任何程序。解释一下它是如何工作的。 (oz。在Haskell中尝试了iota'定义；它进行类型检查，但是当您尝试λx.x S K和λx.x K S K时，您会遇到类型错误。)

方法2:可以使用以下递归类型将未类型化的lambda演算符号嵌入到Haskell中:

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

iota'基本上是一种类型，其元素是从iota到iota = λx.x S K的函数。我们有k = iota (iota (iota iota))可以将s = iota (iota (iota (iota iota)))函数转换为普通的D，而D可以完成相反的操作。因此，如果我们有D，则可以通过执行In :: (D -> D) -> 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)

这需要从D -> D和D中获得一些“噪音”； Haskell仍然禁止您将out :: D -> (D -> D)应用于x :: D，但是我们可以使用out x x :: D和In来解决此问题。您实际上无法对out类型的值做任何有用的事情，但是可以围绕相同的模式设计一个有用的类型。

编辑: iota基本上是D，其中D和In。即，iota接受两个参数的函数，并将其应用于S和K；因此，通过传递一个返回其第一个参数的函数，您将得到S，而通过传递一个返回其第二个参数的函数，您将得到K。因此，如果您可以使用iota编写“返回第一个参数”和“返回第二个参数”，可以用iota来写S和K但是S and K are enough to get Turing completeness，因此您也可以通过讨价还价获得图灵完整性。事实证明，您可以使用iota编写必要的选择器函数，因此iota足以满足图灵完整性。

因此，这减少了从了解iota到了解SK微积分的问题。