\begin{slide}{Rekonstruktion polymorpher Typen}

\dots ist im Allgemeinen nicht möglich:

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

\bigskip

übliche Einschränkung (ML, Haskell):
\emph{let-Polymorphismus}: 

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

\begin{verbatim}
let { t = \ f x -> f(f x) ; s = \ x -> x+1 } 
in t t s 0
\end{verbatim}
folgendes ist dann nicht typisierbar 
(\verb|t| ist monomorph):
\begin{verbatim}
( \ t -> let { s = \ x -> x+1 } in t t s 0 ) 
  ( \ f x -> f (f x) )
\end{verbatim}

\end{slide}

\begin{slide}{Implementierung}

let-Polymorphie, Hindley/Damas/Milner
  \begin{itemize} \parskip 1pt
  \item 
Inferenzsystem ähnlich zu Rekonstruktion
monomorpher Typen mit Aussagen der Form
\( E \vdash X : (T, C) \)
\item
Umgebung $E$ ist jetzt partielle Abbildung
von Name nach Typschema (nicht wie bisher: nach Typ).
\item
Bei Typinferenz für let-gebundene Bezeichner
wird über die freien Typvariablen generalisiert.
\item
Dazu Teil-Constraint-Systeme lokal lösen.
  \end{itemize}

Beispiel
\begin{verbatim}
let { c = ... }         
in let { g = \ f x -> f (if b c x) } in ..
\end{verbatim}

\end{slide}
