Y Combinator in Haskell

Question

Ist es möglich, die Y Combinator in Haskell zu schreiben?

Es scheint, als ob es einen unendlich rekursiven Typ hätte.

Y :: f -> b -> c 
where f :: (f -> b -> c) 

oder so etwas. Auch leicht eine einfache einkalkuliert faktorielles

factMaker _ 0 = 1 
factMaker fn n = n * ((fn fn) (n -1) 

{- to be called as 
(factMaker factMaker) 5 
-} 

nicht mit "Check Tritt: die unendliche Typ nicht konstruieren kann: t = t -> t 2 -> t1"

(Die Y Combinator sieht wie folgt aus

(define Y 
    (lambda (X) 
     ((lambda (procedure) 
     (X (lambda (arg) ((procedure procedure) arg)))) 
     (lambda (procedure) 
     (X (lambda (arg) ((procedure procedure) arg))))))) 

im Schema) Oder kurz und bündig mehr als

(λ (f) ((λ (x) (f (λ (a) ((x x) a)))) 
     (λ (x) (f (λ (a) ((x x) a)))))) 

Für die applicat ive Ordnung Und

(λ (f) ((λ (x) (f (x x))) 
     (λ (x) (f (x x))))) 

die nur eine eta Kontraktion weg für die Faulen Version.

Wenn Sie kurze Variablennamen bevorzugen.

Answer 1

Oh

this wiki page und This Stack Overflow answer scheinen meine Frage zu beantworten.
Ich werde später mehr von einer Erklärung aufschreiben.

Jetzt habe ich etwas Interessantes über diesen Mu-Typ gefunden. Betrachte S = Mu Bool.

data S = S (S -> Bool) 

Wenn man S als ein Satz behandelt und das Gleichheitszeichen als Isomorphismus, dann wird die Gleichung

S ⇋ S -> Bool ⇋ Powerset(S) 

So S die Menge von Sätzen ist, die ihren Powerset isomorph sind! Aber wir wissen aus Cantors Diagonalargument, dass die Kardinalität von Powerset (S) immer streng größer ist als die Kardinalität von S, daher sind sie niemals isomorph. Ich denke, das ist der Grund, warum Sie jetzt einen Fixpunktoperator definieren können, obwohl Sie ohne einen nicht können.

Answer 2

Hier ist eine nicht-rekursive Definition des Y-Combinator in Haskell:

newtype Mu a = Mu (Mu a -> a) 
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x) 

hat tip

Answer 3

Die kanonische Definition des Y Combinator ist wie folgt:

y = \f -> (\x -> f (x x)) (\x -> f (x x)) 

Aber es schreibt Haskell wegen der x x nicht ein, da es einen unendlichen Typ erfordern würde:

Wenn das Typsystem solche rekursiven Typen zulassen würde, würde dies die Typüberprüfung unentscheidbar machen (anfällig für Endlosschleifen).

Aber der Y-Kombinator funktioniert, wenn Sie es zu typecheck erzwingen, z. mit unsafeCoerce :: a -> b:

import Unsafe.Coerce 

y :: (a -> a) -> a 
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x)) 

main = putStrLn $ y ("circular reasoning works because " ++) 

Dies ist unsicher (offensichtlich). rampion's answer demonstriert eine sicherere Möglichkeit, einen Fixpunktkombinator in Haskell ohne Rekursion zu schreiben.

Answer 4

Der Y-Kombinator kann nicht mit Hindley-Milner-Typen typisiert werden, dem polymorphen Lambda-Kalkül, auf dem das Haskell-Typ-System basiert. Sie können dies durch Appell an die Regeln des Typsystems beweisen.

Ich weiß nicht, ob es möglich ist, den Y-Kombinator einzugeben, indem Sie ihm einen höherrangigen Typ geben. Es würde mich überraschen, aber ich habe keinen Beweis, dass das nicht möglich ist. (Der Schlüssel wäre, einen geeigneten polymorphen Typ für den Lambda-gebundenen x zu identifizieren.)

Wenn Sie einen Festkommaoperator in Haskell möchten, können Sie einen sehr einfach definieren, da in Haskell die Bindung fixiert wurde. Punkt Semantik:

fix :: (a -> a) -> a 
fix f = f (fix f) 

Sie können in gewohnter Weise nutzen diese Funktionen zu definieren und sogar einige endliche oder unendliche Datenstrukturen.

Es ist auch möglich, Funktionen auf rekursiven Typen zu verwenden, um Fixpunkte zu implementieren.

Wenn Sie an der Programmierung mit Festpunkten interessiert sind, möchten Sie Bruce McAdams technischen Bericht That About Wraps it Up lesen.