Typinferenzsystemen

Typinferenzsysteme sind formale Mechanismen in statisch typisierten Programmiersprachen, die die Typen von Ausdrücken automatisch ableiten. Ziel ist es, den Programmieraufwand zu reduzieren, ohne Typensicherheit zu opfern. Typinferenz erfolgt typischerweise durch das Erzeugen von Typvariablen und Gleichungen über Ausdrücke und anschließendes Lösen per Unifikation, wodurch die allgemeinste Typisierung (principal type) ermittelt wird. Typen bleiben deklarativ, der Typ von Ausdrücken wird zur Kompilierzeit bestimmt. Typinferenz unterscheidet oft zwischen Inferenz und Typprüfung: Inferenz versucht, Typen zu bestimmen, Typprüfung überprüft explizite Typangaben.

Historisch bekanntes System ist Hindley-Milner (HM) mit dem Algorithmus W, der Polymorphismus durch Let-Polymorphismus ermöglicht. Es liefert für viele Ausdrücke eindeutig die allgemeinste Typisierung. Einschränkungen treten bei Subtyp-/Overloading-Features auf; HM lässt sich mit Erweiterungen kombinieren, etwa Typklassen in Haskell, Generics und GADTs. Sprachen der ML-Familie (ML, OCaml, Haskell) nutzen HM-ähnliche Systeme; Typinferenz wird auch in Sprachen wie Rust, Swift, Kotlin und TypeScript verwendet, oft mit bidirektionalem Typprüfung oder zusätzlichen Annotationen.

Vorteile: geringerer Annotierungsbedarf, frühzeitige Fehlererkennung, bessere Wartbarkeit. Grenzen: manche Typen erfordern explizite Annotationen, besonders bei komplexen Polymorphismusformen oder höheren Typen; Inferenzalgorithmen können Kompilierzeit erhöhen oder in bestimmten Fällen weniger flexibel sein.