Bei der Erläuterung des Y-Kombinators im Kontext von Haskell wird normalerweise darauf hingewiesen, dass die direkte Implementierung in Haskell aufgrund des rekursiven Typs keine Typprüfung durchführt.
Zum Beispiel von Rosettacode :
The obvious definition of the Y combinator in Haskell canot be used
because it contains an infinite recursive type (a = a -> b). Defining
a data type (Mu) allows this recursion to be broken.
newtype Mu a = Roll { unroll :: Mu a -> a }
fix :: (a -> a) -> a
fix = \f -> (\x -> f (unroll x x)) $ Roll (\x -> f (unroll x x))
Und in der Tat gibt die "offensichtliche" Definition keine Typprüfung aus:
λ> let fix f g = (\x -> \a -> f (x x) a) (\x -> \a -> f (x x) a) g
<interactive>:10:33:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
Expected type: t2 -> t0 -> t1
Actual type: (t2 -> t0 -> t1) -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a
<interactive>:10:57:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a
(0.01 secs, 1033328 bytes)
Die gleiche Einschränkung besteht in Ocaml:
utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
Error: This expression has type 'a -> 'b but an expression was expected of type 'a
The type variable 'a occurs inside 'a -> 'b
In Ocaml kann man jedoch rekursive Typen zulassen, indem man den -rectypesSchalter übergibt :
-rectypes
Allow arbitrary recursive types during type-checking. By default, only recursive
types where the recursion goes through an object type are supported.
Mit -rectypesfunktioniert alles:
utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
utop # let fact_improver partial n = if n = 0 then 1 else n*partial (n-1);;
val fact_improver : (int -> int) -> int -> int = <fun>
utop # (fix fact_improver) 5;;
- : int = 120
Da ich neugierig auf Typsysteme und Typinferenz bin, wirft dies einige Fragen auf, die ich immer noch nicht beantworten kann.
- Wie kommt die Typprüfung auf den Typ
t2 = t2 -> t0 -> t1? Nachdem ich diesen Typ gefunden habe, denke ich, besteht das Problem darin, dass sich type (t2) auf der rechten Seite auf sich selbst bezieht. - Zweitens, und vielleicht am interessantesten, was ist der Grund dafür, dass die Systeme vom Typ Haskell / Ocaml dies nicht zulassen? Ich vermute, es gibt einen guten Grund, da Ocaml es auch nicht standardmäßig zulässt, selbst wenn es mit rekursiven Typen umgehen kann, wenn der
-rectypesSchalter gegeben ist.
Wenn dies wirklich große Themen sind, würde ich Hinweise auf relevante Literatur schätzen.
In OCaml müssen Sie
-rectypesals Parameter an den Compiler übergeben (oder#rectypes;;in die oberste Ebene eingeben). Grob gesagt, wird dies während der Vereinigung deaktiviert. Die SituationThe type variable 'a occurs inside 'a -> 'bwird kein Problem mehr sein. Das Typensystem ist weiterhin "korrekt" (Ton usw.), die unendlichen Bäume, die als Typen entstehen, werden manchmal als "rationale Bäume" bezeichnet. Das Typsystem wird schwächer, dh es können keine Programmierfehler mehr erkannt werden.Weitere Informationen zu Fixpunktoperatoren mit Beispielen in OCaml finden Sie in meinem Vortrag zur Lambda- Berechnung (ab Folie 27).
quelle