Implementierung von Iota in Haskell

Question

Iota ist eine lächerlich kleine "Programmiersprache", die nur einen Kombinator verwendet. Ich bin daran interessiert zu verstehen, wie es funktioniert, aber es wäre hilfreich, die Implementierung in einer mir vertrauten Sprache zu sehen.

Ich fand eine Implementierung der Programmiersprache Iota in Scheme geschrieben. Ich habe ein wenig Mühe, es nach Haskell zu übersetzen. Es ist ziemlich einfach, aber ich bin relativ neu in Haskell und Scheme.

Wie würden Sie eine äquivalente Iota-Implementierung in Haskell schreiben?

(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

Ich habe mich etwas über dieses Thema unterrichtet, so dass ich hoffe, dass ich folgendes Recht bekommen ...

Als n.m. erwähnt, dass die Tatsache, dass Haskell getippt wird, für diese Frage von enormer Bedeutung ist; Typsysteme schränken ein, welche Ausdrücke gebildet werden können, und insbesondere die grundlegendsten Typsysteme für den Lambda-Kalkül verbieten die Selbstanwendung, was letztendlich zu einer nicht-Turing-vollständigen Sprache führt. Die Turing-Vollständigkeit wird oben des Basistypsystems als eine zusätzliche Eigenschaft der Sprache hinzugefügt (entweder ein fix :: (a -> a) -> a-Operator oder rekursive Typen).

Dies bedeutet nicht, dass Sie dies in Haskell überhaupt nicht implementieren können, sondern dass eine solche Implementierung nicht nur einen Operator hat.

Ansatz # 1: die second example one-point combinatory logic basis from here implementieren, und fügen Sie eine fix Funktion:

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 

Jetzt können Sie jedes Programm in Bezug auf iota' und fix schreiben. Zu erklären, wie das funktioniert, ist ein bisschen kompliziert. (EDIT:. beachten Sie, dass diese iota' ist nicht die gleiche wie die λx.x S K in der ursprünglichen Frage, es ist λx.x K S K, die auch Turing-complete Es ist der Fall, dass iota' Programme unterscheiden sich von iota Programme sein werden ich habe. in Haskell versucht, die iota = λx.x S K Definition, es typechecks, aber wenn man k = iota (iota (iota iota)) versuchen und s = iota (iota (iota (iota iota))) Sie Art Fehler erhalten)

Ansatz # 2:. Untypisierte Lambda-Kalkül Denotationen in Haskell werden können mit dieser rekursiven eingebettet:

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

ist im Grunde ein Typ, dessen Elemente Funktionen von bis sind. Wir haben In :: (D -> D) -> D, um eine D -> D Funktion in eine einfache umzuwandeln, und out :: D -> (D -> D), um das Gegenteil zu tun. Wenn wir also x :: D haben, können wir es selbst anwenden, indem wir out x x :: D tun.

dass Geben, jetzt können wir schreiben:

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) 

Dies erfordert einige "Rauschen" aus dem In und out; Haskell verbietet Ihnen immer noch, eine D auf eine D anzuwenden, aber wir können In und out verwenden, um dies zu umgehen.Mit Werten des Typs D können Sie nichts Nützliches tun, aber Sie könnten einen nützlichen Typ um das gleiche Muster herum entwickeln.

---

EDIT: Jota ist im Grunde λx.x S K, wo K = λx.λy.x und S = λx.λy.λz.x z (y z). D.h., Iota nimmt eine Zwei-Argument-Funktion und wendet sie auf S und K an; Wenn Sie also eine Funktion übergeben, die ihr erstes Argument zurückgibt, erhalten Sie S, und indem Sie eine Funktion übergeben, die ihr zweites Argument zurückgibt, erhalten Sie K. Wenn Sie also das "erste Argument zurückgeben" und das "zweite Argument zurückgeben" mit iota schreiben können kann S und K mit Iota schreiben. Aber S and K are enough to get Turing completeness, also bekommt man auch Turing-Vollständigkeit dazu. Es stellt sich heraus, dass Sie die erforderlichen Selektorfunktionen mit Iota schreiben können, so dass Iota für Turing-Vollständigkeit ausreicht.

So reduziert dies das Problem des Verständnisses von Iota zum Verständnis des SK-Kalküls.