Sprawdzanie typów i typy rekurencyjne (Pisanie kombinatora Y w Haskell / Ocaml)

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 -rectypesprzełą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 -rectypeswszystko 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 -rectypesprzełącznik.

Jeśli są to naprawdę duże tematy, doceniłbym wskazówki do odpowiedniej literatury.

Po pierwsze błąd GHC,

GHC próbuje ujednolicić kilka ograniczeń x, po pierwsze, używamy go jako funkcji

x :: a -> b

Następnie używamy go jako wartości dla tej funkcji

x :: a

I w końcu ujednolicamy to z pierwotnym wyrażeniem argumentu tzw

x :: (a -> b) -> c -> d

Teraz x xstaje się jednak próbą zjednoczenia t2 -> t1 -> t0. Nie możemy tego zjednoczyć, ponieważ wymagałoby to zjednoczenia t2, pierwszego argumentu x, z x. Stąd nasz komunikat o błędzie.

Następnie dlaczego nie ogólne typy rekurencyjne. Pierwszą rzeczą, na którą warto zwrócić uwagę, jest różnica między typami rekurencyjnymi equi i iso,

• ekwirekurencyjne to, czego można się spodziewać, mu X . Typejest dokładnie równoważne dowolnemu rozszerzaniu lub składaniu.
• typy izo-rekurencyjne stanowią parę prowadzących, folda unfoldktóry i rozkâadanie rekurencyjnego definicje typów.

Teraz typy ekwirekurencyjne brzmią idealnie, ale absurdalnie trudno jest uzyskać właściwy układ w typach złożonych. Może sprawić, że sprawdzanie typu będzie nierozstrzygalne. Nie jestem zaznajomiony z każdym szczegółem systemu typów OCaml, ale w pełni równoważne typy w Haskell mogą powodować, że kontroler typów zapętla się arbitralnie, próbując ujednolicić typy, domyślnie Haskell zapewnia zakończenie sprawdzania typu. Co więcej, w Haskell synonimy typów są głupie, najbardziej przydatne typy rekurencyjne byłyby zdefiniowane tak type T = T -> (), jakkolwiek, są one jednak wstawiane prawie natychmiast w Haskell, ale nie można wstawić typu rekurencyjnego, jest nieskończony! Dlatego typy rekurencyjne w Haskell wymagałyby ogromnego przeglądu sposobu obsługi synonimów, prawdopodobnie nie warte wysiłku, aby wprowadzić je nawet jako rozszerzenie języka.

Iso-rekurencyjne typy są trochę uciążliwe w użyciu, musisz mniej więcej wyraźnie powiedzieć kontrolerowi typów, jak składać i rozkładać typy, co sprawia, że ​​twoje programy są bardziej skomplikowane w czytaniu i pisaniu.

Jest to jednak bardzo podobne do tego, co robisz ze swoim Mutypem. Rollskłada się i unrollrozwija. Tak naprawdę mamy wypieczone typy izo-rekurencyjne. Jednak typy ekwikursywne są po prostu zbyt złożone, więc systemy takie jak OCaml i Haskell zmuszają cię do przekazywania nawrotów przez punkty stałe na poziomie typu.

Teraz, jeśli Cię to interesuje, poleciłbym Typy i Języki programowania. Moja kopia siedzi na moich kolanach, pisząc to, aby upewnić się, że mam odpowiednią terminologię :)

W OCaml musisz przekazać -rectypeskompilator jako parametr (lub wpisać #rectypes;;najwyższy poziom). Z grubsza mówiąc, spowoduje to wyłączenie „kontroli sprawdzania” podczas unifikacji. Sytuacja The type variable 'a occurs inside 'a -> 'bnie 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.