在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演算的理解問題。