在Haskell中实现Iota

Question

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

我发现在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定义;它typechecks，但是当你尝试k = iota (iota (iota iota))和s = iota (iota (iota (iota iota)))你得到类型错误）

方法2：

：非类型化演算denotations可以使用这个递归式嵌入哈斯克尔

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对于图灵完备性来说已经足够了。

因此，这减少了理解SK演算的理解问题。