Typen

für nicht polymorphe Typen: tatsächlicher Argumenttyp muß mit deklariertem Argumenttyp übereinstimmen:

wenn f : : AB und x : : A, dann (fx) : : B.


bei polymorphen Typen können der Typ von f : : AB und der Typ von x : : A' Typvariablen enthalten.

Dann müssen A und A' nicht übereinstimmen, sondern nur unfizierbar sein (eine gemeinsame Instanz besitzen).


σ : = mgu(A, A') (allgemeinster Unifikator)

allgemeinster Typ von (fx) ist dann .

Typ von x wird dadurch spezialisiert auf A'σ


Bestimme allgemeinsten Typ von t = λfx.f (fx)), von (tt).



Johannes Waldmann 2012-06-25