Typ-Inferenz für polymorphe Rekursion kodiert als Modul Rekursion

Question

Standard-ML hat keine polymorphe Rekursion. Das Hinzufügen einer Rekursion zu der Modulsprache ermöglicht es uns, polymorphe Rekursion als Spezialfall wiederherzustellen, wobei Fixpunkte von endofunctors verwendet werden. Zum Beispiel:

Es ist bekannt, dass polymorphe Rekursion Typinferenz unentscheidbar macht. Eine Funktordefinition enthält jedoch bereits partielle Typinformationen, nämlich die Signatur ihres Arguments. Reicht diese Information aus, um die Typrückschlüsse wieder entscheidbar zu machen?

Answer 1

Ja, da die Signatur eine "forward declaration" des polymorphen Typs bereitstellt, sodass sie nicht rekursiv abgeleitet werden muss. Außerdem benötigen Sie keinen Funktor, Sie können eine rekursive Strukturbindung direkt schreiben. Dies erfordert jedoch eine Signaturanmerkung und ist daher gleich.