[EDYCJA: Voilà kilka słów na każdym]
Istnieje kilka sposobów rozszerzenia wnioskowania o typ HM. Moja odpowiedź opiera się na wielu, mniej lub bardziej udanych, próbach wdrożenia niektórych z nich. Pierwszy, na który natknąłem się, to polimorfizm parametryczny . Systemy typu próbujące rozszerzyć HM w tym kierunku mają tendencję do Systemu F i dlatego wymagają adnotacji typu. Dwa znaczące rozszerzenia w tym kierunku, które spotkałem, to:
HMF, pozwala na wnioskowanie typu dla wszystkich typów System-F, co oznacza, że możesz mieć uniwersalną kwantyfikację „w środku” typu, ich wygląd nie jest domyślnie umieszczony w najwyższym zakresie, jak dla typów polimorficznych HM. Artykuł jasno stwierdza, że nie istnieje jasna reguła określająca, ile i gdzie adnotacje typu mogą być potrzebne. Również typy należące do Systemu F, terminy zwykle nie mają typu głównego.
MLF jest nie tylko rozszerzeniem HM, ale także rozszerzeniem Systemu F, który odzyskuje główną właściwość typu HM poprzez wprowadzenie pewnego rodzaju ograniczonej kwantyfikacji względem typów. Autorzy dokonali porównania, MLF jest silniejszy niż HMF, a adnotacje są wymagane tylko dla parametrów używanych polimorficznie.
Innym sposobem rozszerzenia HM jest zmiana domeny ograniczeń.
HM (X) jest sparametryzowany przez Hindleya-Milnera w domenie ograniczeń X. W tym podejściu algorytm HM generuje ograniczenia wysyłane do solvera domeny dla X. Dla zwykłego HM solver domeny jest procedurą unifikacji, a domena składa się z zestawu terminów zbudowanych z typów i zmiennych typu.
Innym przykładem X mogą być ograniczenia wyrażone w języku arytmetyki Presburger'a (w takim przypadku wnioskowanie / sprawdzanie typu jest rozstrzygalne) lub w języku arytmetyki Peano (już nie można rozstrzygać). X zmienia się w zależności od spektrum teorii, z których każda ma swoje własne wymagania dotyczące ilości i lokalizacji potrzebnych adnotacji typu i waha się od nie w ogóle do wszystkich.
Klasy typów Haskell są także rodzajem rozszerzenia domeny ograniczeń poprzez dodanie predykatów typu formy MyClass(MyType)(co oznacza, że istnieje instancja MyClass dla typu MyType).
Klasy typów zachowują wnioskowanie o typach, ponieważ są to (prawie) ortogonalne pojęcia, które realizują polimorfizm adhoc .
Jako przykład weźmy symbol valtypu val :: MyClass a => a, dla których można mieć wystąpień MyClass A, MyClass Bitd. Jeśli odnieść się do tego symbolu w kodzie, to faktycznie ponieważ typ wnioskowanie jest już wykonywana, że kompilator może wnioskować która instancję klasy do użytku. Oznacza to, że rodzaj valzależy od kontekstu, w którym jest używany. Dlatego też uruchomienie pojedynczych valinstrukcji prowadzi doambiguous type error : kompilator nie może wywnioskować żadnego typu na podstawie kontekstu.
W bardziej zaawansowanych systemach typów, takich jak GADT, rodziny typów, typy zależne, System (F) ω itd., Typy nie są już „typami”, lecz stają się złożonymi obiektami obliczeniowymi. Na przykład oznacza to, że dwa typy, które nie wyglądają tak samo, niekoniecznie są różne. Zatem równość typów nie jest wcale trywialna.
Aby dać przykład faktycznej złożoności, rozważmy zależny typ listy: NList a ngdzie ajest typ obiektów na liście i njego długość.
Funkcja dołączania miałaby typ, append :: NList a n -> NList a m -> NList a (n + m)a funkcja zip byłaby zip :: NList a n -> NList b n -> NList (a, b) n.
Wyobraź sobie, że teraz mamy lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Tutaj pierwszy argument zip jest typu, NList t (n + m)a drugi typu NList t (m + n).
Prawie to samo, ale jeśli sprawdzanie typów nie wie, że „+” dojeżdża do liczb naturalnych, musi odrzucić funkcję, ponieważ (n + m) nie jest dosłownie (m + n). Nie chodzi już o wnioskowanie typu / sprawdzanie typu, chodzi o udowodnienie twierdzenia.
Wydaje się, że typy płynów dokonują pewnych wnioskowania na temat typów zależnych. Ale, jak rozumiem, nie jest to tak naprawdę typ zależny, a bardziej jak zwykłe typy HM, na których dokonuje się dodatkowych wnioskowania w celu obliczenia granic statycznych.
Mam nadzieję, że to pomoże.