Hindley Milner Typ Inferenz
 
StartSeite | Neues | TestSeite | ForumSeite | Teilnehmer | Kategorien | Index | Hilfe | Einstellungen | Ändern

Hindley-Milner-Typsystem

Hindley und Milner entwickelten dieses Typsystem, Erweiterungen davon bilden die Basis von Standard ML, Haskell und einigen anderen funktionalen Programmiersprachen. Das besondere am Hindley-Milner-Typsystem ist, dass jedes Stück Code genau einen allgemeinsten Typ besitzt, und dass es einen Algorithmus, eben die HindleyMilnerTypInferenz, gibt, der diesen allgemeinsten Typ findet. Typen sind:

Das ist schon alles! Funktionen mit mehreren Argumenten braucht man nicht, man nimmt einfach eine Funktion mit einem Argument, deren Ergebnis eine Funktion ist (a -> b -> c == a -> (b -> c)).

Typinferenz

Die Inferenz (ist Typabgleich eine gute Übersetzung?) selbst ist auch recht einfach. Alle Variablen im Programm erhalten zunächst den Typ "a" (a ist eine noch unbenutzte Typvariable), alle Funktionen haben bereits einen, ebenso Konstanten und Datenkonstruktoren. Jetzt werden Typregeln angewandt, die dazu führen, dass bestimmte Typen gleich sein müssen. Tatsächlich sind es nur zwei Regeln: eine Funktion muss auf ihren Argumenttyp angewandt werden und beide gemeinsam haben den Ergebnistyp und eine weitere Regel für rekursive Aufrufe. Sollen zwei Typen gleich sein, werden sie gleichgesetzt, damit werden die Variablen an Typen gebunden. Klappt das Gleichsetzen (unification), sind am Ende die Variablen an den allgemeinsten Typ gebunden. Klappt sie nicht, gibt es gar keinen Typ, das Programm ist falsch.

In Haskell gibt es außerdem noch Typklassen. Normalerweise passt eine Typvariable auf jeden Typ. Sie kann aber eingeschränkt werden, so dass sie nur noch auf einen Typ der entsprechenden Klasse passt. Typen gelangen in eine Klasse, indem man deklariert, dass der Typ zu der Klasse gehört und die erforderlichen Methoden implementiert.

Beispiele

Im praktischen Einsatz: Das Hindley-Milner-Typsystem besitzt Typkonstruktoren mit Parametern. So ist etwa eine Liste ein polymorpher Typ:

 data List a = Nil | Cons a (List a) 

zu lesen als "für beliebige Typen a ist eine Liste von Typ-a-Werten entweder leer (Nil) oder die Verkettung (Cons wie construct) eines Elementes vom Typ a mit einer Liste über den Typ a". Man kann es auch so lesen: Nil ist das Listenende, Cons sagt dass noch ein Element kommt und es danach weiter geht. Funktionen können demzufolge auch polymorph sein:

 length :: List a -> Integer 

"für jeden Typ a ist length eine Funktion, die Listen über den Typ a auf ganze Zahlen abbildet". Das geht auch mit mehreren Parametern. In Haskell kann man außerdem die Polymorphie durch Typklassen einschränken, etwa so, dass nur Typen erlaubt sind, die Zahlen darstellen, und die man folgerichtig addieren kann. Das entscheidende ist jetzt, dass jeder Ausdruck in diesem System einen "allgemeinsten Typ" besitzt, der automatisch ermittelt werden kann. Genau dazu muß ein Haskell-Compiler in der Lage sein. Deshalb sind Typdeklarationen in der Regel redundant, mehr Typdeklarationen führen aber oft zu genaueren Fehlermeldungen. Haskell kennt übrigens keinen Type-Cast, und ich hab ihn auch noch nie vermißt.

Das Zusammenspiel von Einschränkung und Inferenz habe ich noch nicht kapiert. Was sind denn die Typen einer sortierten Liste (Elemente implementieren Vergleich auf Kleiner), einer Hashtabelle und eines Wörterbuches (Elemente implementieren eine Hashfunktion)?

Typen mit eingeschränkter Polymorphie sind erlaubt, aber eigentlich Unsinn. Manchmal möchte man eine Absicht ausdrücken machen, und dann deklariert man ein Wörterbuch vielleicht so:

 data (Ord key, Eq value) => FiniteMap key value = ... 

Sinnvoller ist das bei Funktionen. Nehmen wir eine Funktion zum Sortieren einer Liste:

 sort :: Ord a => [a] -> [a] 

zu lesen als "für jeden Typ a mit einer Ordnung (Klasse Ord) ist sort eine Funktion, welche eine Liste über dem Typ a wiederum in eine Liste vom Typ a transformiert." Die Klasse Ord enthält den Vergleichsoperator (sinngemäß):

 class Ord a where compare :: a -> a -> Ordering 

Implementiert man sort einfach ohne Typdeklaration, so verwendet man natürlich die Funktion compare. Da die nur in der Klasse Ord existiert, wird daraus das einschränkende "Ord a" durch den Typabgleich gefunden. Im Prinzip wäre es praktisch, könnte man auf die Typklassen verzichten und einfach Überladung wie in C++ erlauben. Leider wird davon die Typinferenz NP-vollständig (oder was ähnlich schlimmes, das hab ich nicht so im Kopf), also hält man das lieber etwas im Zaum. Der Dokumentationseffekt ist es meines Erachtens allemal wert.

Übrigens gibt es auch eine Sortierfunktion mit beliebigem Kriterium. Die ist wieder voll polymorph. Man beachte, dass das ungefähr dem qsort in C entspricht, aber letzteres auf (void*) und eine häßliche Lücke im Typsystem zurückgreifen muß.

sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sort = sortBy compare

Ein anderes Beispiel ist die FiniteMap? (aka Wörterbuch). Der Datentyp ist vollkommen polymorph. Da die FiniteMap? aber intern ein Suchbaum ist, funktioniert sie natürlich nur, wenn man die Schlüssel auch vergleichen kann. Das schränkt den Typ jeder darauf arbeitenden Funktion ein:

 addToFM :: Ord key => FiniteMap key value -> key -> value -> FiniteMap key value
 deleteFromFM :: Ord key => FiniteMap key value -> key -> FiniteMap key value
 unionManyFM :: Ord key => [FiniteMap key value] -> FiniteMap key value

Manche funktionieren auch ohne Einschränkung. Beispielsweise kann man das Wörterbuch durchlaufen ohne Schlüssel zu vergleichen. Klar, man klappert ja den fertigen Baum ab. Diese Freiheit nutzt einem allerdings nicht viel, woher soll man jemals eine FiniteMap? mit Schlüsseltyp ohne Ordnung bekommen? Immerhin sind das leere und das einelementige Wörterbuch ohne diese Typeinschränkung zu haben.

 foldFM :: (key -> value -> a -> a) -> a -> FiniteMap key value -> a

Das mag jetzt etwas verkorkst klingen und im Zweifelsfall wie viel Schreibarbeit aussehen, ist aber ganz praktisch. Erstens schreibt man nie mit Absicht fehlgetypte Programme, da sie ohnehin nicht funktionieren würden, zweitens ist man nie verpflichtet, die Typen wirklich hinzuschreiben. Normalerweise bleiben sie auch recht kurz.

Wäre so etwas in einer Sprache wie Smalltalk oder Java denkbar?

Auf Smalltalk passt sowas meiner Ansicht nach nicht. Smalltalk lebt davon, dass man Nachrichten "blind" an Objekte sendet, ohne Rücksicht auf deren Typ oder Klasse. Man kann ja sogar Listen von miteinander überhaupt nicht verwandten Objekten erstellen und an jedes davon die gleiche Nachricht senden, manche der Objekte verstehen die vielleicht überhaupt nicht, usw. Das ist alles nicht mit statischer Typisierung zu erfassen. Ja, vielleicht geht es, aber das Resultat wäre nicht mehr Smalltalk. Und Java... Java hat das Objektmodell von Smalltalk übernommen und dann das armselige Typsystem von C (ohne ++) übergestülpt. In Java ist man immer geneigt, alle Interfaces nur mit "Object" zu deklarieren und sieht sich dann gezwungen, beim Methodenaufruf zu casten. Ehrlich gesagt denke ich, Java ist sowieso nicht mehr zu retten. Wer mitdenkt, nimmt (je nach Geschmack und Problemstellung) Smalltalk, C++ oder ML.

Typinferenz geht auch bei dynamischer Typisierung. Im RefactoringBrowser für SpracheSmalltalk ist ein Typinferenzer integriert. Der ist allerdings etwas versteckt. Er erzeugt einen Klassen-Kommentar, in dem für jede Membervariable alle möglichen Typen angegeben werden. Der Inferenzer leistet allerdings erheblich weniger, als bei statsicher Typisierung und insbesondere bei funktionaler Programmierung möglich wäre. Typannotationen im Stile dessen, was der RefactoringBrowser vorschlägt, werden in Smalltalk benötigt, um das Rountrip-Engeneering per Case-Tool zu vereinfachen.

Heterogene Container

Was ist der Typ für eine Hashtabelle (Elemente implementieren Hashfunktion)?

Meinst du eine heterogene Tabelle verschiedener Dinge, die eine Hashfunktion besitzen, sonst aber nichts gemeinsam haben?

Falls ja: Das geht nicht. Im Hindley-Milner-System gibt es nur homogene Container. Normalerweise macht das nichts: Irgendwann hole ich ja die Dinge wieder aus dem Container heraus, und dann will ich etwas mit ihnen machen, und zwar nicht zu irgendwas casten! Was immer dann möglich ist, kann ich auch vorher tun und Funktionen in den Container stecken. Dann ist er wieder homogen.

Wenn man eine bestimmte Auswahl an Typen im Blick hat, kann man allerdings einen Typen definieren, der diese Typen vereint. Das ist wie ein typsicheres union in der SpracheCee oder variante Datenverbünde in der SpracheModula2?. Man kann etwa mit
data TypMix =
    Text      String
  | Bruch     Double
  | GanzeZahl Integer
die drei Typen String, Double und Integer als Alternativen verwenden. Allerdings sollte das nicht dazu missbraucht werden, um dynamische Typisierung zu simulieren!


StartSeite | Neues | TestSeite | ForumSeite | Teilnehmer | Kategorien | Index | Hilfe | Einstellungen | Ändern
Text dieser Seite ändern (zuletzt geändert: 7. April 2005 14:24 (diff))
Suchbegriff: gesucht wird
im Titel
im Text