Was sind die stärksten bekannten Typsysteme, für die eine Inferenz entscheidend ist?

Es ist bekannt, dass die Hindley-Milner-Typinferenz (der einfach typisierte Kalkulus mit Polymorphismus) eine entscheidbare Typinferenz aufweist: Sie können Prinziptypen für alle Programme ohne Anmerkungen rekonstruieren.$\lambda$

Das Hinzufügen von Haskell-Typenklassen scheint diese Entscheidbarkeit beizubehalten, aber weitere Hinzufügungen machen Rückschlüsse ohne Anmerkungen unentscheidbar (Typfamilien, GADTs, abhängige Typen, Rank-N-Typen, System usw.).$\omega$

Ich frage mich: Was sind die stärksten bekannten Typsysteme mit vollständig entscheidbarer Folgerung? Es wird irgendwo zwischen Hindley-Milner (völlig entscheidbar) und abhängigen Typen (völlig unentscheidbar) liegen. Gibt es Aspekte von DTs, die hinzugefügt werden können, um die Entscheidbarkeit von Inferenzen zu erhalten? Welche Untersuchungen wurden durchgeführt, um festzustellen, inwieweit dies vorangetrieben werden kann?

Mir ist klar, dass es kein einziges stärkstes System gibt, dass es wahrscheinlich unendlich kleine, inkrementelle Änderungen gibt, die zur Schlussfolgerung von HM hinzugefügt werden können. Es gibt jedoch wahrscheinlich einige praktische Kandidaten für Systeme, die entdeckt wurden.

Bearbeiten: Da es kein "stärkstes" System gibt, werde ich eine Antwort akzeptieren, die die bemerkenswerten Systeme, die Hindley Milner erweitern, mit entscheidbaren Schlussfolgerungen umreißt . Beispiele könnten Flüssigkeitstypen, Rang 2 usw. sein.

[EDIT: Voilà ein paar Worte zu jedem]

Es gibt verschiedene Möglichkeiten, die Inferenz des HM-Typs zu erweitern. Meine Antwort basiert auf vielen, mehr oder weniger erfolgreichen Versuchen, einige davon umzusetzen. Der erste, auf den ich gestoßen bin, ist der parametrische Polymorphismus . Typsysteme, die versuchen, HM in diese Richtung auszudehnen, tendieren zu System F und erfordern daher Typanmerkungen. Zwei bemerkenswerte Erweiterungen in dieser Richtung, auf die ich gestoßen bin, sind:

• HMF: Ermöglicht die Typinferenz für alle System-F-Typen. Dies bedeutet, dass Sie eine universelle Quantifizierung "in der Mitte" eines Typs durchführen können. Ihr Erscheinungsbild befindet sich nicht implizit im höchsten Bereich, wie dies bei polymorphen HM-Typen der Fall ist. In dem Papier wird klargestellt, dass es keine klare Regel dafür gibt, wie viele und wo Typanmerkungen erforderlich sind. Auch die Typen von System F haben normalerweise keinen Haupttyp.

• MLF ist nicht nur eine Erweiterung von HM, sondern auch eine Erweiterung von System F, mit der die Haupttyp-Eigenschaft von HM durch Einführung einer Art begrenzter Quantifizierung über Typen wiederhergestellt wird. Die Autoren haben einen Vergleich angestellt, MLF ist strikt leistungsfähiger als HMF und Anmerkungen sind nur für polymorph verwendete Parameter erforderlich.

Eine andere Möglichkeit, HM zu erweitern, besteht in der Variation der Einschränkungsdomäne.

• HM (X) wird nach Hindley-Milner über eine Einschränkungsdomäne X parametrisiert. Bei diesem Ansatz generiert der HM-Algorithmus die Einschränkungen, die an einen Domänenlöser für X gesendet werden. Für das übliche HM ist der Domänenlöser die Vereinigungsprozedur und die Domäne besteht der Menge von Begriffen aus den Typen und den Typvariablen bauen.
  Ein weiteres Beispiel für X könnten Einschränkungen sein, die in der Sprache der Presburger-Arithmetik (in welchem ​​Fall die Typinferenz / -prüfung entscheidbar ist) oder in der Sprache der Peano-Arithmetik (nicht mehr entscheidbar) ausgedrückt werden. X variiert entlang eines Spektrums von Theorien, wobei jede ihre eigenen Anforderungen hinsichtlich der Menge und Lokalisierung der benötigten Typanmerkungen hat und von überhaupt nicht bis zu allen reicht.

• Haskells Typklassen sind auch eine Art Erweiterung der Einschränkungsdomäne durch Hinzufügen von MyClass(MyType)Typprädikaten des Formulars (dh, es gibt eine Instanz von MyClass für den Typ MyType).
  Typklassen bewahren die Typinferenz, da es sich im Grunde genommen um (fast) orthogonale Konzepte handelt, die sie in Form eines Ad-hoc-Polymorphismus implementieren .
  Nehmen Sie als Beispiel ein Symbol valvom Typ, val :: MyClass a => afür das Sie Instanzen usw. haben MyClass Akönnen MyClass B. Wenn Sie in Ihrem Code auf dieses Symbol verweisen, kann der Compiler tatsächlich aufgrund der bereits durchgeführten Typinferenz auf die zu verwendende Instanz der Klasse schließen. Dies bedeutet, dass der Typ von valvon dem Kontext abhängt, in dem er verwendet wird. Das ist auch der Grund, warum das Ausführen einer einzelnen valAnweisung zu einer führtambiguous type error : Der Compiler kann basierend auf dem Kontext keinen Typ ableiten.

Für fortgeschrittenere Typsysteme wie GADTs, Typfamilien, abhängige Typen, System (F) ω usw. sind Typen keine "Typen" mehr, sondern werden zu komplexen Rechenobjekten. Zum Beispiel bedeutet dies, dass zwei Typen, die nicht gleich aussehen, nicht unbedingt unterschiedlich sind. So wird die Gleichheit der Typen (überhaupt) nicht trivial.

Um Ihnen ein Beispiel für die tatsächliche Komplexität zu geben, betrachten wir den abhängigen Listentyp: NList a nWo aist der Objekttyp in der Liste und wie lang nist er?
Die Append-Funktion hätte Typ append :: NList a n -> NList a m -> NList a (n + m)und die Zip-Funktion wäre zip :: NList a n -> NList b n -> NList (a, b) n.
Stellen Sie sich vor, wir haben jetzt den Lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Hier ist das erste Argument von zip vom Typ NList t (n + m)und das zweite vom Typ NList t (m + n).
Fast das Gleiche, aber wenn die Typprüfung nicht weiß, dass "+" auf natürlichen Zahlen pendelt, muss sie die Funktion ablehnen, da (n + m) nicht wörtlich (m + n) ist. Es geht nicht mehr um Typinferenz / Typprüfung, sondern um Theorembeweis.

Flüssigkeitstypen scheinen eine abhängige Typinferenz zu machen. Nach meinem Verständnis handelt es sich jedoch nicht wirklich um einen abhängigen Typ, sondern um einen HM-Typ, auf den zusätzliche Rückschlüsse gezogen werden, um statische Grenzen zu berechnen.

Ich hoffe das hilft.