Y Combinator in Haskell

Question

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

Es scheint, wie es eine unendlich rekursive Art haben würde.

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

oder so etwas. Auch leicht ein einfach faktorisierter faktorielles

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

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

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

(Die Y Combinator wie folgt aussieht

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

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

Für die applicative bestellen Und

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

Was für die Faulen Version nur eta Kontraktion entfernt ist.

Wenn Sie kurze Variablennamen bevorzugen.

Answer 1

Oh

diese Wikiseite Diese Antwort Stack-Überlaufes scheint meine Frage zu beantworten.
Ich werde schreiben, bis mehr eine Erklärung später.

Nun, ich habe festgestellt, etwas interessantes dieses Typs Mu. Betrachten wir S = Mu Bool.

data S = S (S -> Bool)

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

S ⇋ S -> Bool ⇋ Powerset(S)

So S ist die Menge von Sätzen, die auf ihre Powerset isomorph sind! Aber wir wissen aus Cantors Diagonal Argumente, dass die Mächtigkeit von Powerset (S) ist immer streng größer als die Mächtigkeit von S, so sind sie nie isomorph. Ich denke, das ist, warum können Sie jetzt einen festen Punkt Operator definieren, auch wenn man nicht ohne.

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)

Hutspitze

Answer 3

Das Y Combinator kann nicht Hindley-Milner-Typen eingegeben wird unter Verwendung des polymorphe Lambda-Kalkül, auf dem Haskell Typ-System basiert. Sie können dies den Regeln des Typsystems durch Anziehungskraft unter Beweis stellen.

Ich weiß nicht, ob es möglich ist, die Y Combinator eingeben, indem er einen höherrangigen Art geben. Es wäre überrascht mich, aber ich habe keinen Beweis dafür, dass es nicht möglich ist. (Der Schlüssel wäre ein geeigneter polymorphen Typ für die Lambda-gebundenen x zu identifizieren.)

Wenn Sie einen Festpunkt-Operator in Haskell wollen, können Sie eine Definition sehr einfach, weil in Haskell, let-Bindung hat Festpunkt Semantik:

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

Sie können dies in der üblichen Art und Weise verwenden Funktionen zu definieren und sogar einige endliche oder unendliche Datenstrukturen.

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

Wenn Sie in die Programmierung mit Fixpunkten interessiert sind, möchten Sie Bruce McAdam technischen Bericht das über Wraps it Up .

Answer 4

Die kanonische Definition des Y-Kombinator ist wie folgt:

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

Aber es gibt nicht Scheck in Haskell wegen des x x, da es eine unendliche Art erfordern würde:

x :: a -> b -- x is a function
x :: a      -- x is applied to x
--------------------------------
a = a -> b  -- infinite type

Wenn das Typsystem waren solche rekursive Typen zu ermöglichen, wäre es Art Überprüfung unentscheidbar (anfällig für Endlosschleifen) machen.

Aber die Y Combinator wird funktionieren, wenn Sie es zwingen, typecheck, z.B. unter Verwendung von 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 Antwort zeigt einen sichereren Weg, um einen Fixpunkt-Kombinator in Haskell zu schreiben, ohne Rekursion.