
\newcommand{\Ref}{\operatorname{Ref}}

\begin{slide}{Inferenzsystem für Typen (Syntax)}

  \begin{itemize}\itemsep 0pt
  \item Grundbereich: Aussagen der Form $E \vdash X : T$

    (in Umgebung $E$ hat Ausdruck $X$ den Typ $T$)
  \item
    Menge der Typen:
    \begin{itemize}
    \item primitiv: Int, Bool
    \item zusammengesetzt: 
      \begin{itemize}
      \item Funktion $T_1 \to T_2$
      \item Verweistyp $\Ref T$
      \item Tupel $(T_1, \ldots, T_n)$, einschl. $n=0$
      \end{itemize}
    \end{itemize}
  \item Umgebung bildet Namen auf Typen ab
  \end{itemize}

\end{slide}


\begin{slide}{Inferenzsystem für Typen (Semantik)}

  \begin{itemize}
  \item 
    Axiome f. Literale: $E \vdash \text{Zahl-Literal} : \text{Int}$, \dots
  \item 
    Regel für prim. Operationen:
    \(\displaystyle
    \frac{E\vdash X : \text{Int},E\vdash Y : \text{Int}}
    {E \vdash (X+Y) : \text{Int}}
      \), \dots
   \item Abstraktion/Applikation: \dots


   \item Binden/Benutzen von Bindungen: \dots
  \end{itemize}
hierbei (vorläufige) Design-Entscheidungen:
\begin{itemize}
\item Typ eines Ausdrucks wird inferiert
\item Typ eines Bezeichners wird \dots
  \begin{itemize}
  \item in Abstraktion: deklariert
  \item in Let: inferiert
  \end{itemize}
\end{itemize}



\end{slide}


\begin{slide}{Inferenz für Let}

(alles ganz analog zu Auswertung von Ausdrücken)

  \begin{itemize}
\item Regeln für Umgebungen

  \begin{itemize}
  \item 
  \( \displaystyle E[v:=t] \vdash v : t \)
\item
  \( \displaystyle
  \frac{E \vdash v' : t'}{E[v:=t] \vdash v' : t'}
  \) für $v \neq v'$
  \end{itemize}
\item Regeln für Bindung:
\[
\frac{E\vdash X : s, \quad  E [v:=s]  \vdash Y : t}
{E \vdash \mathtt{let~} v=X \mathtt{~in~} Y : t}
\]
  \end{itemize}

\end{slide}

\begin{slide}{Applikation und Abstraktion}

  \begin{itemize}
  \item Applikation:
\[
\frac{E\vdash F : T_1 \to T_2, \quad E \vdash A : T_1}
{E \vdash (F A) : T_2} 
\]

vergleiche mit \emph{modus ponens}

\item Abstraktion (mit deklariertem Typ der Variablen)

\[ \frac{E[v:=T_1] \vdash X : T_2}
{E\vdash (\lambda (v :: T_1) X) : T_1 \to T_2}
\]
  

  \end{itemize}

\end{slide}


\begin{slide}{Eigenschaften des Typsystems}

Wir haben hier den \emph{einfach getypten Lambda-Kalkül} nachgebaut:

  \begin{itemize}
  \item jedes Programm hat höchstens einen Typ
  \item nicht jedes Programm    hat einen Typ.

    Der $Y$-Kombinator 
    $(\lambda x.xx)(\lambda x.xx)$
    hat keinen Typ
  \item jedes getypte Programm terminiert
    
    (Begründung: bei jeder Applikation $F A$
    ist der Typ von $F A$ kleiner als der Typ von $F$)

  \end{itemize}

Übung: typisiere \verb|t t t t succ 0|
mit \verb|succ = \ x -> x + 1| 
und \verb|t = \ f x -> f (f x)|

\end{slide}
