[FMFP] Typing

semester4/fmfp/formal-methods-functional-programming-summary.tex

@@ -68,13 +68,15 @@
 % \input{parts/01_formal-reasoning/05_correctness/}
 % \input{parts/01_formal-reasoning/}
 
+
 \newsection
 \section{Typing}
 \input{parts/02_typing/00_intro.tex}
 \input{parts/02_typing/01_mini-haskell/00_syntax.tex}
+\input{parts/02_typing/01_mini-haskell/01_lambda-calculus.tex}
+\input{parts/02_typing/01_mini-haskell/02_further-rules.tex}
+\input{parts/02_typing/01_mini-haskell/03_type-inference.tex}
 % \input{parts/02_typing/01_mini-haskell/}
-\input{parts/02_typing/02_lambda-calculus.tex}
-% \input{parts/02_mini-haskell/}
 
 
 \end{document}

semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex

@@ -4,8 +4,12 @@ This is a stripped down version of Haskell, used here to explore the type system
 \subsubsection{Syntax}
 Programs are terms, the core is the lambda-calculus, where $\cV$ is the set of variables and $\Z$ the set of integers:
 \[
-    t :: = \cV \divider (\lambda x. t) \divider (t_1 t_2) \divider True \divider False \divider (\textbf{iszero } t) \divider \Z \divider (t_1 + t_2) \divider t_1 * t_2 
+    t :: = \cV \divider (\lambda x. t) \divider (t_1 t_2) \divider True \divider False \divider (\textbf{iszero } t) \divider \Z \divider (t_1 + t_2) \divider t_1 * t_2
     \divider \textbf{if } t_0 \textbf{ then } t_1 \textbf{ else } t_2 \divider (t_1, t_2) \divider (\textbf{fst } t) \divider (\textbf{snd } t)
 \]
 
 It is easily possible to add additonal syntax and types and we employ syntactic sugar, such as omitting parenthesis.
+
+The types are given by $\tau ::= \cV_T \divider \texttt{Bool} \divider \texttt{Int} \divider (\tau, \tau) \divider (\tau \rightarrow \tau)$, where $\cV_T$ is a set of type variables.
+The type system is based on typing judgement of form $\Gamma \vdash t :: r$, where $\Gamma$ is a set of bindings $x_i : \tau_i$
+that maps variables to types and can be understood as a typing symbol table.

semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex

@@ -0,0 +1,21 @@
+\subsubsection{Lambda calculus}
+To prove that types are correct, the lambda calculus comes in handy.
+It is based on the same concept as natural deduction trees
+
+\paragraph{Core rules for Lambda-Calculus}
+\[
+    \begin{prooftree}
+        \infer0[Var]{\Gamma, x : \tau \vdash x :: \tau}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma, x : \sigma \vdash t :: \tau}
+        \infer1[Abs]{\Gamma \vdash (\forall x. t) :: \sigma \rightarrow \tau}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t_1 :: \sigma \rightarrow \tau}
+        \hypo{\Gamma \vdash t_2 :: \sigma}
+        \infer2[App]{\Gamma \vdash (t_1 t_2) :: \tau}
+    \end{prooftree}
+\]

semester4/fmfp/parts/02_typing/01_mini-haskell/02_further-rules.tex

@@ -0,0 +1,58 @@
+\subsubsection{Further rules for mini-Haskell}
+\paragraph{Base types}
+\[
+    \begin{prooftree}
+        \infer0[Int]{\Gamma \vdash n :: \texttt{Int}}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[True]{\Gamma \vdash \texttt{True} :: \texttt{Bool}}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[False]{\Gamma \vdash \texttt{False} :: \texttt{Bool}}
+    \end{prooftree}
+\]
+
+\paragraph{Operations}
+Let $\textbf{op} \in \{ +, * \}$
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t :: \texttt{Int}}
+        \infer1[iszero]{\Gamma \vdash (\textbf{iszero } t) :: \texttt{Bool}}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t_1 :: \texttt{Int}}
+        \hypo{\Gamma \vdash t_2 :: \texttt{Int}}
+        \infer2[BinOp]{\Gamma \vdash (t_1 \textbf{ op } t_2) :: \texttt{Int}}
+    \end{prooftree}
+\]
+\[
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t_0 :: \texttt{Bool}}
+        \hypo{\Gamma \vdash t_1 :: \tau}
+        \hypo{\Gamma \vdash t_2 :: \tau}
+        \infer3[if]{\Gamma \vdash (\textbf{if } t_0 \textbf{ then } t_1 \textbf{ else } t_2) :: \tau}
+    \end{prooftree}
+\]
+
+\paragraph{Tuples}
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t_1 :: \tau_1}
+        \hypo{\Gamma \vdash t_2 :: \tau_2}
+        \infer2[Tuple]{\Gamma \vdash (t_1, t_2) :: (\tau_1, \tau_2)}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t :: (\tau_1, \tau_2)}
+        \infer1[fst]{\Gamma \vdash (\textbf{fst } t) :: \tau_1}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash t :: (\tau_1, \tau_2)}
+        \infer1[snd]{\Gamma \vdash (\textbf{snd } t) :: \tau_2}
+    \end{prooftree}
+\]

semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex

@@ -0,0 +1,26 @@
+\subsubsection{Type inference}
+Type inference in general fails, if two (or more) branches fail to resolve to unifiable types.
+
+We start a \bi{type judgement} with judgement $\vdash t :: \tau_0$, then build a derivation tree bottom-up.
+Finally, apply constraints / unification to get possible types.
+
+
+\paragraph{Self application}
+This means that you apply a function to itself.
+In Haskell, this is not typeable because there would need to be an infinite function type, but all \bi{Haskell types are finite} 
+
+
+\paragraph{Curry-Howard isomorphism}
+We can also apply the implication introduction and implication elimination rules:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma, \sigma \vdash \tau}
+        \infer1[$\rightarrow$-I]{\Gamma \vdash \sigma \rightarrow \tau}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash \sigma \rightarrow \tau}
+        \hypo{\Gamma \vdash \sigma}
+        \infer2[$\rightarrow$-E]{\Gamma \vdash \tau}
+    \end{prooftree}
+\]

semester4/fmfp/parts/02_typing/02_lambda-calculus.tex

@@ -1 +0,0 @@
-\subsection{Lambda calculus}