Inferenzregeln f. Rekonstruktion (Plan)

Plan:

• Aussage E $\vdash$ X : (T, C) mathend000# ableiten,
• dann C mathend000# lösen (allgemeinsten Unifikator σ mathend000# bestimmen)
• dann ist Tσ mathend000# der (allgemeinste) Typ von X mathend000# (in Umgebung E mathend000#)

Für (fast) jeden Teilausdruck eine eigene („frische``) Typvariable ansetzen, Beziehungen zwischen Typen durch Constraints ausdrücken.

Inferenzregeln? Implementierung? -- Testfall:

\ f g x y -> 
   if (f x y) then (x+1) else (g (f x True))