在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

我一直在教自己一些这样的东西,所以我当然希望我得到以下正确的...

正如纳米提到的那样,输入Haskell的事实对这个问题非常重要; 类型系统限制可以形成的表达式,特别是lambda演算的最基本类型系统禁止自我应用,最终为您提供非图灵完整语言.图灵齐全性被添加到基本类型系统之上,作为语言的额外功能(fix :: (a -> a) -> a运算符或递归类型).

这并不意味着你不能在Haskell中实现这一点,而是这样的实现不会只有一个运算符.

方法#1:从这里实现第二个示例单点组合逻辑基础,并添加一个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也是Turing-complete.iota'程序将与iota程序不同.我iota = ?x.x S K在Haskell中尝试过这个定义;它typechecks,但是当你尝试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; 哈斯克尔仍然禁止你应用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和K足以让图灵完整,所以你也可以在交易中获得图灵的完整性.事实证明,您可以使用iota编写必需的选择器函数,因此iota足以满足图灵的完整性.

因此,这减少了理解iota以理解SK演算的问题.