Es gibt aktuelle Arbeiten von Paul-André Melliès und Noam Zeilberger , die dies untersuchen. Insbesondere sind die Arbeiten Functors Type Refinement Systems und An Isbell Duality Theorem for Type Refinement Systems . Es gibt auch ein Video von einem Vortrag über den ersten.
Ich denke, es gibt eine Menge Verwirrung um Verfeinerungstypen, weil Leute bestimmte Systeme als repräsentativ ansehen, was dazu führt, dass Ziele und Details dieser bestimmten Systeme der allgemeinen Idee zugeschrieben werden. Die Abkürzung ist, dass Typverfeinerungssysteme Begriffe klassifizieren, die unabhängig existieren, während (Nichtverfeinerungs-) Typen, abhängig oder auf andere Weise, Teil von Begriffen sind. Dies mag vertraut und möglicherweise sogar ein bisschen widersprüchlich klingen.
Der möglicherweise vertraute und möglicherweise widersprüchlich erscheinende Teil entsteht, wenn Sie Typen à la Curry (von außen) und Typen à la Church (von innen) betrachten. Wenn wir an Typen à la Curry denken, denken wir an Typen, die untypisierte Begriffe klassifizieren, die bereits eine Bedeutung haben. In Types à la Church existieren nur gut typisierte Ausdrücke, dh die Typbeschränkungen sind Teil unserer Syntax. Was ich damit sagen will, ist, dass ein Curry-Typ-System tatsächlich ein Typverfeinerungssystem ist, das untypisierte Begriffe verfeinert, während ein kirchliches Typsystem kein Typverfeinerungssystem ist. Dies bedeutet, dass wir uns zum Beispiel den einfach typisierten Lambda-Kalkül entweder als ein Typverfeinerungssystem oder als ein Nichtverfeinerungssystem vorstellen können.
Natürlich sagt niemand, dass unsere Begriffe untypisierte Begriffe sein müssen. Wir könnten genauso gut ein Typverfeinerungssystem auf typisierte Begriffe anwenden, und historisch gesehen ist dies der Kontext, in dem Verfeinerungstypen (mit diesem Namen) entstanden sind. Anwendungen für die weiche Typisierung veranschaulichen jedoch etwas, das der oben beschriebenen Situation näher kommt.
Bisher habe ich nichts über abhängige Typen gesagt. Der Grund ist, dass es sich um ein völlig orthogonales Problem handelt. Ich würde sagen, die archetypischen abhängigen Typensysteme werden normalerweise im kirchlichen Stil dargestellt und sind daher keine Typverfeinerungssysteme , sondern NuPRL (basierend auf Computational Type Theory , einer Variante der archetypischsten Theorie abhängiger Typen, Martin-Löf-Typentheorie). ist offensichtlich ein Verfeinerungssystem, wie ich es beschrieben habe. Begriffe , die in Nuprl können nicht einmal haben Typen! Zugegeben, die Tatsache, dass "PRL" für "Program Refinement Logic" steht, könnte ebenfalls ein Hinweis sein. Auf der anderen Seite beschreibt Refinement Types for ML ein Verfeinerungssystem, möglicherweise den Ursprung des Begriffs, das in keiner Weise ein abhängiges Typensystem ist.
Hoare-Tripel sind ein Verfeinerungssystem. Sie werden im ersten Artikel als Beispiel für ein Typverfeinerungssystem verwendet. Die Hoare-Typentheorie gibt jedoch etwas an, das als ein nicht verfeinertes Typensystem für eine Sprache mit Hoare-Tripeln angesehen werden kann.
Um eine Antwort auf die "Leistung" verschiedener Systeme zu erhalten, müssen Sie ein bestimmtes (eine Familie von) abhängigen Typsystemen und ein bestimmtes (eine Familie von) Verfeinerungssystemen angeben. Der Begriff "abhängiges Typsystem" deckt eine sehr breite Klasse von Typsystemen ab, und "Typverfeinerungssysteme" sind noch weiter gefasst. Selbst dann schließen sich die Begriffe nicht gegenseitig aus, sodass es sich nicht um einen Vergleich zwischen "abhängigen Typsystemen" und "Verfeinerungssystemen" handelt. Wenn Sie jedoch unter "abhängiges Typensystem" an etwas wie Coq denken und unter "Verfeinerungssystem" an etwas wie Flüssigtypendann ist es ziemlich einseitig. Coq wird allgemein als leistungsfähig genug angesehen, um praktisch die gesamte Mathematik in der Praxis zu beherrschen. Sie können einen SMT-Löser buchstäblich in Coq implementieren und nachweisen und ihn dann verwenden. und es kann ein sehr nahes Analogon zum Untergruppentyp formuliert werden. (NuPRL hat buchstäblich Subset-Typen.) Auf der anderen Seite sind SMT-Löser normalerweise auf entscheidbare Theorien beschränkt, bei denen Coq keine solche Einschränkung hat. und viele Systeme wie Liquid Types haben eine eingeschränkte und nicht erweiterbare Sprache zur Angabe von Prädikaten. (Natürlich könnten Sie mit "abhängiges Typsystem" "abhängiges ML" und mit "Typverfeinerungssystem" "NuPRL" [das auch ein abhängiges Typsystem ist] meinen, das auf die andere Weise einseitig wäre.)
