Zrozumienie wielościpów w Hindley-Milner Typ Wnioskowanie

Question

Czytam artykuł z Wikipedii na temat Hindley–Milner Type Inference próbując zrozumieć. Do tej pory to właśnie zrozumiałem:

1. Typy są klasyfikowane jako monotypy lub poliakty.
2. Monotypy są dalej klasyfikowane jako stałe typu (np. int lub string) lub zmienne typu (takie jak α i β).
3. Stałe mogą być typu betonu (np. int i string) lub konstruktorów typów (takich jak Map i Set).
4. Zmienne typu (takie jak α i β) zachowują się jak symbole zastępcze dla konkretnych typów (np. int i string).

Teraz mam trochę trudności ze zrozumieniem polytypes ale po naukę trochę Haskell jest to, co mam zrobić z nim:

1. Rodzaje sami mają typy. Formalne typy typów są nazywane rodzajami (tj. Istnieją różne rodzaje typów).
2. rodzaje betonu (jak int i string) i typ zmiennych (jak α i β) są od rodzaju *.
3. typu konstruktory (jak Map i Set) są lambda abstrakcje rodzajów (np Set jest rodzaju * -> * i Map jest rodzaju * -> * -> *).

To, czego nie rozumiem, to co oznaczają kwalifikatory. Na przykład co reprezentuje ∀α.σ? I nie wydaje się, aby monetą z niego i bardziej czytam dodaje się ustęp bardziej zdezorientowany uzyskać:

Funkcja z polytype ∀α.α -> α przez kontrast może odwzoruj dla siebie każdą wartość tego samego typu, a wartość identity function jest wartością dla tego typu. Jako inny przykład: ∀α. (Set α) -> int to typ funkcji odwzorowującej wszystkie zbiory skończone na liczby całkowite. Liczba członków jest wartością dla tego typu. Zauważ, że kwalifikatory mogą pojawiać się tylko na najwyższym poziomie, np. Na przykład typ ∀α.α -> ∀α.α jest wykluczony przez składnię typów i te monotypy są zawarte w typach, więc typ ma ogólny formularz ∀α₁. . . ∀αₙ.τ.

Answer 1

Po pierwsze, rodzaje i typy polimorficzne to różne rzeczy. Możesz mieć system typu HM, w którym wszystkie rodzaje są tego samego rodzaju (*), możesz również mieć system bez polimorfizmu, ale o złożonych rodzajach.

Jeśli termin M jest typu ∀a.t, oznacza to, że dla każdego typu s możemy zastąpić s dla a w t (często zapisywane jako t[a:=s] i musimy że M jest typu t[a:=s]. Jest nieco podobny do logika, gdzie możemy podstawić dowolny termin dla zmiennej powszechnie ilościowo, ale tutaj mamy do czynienia z typami.

to jest właśnie to, co dzieje się w Haskell, tylko że w Haskell nie widać kwantyfikatorów. wszystko zmienne typu pojawiające się w sygnaturze typu są domyślnie kwantyfikowane, po prostu a s, jeśli masz przed sobą typ forall. Na przykład, map musiałby typ

map :: forall a . forall b . (a -> b) -> [a] -> [b] 

itd. Bez tego utajonego kwantyfikator ogólny, zmienne typu a i b musiałby mieć jakieś stałe znaczenie i map nie będzie polimorficzny.

Algorytm HM wyróżnia rodzaje (bez kwantyfikatorów, monotypy) i typu schematy (universaly ilościowo rodzaje, polytypes). Ważne jest, aby w niektórych miejscach używać schematów typu (jak w let), ale w innych miejscach dozwolone są tylko typy. To sprawia, że ​​cała sprawa jest rozstrzygająca.

Proponuję również przeczytać artykuł o System F. Jest to bardziej złożony system, który pozwala na dowolne typy (w związku z czym wszystko jest nazywane typ), ale typ wnioskowania/sprawdzania jest nierozstrzygalny. Pomoże Ci zrozumieć, jak działa forall. System F jest szczegółowo opisany w Girard, Lafont i Taylor, Proofs and Types.

Answer 2

Zastanów się l = \x -> t w Haskell. Jest to lambda, która reprezentuje określenie t ze zmienną x, która zostanie później podstawiona (na przykład l 1, cokolwiek by to miało znaczyć). Podobnie, ∀α.σ reprezentuje typ ze zmienną typu α, to jest f : ∀α.σ, jeżeli funkcja jest sparametryzowana przez typ α. W pewnym sensie, σ zależy od α, więc f zwraca wartość typu σ(α), gdzie α zostanie podstawiony później w σ(α), a otrzymamy konkretny typ.

W języku Haskell można pominąć ∀ i zdefiniować funkcje podobnie jak id : a -> a. Powodem dopuszczenia pominięcia kwantyfikatora jest to, że są dozwolone tylko na najwyższym poziomie (bez rozszerzenia RankNTypes). Można spróbować ten kawałek kodu:

id2 : a -> a -- I named it id2 since id is already defined in Prelude 
id2 x = x 

Jeśli zapytać ghci dla typu id (:t id), zwróci a -> a. Aby być bardziej precyzyjnym (więcej typów teoretycznych), id ma typ ∀a. a -> a.Teraz, jeśli dodać do kodu:

val = id2 3 

, 3 ma typ Int, więc typ Int zostaną podstawione do σ i otrzymamy konkretny typ Int -> Int.