Wyjaśniając kombinator Y w kontekście Haskell, zwykle zauważa się, że prosta implementacja nie będzie sprawdzać typu w Haskell ze względu na jego typ rekurencyjny.
Na przykład z 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))
I rzeczywiście, „oczywista” definicja nie sprawdza typu:
λ> 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)
To samo ograniczenie istnieje w 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
Jednak w Ocaml można zezwolić na typy rekurencyjne, przekazując -rectypes
przełącznik:
-rectypes
Allow arbitrary recursive types during type-checking. By default, only recursive
types where the recursion goes through an object type are supported.
Przy użyciu -rectypes
wszystko działa:
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
Ciekawość systemów typów i wnioskowania o typach rodzi pytania, na które wciąż nie jestem w stanie odpowiedzieć.
- Po pierwsze, w jaki sposób moduł sprawdzania typu wymyśla typ
t2 = t2 -> t0 -> t1
? Po wymyśleniu tego typu wydaje mi się, że problem polega na tym, że typ (t2
) odnosi się do siebie po prawej stronie? - Po drugie, być może najciekawsze, jaki jest powód, dla którego systemy typu Haskell / Ocaml tego nie dopuszczają? Sądzę, że jest dobry powód, ponieważ Ocaml również domyślnie nie zezwala na to, nawet jeśli może poradzić sobie z typami rekurencyjnymi, jeśli zostanie podany
-rectypes
przełącznik.
Jeśli są to naprawdę duże tematy, doceniłbym wskazówki do odpowiedniej literatury.
W OCaml musisz przekazać
-rectypes
kompilator jako parametr (lub wpisać#rectypes;;
najwyższy poziom). Z grubsza mówiąc, spowoduje to wyłączenie „kontroli sprawdzania” podczas unifikacji. SytuacjaThe type variable 'a occurs inside 'a -> 'b
nie będzie już problemem. System typów nadal będzie „poprawny” (dźwięk itp.), Nieskończone drzewa powstające jako typy są czasem nazywane „drzewami racjonalnymi”. System typów słabnie, tzn. Niemożliwe jest wykrycie niektórych błędów programisty.Zobacz mój wykład na temat rachunku lambda (od slajdu 27), aby uzyskać więcej informacji na temat operatorów punktów stałych z przykładami w OCaml.
źródło