在Haskell中实现Iota [英] Implementing Iota in Haskell

问题描述

Iota是一种使用只有一个组合器的可笑的小型编程语言。我有兴趣了解它是如何工作的，但以我熟悉的语言查看实现会很有帮助。

我找到了一个Iota用Scheme编写的编程语言。尽管我把它翻译成Haskell有点麻烦。这很简单，但我对Haskell和Scheme都比较陌生。

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

 （let iota（）
（if（eq？＃\ *（read-char））（（iota）（iota））
（lambda（c）（（c（lambda（x）（lambda（y）（lambda（z）（（xz）（yz））））））
（lambda（x）（lambda（y ）x））））））
  

解决方案

一直在教我自己的一些东西，所以我当然希望我能得到以下的权利......

由于nm提到，Haskell输入的事实对于这个问题是非常重要的。类型系统限制可以形成什么表达式，特别是lambda演算的最基本的类型系统禁止自我应用，这最终会给你一个非图灵完整的语言。图灵完整性被添加到基本类型系统的顶部作为该语言的一个额外功能（ fix ::（a - > a） - > a code>运算符或递归类型）。



这并不意味着你不能在Haskell中实现它，而是这样的实现不是将只有一个运营商。

方法1：执行第二个例子来自这里的一点组合逻辑基础，并添加一个 fix 函数： t2-> t1）
- >（（t5->> t1）>

  ; t4→t3）→t5→t4→t5→t3）
→（t6→t7→t6）
→> ; t）
  - > t 
 iota'x = x k s k 
其中k x y = x 
 s x y z = x z（y z）
 
 fix ::（a  - > a） - > a 
修复f = let结果= f导致结果
  

现在您可以编写任何程序根据 iota'和修正。解释这是如何工作的有点涉及。 （编辑：）注意这个 iota'与λx.xSK 在原始问题中，它是λx.xKSK ，它也是图灵完成的。 iota'程序将不同于 iota 程序。我已经尝试了 iota =λx.xSK 定义在Haskell中;它会检查类型，但是当你尝试 i c i ）））你会得到类型错误。）

方法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 xx :: D 来自行应用它。

现在我们可以写出：

  iota :: D 
 iota = In $ \x  - > out（out x s）k 
其中k = In $ \ x  - >在$ \y  - > x 
 s = In $ \x  - >在$ \y  - >在$ \z  - > out（out xz）（out yz）
  

这需要在和 out ; Haskell仍然禁止将 D 应用于 D ，但我们可以使用 In 和 out 来解决这个问题。您实际上无法对 D 类型的值进行任何有用的操作，但您可以围绕相同的模式设计一个有用的类型。

---

编辑： iota基本上是λx.xSK ，其中 K =λx.λy.x和 S =λx.λy.λz.xz（yz）。即，iota采用双参数函数并将其应用于S和K;所以通过传递一个返回第一个参数的函数得到S，并通过传递一个返回第二个参数的函数得到K.因此，如果你可以用iota写出返回第一个参数和返回第二个参数，那么你可以用iota写S和K.但是 S和K足以获得图灵的完整性，所以你也可以得到图灵的完整性在讨价还价。事实证明，你可以用iota编写必要的选择器函数，所以iota对于图灵完备性来说已经足够了。

因此这减少了理解iota的问题以理解SK微积分。

Iota is a ridiculously small "programming language" using only one combinator. I'm interested in understanding how it works, but it would be helpful to see the implementation in a language I'm familiar with.

I found an implementation of the Iota programming language written in Scheme. I've been having a little trouble translating it to Haskell though. It's rather simple, but I'm relatively new to both Haskell and Scheme.

How would you write an equivalent Iota implementation in Haskell?

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

解决方案

I've been teaching myself some of this stuff, so I sure hope I get the following right...

As n.m. mentions, the fact that Haskell is typed is of enormous importance to this question; type systems restrict what expressions can be formed, and in particular the most basic type systems for the lambda calculus forbid self-application, which ends up giving you a non-Turing complete language. Turing completeness is added on top of the basic type system as an extra feature to the language (either a fix :: (a -> a) -> a operator or recursive types).

This doesn't mean you can't implement this at all in Haskell, but rather that such an implementation is not going to have just one operator.

Approach #1: implement the second example one-point combinatory logic basis from here, and add a fix function:

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

Now you can write any program in terms of iota' and fix. Explaining how this works is a bit involved. (EDIT: note that this iota' is not the same as the λx.x S K in the original question; it's λx.x K S K, which is also Turing-complete. It is the case that iota' programs are going to be different from iota programs. I've tried the iota = λx.x S K definition in Haskell; it typechecks, but when you try k = iota (iota (iota iota)) and s = iota (iota (iota (iota iota))) you get type errors.)

Approach #2: Untyped lambda calculus denotations can be embedded into Haskell using this recursive type:

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

D is basically a type whose elements are functions from D to D. We have In :: (D -> D) -> D to convert a D -> D function into a plain D, and out :: D -> (D -> D) to do the opposite. So if we have x :: D, we can self-apply it by doing out x x :: D.

Give that, now we can write:

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)

This requires some "noise" from the In and out; Haskell still forbids you to apply a D to a D, but we can use In and out to get around this. You can't actually do anything useful with values of type D, but you could design a useful type around the same pattern.

---

EDIT: iota is basically λx.x S K, where K = λx.λy.x and S = λx.λy.λz.x z (y z). I.e., iota takes a two-argument function and applies it to S and K; so by passing a function that returns its first argument you get S, and by passing a function that returns its second argument you get K. So if you can write the "return first argument" and the "return second argument" with iota, you can write S and K with iota. But S and K are enough to get Turing completeness, so you also get Turing completeness in the bargain. It does turn out that you can write the requisite selector functions with iota, so iota is enough for Turing completeness.

So this reduces the problem of understanding iota to understanding the SK calculus.

这篇关于在Haskell中实现Iota的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！