diff --git a/vortrag.tex b/vortrag.tex index 64a5d28..24a9988 100644 --- a/vortrag.tex +++ b/vortrag.tex @@ -19,11 +19,11 @@ $\begin{array}{l} \begin{array}{@{}c} \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad - \Delta \vdash \expr{v}, \ol{v} : \ol{T} + \Delta \vdash \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T} \\ \hline \vspace*{-0.3cm}\\ - \Delta \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T} + \Delta \vdash \expr{v}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T} \end{array} \end{array}$ \end{center} @@ -45,17 +45,61 @@ $\begin{array}{l} \end{array}$ \end{center} +\textbf{Beispiele:}\\ \begin{verbatim} X head(List l) { ... } \end{verbatim} +\begin{itemize} +\item +$\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$ +\end{itemize} \begin{verbatim} List emptyList() { ... } \end{verbatim} - -$\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$ - +\begin{itemize} +\item $\textit{mtype}(\texttt{emptyList}) = \generics{\type{X}}\ [] \to \exptype{List}{\type{X}}$ +\end{itemize} +\end{frame} + +\begin{frame}[fragile] +\frametitle{Java Method Call} +\rulename{T-Call} \\[1em] +\begin{center} +$\begin{array}{l} + \begin{array}{@{}c} + \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad + \Delta \vdash \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T} + \\ + \hline + \vspace*{-0.3cm}\\ + \Delta \vdash \expr{v}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T} + \end{array} +\end{array}$ +\end{center} +\textbf{Beispiel:}\\ +$\begin{array}{l} + \begin{array}{@{}c} + \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad + \texttt{new List}() : [\type{String}/\type{X}]\exptype{List}{\type{X}} + \\ + \hline + \vspace*{-0.3cm}\\ + \generics{\type{String}}\texttt{head}(\texttt{new List}()) : [\type{String}/\type{X}]\type{X} + \end{array} +\end{array}$ + +$\begin{array}{l} + \begin{array}{@{}c} + \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad + \texttt{new List}() : \exptype{List}{\type{String}} + \\ + \hline + \vspace*{-0.3cm}\\ + \generics{\type{String}}\texttt{head}(\texttt{new List}()) : \type{String} + \end{array} +\end{array}$ \end{frame} \begin{frame}[fragile]