\begin{slide}{Inferenzregeln f. Rekonstruktion (Plan)}

Plan: 
\begin{itemize}
\item 
  Aussage \( E \vdash X : (T, C) \) ableiten,
\item
  dann $C$ lösen (allgemeinsten Unifikator $\sigma$ bestimmen)
\item
  dann ist $T \sigma$ der (allgemeinste) Typ von $X$ (in Umgebung $E$)
\end{itemize}

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

Inferenzregeln? Implementierung? --- Testfall:
\begin{verbatim}
\ f g x y -> 
   if (f x y) then (x+1) else (g (f x True))
\end{verbatim}

\end{slide}

\begin{slide}{Inferenzregeln f. Rekonstrukion}

  \begin{itemize}
  \item primitive Operationen (Beispiel)
\newcommand{\Int}{\text{Int}}
\[ 
\frac
{E \vdash X_1:(T_1,C_1), \quad E \vdash X_2:(T_2,C_2)}
{E \vdash X_1 + X_2 : 
(\Int, \{ T_1=\Int,T_2=\Int\}\cup C_1 \cup C_2)
}
\]
\item Applikation
\[\frac
{E \vdash F : (T_1, C_1), \quad E \vdash A : (T_2,C_2)}
{E \vdash (F A): \ldots}
\]
\item Abstraktion
\[
\frac{\ldots}{E\vdash \lambda x.B : \ldots}
\]
\item (Ü) Konstanten, Variablen, if/then/else
  \end{itemize}



\end{slide}
