Forschung zur Call-Site-basierten Typinferenz?

Ich versuche, mehr über Typprüfungs- und Typinferenzierungssysteme für das gesamte Programm zu erfahren, die Informationen von Funktionsaufrufseiten verwenden, um Typinformationen zu berechnen (zusätzlich zum Standardansatz der Verwendung des Funktionskörpers). Beispielsweise könnte ein solcher Algorithmus einen Funktionsaufruf verwenden, um daraus foo(1)zu schließen, dass die Funktion in fooganzzahlige Argumente akzeptiert. Offensichtlich würde dies die Folgerung sehr erschweren und die Prüfung nicht modular machen.

Wie auch immer, ich hatte nicht viel Glück, Nachforschungen zu diesem Ansatz anzustellen, wahrscheinlich weil ich nicht die richtige Terminologie kenne, um zu beschreiben, wovon ich spreche. Irgendwelche Hinweise?

Fast alle Systeme mit Typinferenz verwenden dazu Call-Site-Informationen. Beispiele umfassen Standard ML, OCaml, F # und Haskell. Viele andere Sprachen verwenden Call-Site-Informationen, um auf die Instanziierung von Typparametern zu schließen, z. B. Java, C #, Scala und Typed Racket. Dies wird häufig als "Local Type Inference" bezeichnet.

Ich würde nur beschreiben, wonach Sie suchen, als "Typinferenz", und Sie sollten wahrscheinlich zunächst nachschlagen, was allgemein als "Hindley-Milner" -System bekannt ist. Die Wikipedia- Seite bietet eine sinnvolle Einführung und Verweise auf die Originalarbeiten.

Der Ausgangspunkt für die lokale Typinferenz ist das Originalpapier von Pierce und Turner, das am besten in der TOPLAS 2000-Version ( ACM , PDF ) gelesen werden kann .

Sie können sich Typsysteme für Kreuzungstypen ansehen, die Ihnen so etwas wie geben können a :: Int -> Int | Bool -> Bool, damit Sie wissen, dass zwei Spezialisierungen ausreichen Intund Boolausreichen, oder eine übliche Typinferenz verwenden, um auf die meisten allgemeinen Typen zu schließen, gefolgt von einer Kontrollflussanalyse, um die tatsächlichen zu erfassen Typ Argumente. Tatsächlich gibt es hybride Ansätze (CFA ausgedrückt als Typensystem und umgekehrt).

Die Forschung arbeitet daran, auf die am wenigsten allgemeinen Typen anstatt auf die meisten allgemeinen Typen zu schließen, aber ich bin mir ihrer nicht bewusst.

Für Techniken zur Implementierung des Polymorphismus gibt es zwei Lösungen: 1) Spezialisierung (denken Sie an C ++ - Vorlagen) 2) Annahme einer einheitlichen Darstellung (denken Sie an Sammlungen im C-Stil mit void *).

Für 2 benötigen Sie den Typ von der Call-Site während der Typüberprüfung nicht und können die separate Kompilierung einfacher unterstützen.

Beachten Sie, dass es sich hier um parametrischen Polymorphismus handelt und dass virtuelle OO-Methodenaufrufe eine völlig andere Sache sind, die als Subtyp-Polymorphismus bezeichnet wird. Beachten Sie, dass C ++ - Vorlagen sowohl parametrischen Polymorphismus als auch Ententypisierung unterstützen, eine weitere Form des Polymorphismus.