\newcommand{\mgu}{\operatorname{mgu}}

\begin{slide}{Typen}

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

wenn $f :: A \to B$ und $x :: A$, dann $(f x) :: B$.


\bigskip

bei polymorphen Typen können der Typ von $f :: A \to B$ 
und der Typ von $x :: A'$ Typvariablen enthalten.

Dann müssen $A$ und $A'$ nicht übereinstimmen,
sondern nur \emph{unfizierbar} sein
(eine gemeinsame Instanz besitzen).

\bigskip

$\sigma := \mgu(A,A')$ (allgemeinster Unifikator)

allgemeinster Typ von $(f x)$ ist dann $B\sigma$.

Typ von $x$ wird dadurch spezialisiert auf $A'\sigma$


\bigskip

Bestimme allgemeinsten Typ 
von $t = \lambda f x . f(f x))$, von $(t t)$.


\end{slide}
