Typen

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

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

bei polymorphen Typen können der Typ von f : : A→B 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 Bσ.

Typ von x wird dadurch spezialisiert auf A'σ

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