Inferenzregeln f. Rekonstruktion (Plan)

Plan:

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

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))