Ich habe ein Forschungspapier über Haskell und die Implementierung von HList gelesen und mich gefragt, wann die beschriebenen Techniken für den Typprüfer entscheidbar sind und wann nicht. Da man ähnliche Dinge mit GADTs machen kann, habe ich mich außerdem gefragt, ob die Typüberprüfung von GADTs immer entscheidbar ist.
Ich würde Zitate bevorzugen, wenn Sie sie haben, damit ich die Erklärungen lesen/verstehen kann.
Gracias.
Ich glaube, dass die GADT-Typüberprüfung immer entscheidbar ist; es ist die Inferenz, die unentscheidbar ist, da sie eine Vereinheitlichung höherer Ordnung erfordert. Aber ein GADT-Typ-Prüfer ist eine eingeschränkte Form der Proof-Checker, die man z.B. in Coq sieht, wo die Konstruktoren den Proof-Term aufbauen. Das klassische Beispiel für die Einbettung des Lambda-Kalküls in GADTs hat zum Beispiel einen Konstruktor für jeden Reduzierungsregel Wenn Sie also die Normalform eines Begriffs finden wollen, müssen Sie ihm sagen, welche Konstruktoren Sie zu ihr führen. Das Halteproblem wurde in die Hände des Benutzers verlagert :-)
Sie haben das wahrscheinlich schon gesehen, aber es gibt eine Sammlung von Papieren zu diesem Thema bei Microsoft Research: Typ Kontrollpapiere . Der erste beschreibt den dezidierbaren Algorithmus, der im Glasgow-Haskell-Compiler verwendet wird.
CodeJaeger ist eine Gemeinschaft für Programmierer, die täglich Hilfe erhalten..
Wir haben viele Inhalte, und Sie können auch Ihre eigenen Fragen stellen oder die Fragen anderer Leute lösen.
