Rekonstruktion polymorpher Typen

...ist im Allgemeinen nicht möglich:

Joe Wells: Typability and Type Checking in System F Are Equivalent and Undecidable, Annals of Pure and Applied Logic 98 (1998) 111-156, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483

übliche Einschränkung (ML, Haskell): let-Polymorphismus:

Typ-Abstraktionen nur für let-gebundene Bezeichner:

let { t = \ f x -> f(f x) ; s = \ x -> x+1 } 
in t t s 0

folgendes ist dann nicht typisierbar (t ist monomorph):

( \ t -> let { s = \ x -> x+1 } in t t s 0 ) 
  ( \ f x -> f (f x) )