Work in progress inference

diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index f3325b2..3687777 100644 (file)
--- a/deliverables/report/sem.tex
+++ b/deliverables/report/sem.tex
@@ -153,37 +153,96 @@ Bool \rightarrow Bool$.
        \infer[Op2]
                {\Gamma \vdash e_1 \oplus e_2 \Rightarrow 
                        (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus e_2')^\star)}
-               {\Gamma \vdash e_1 \Rightarrow (\star_1, \tau_1, e_1') 
-               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\star_2, \tau_2, e_2') 
-               &\tau_1 \rightarrow \tau_2 \rightarrow \alpha \unif
+               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
+               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
+                       \star_2, \tau_2, e_2') 
+               &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
                        \textit{op2type}(\oplus) = \star_3
                &\star = \star_3 \cdot \star_2 \cdot \star_1
                }
 \end{equation}
 
 \paragraph{Op1 expressions}
-The inference rule for op1 expressions is very similar to that of op2 
-expressions and is shows in Equation~\ref{eq:inferOp1}
-
 \begin{equation} \label{eq:inferOp1}
        \infer[Op1]
                {\Gamma \vdash \ominus e \Rightarrow 
                        (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
                {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1') 
-               &\tau \rightarrow \alpha \unif
+               &(\tau \rightarrow \alpha) \unif
                        \textit{op1type}(\ominus) = \star_2
                &\star = \star_2 \cdot \star_1
                }
 \end{equation}
 
 \paragraph{Tuples}
+\begin{equation} \label{eq:tuples}
+       \infer[Tuple]
+               {\Gamma \vdash (e_1, e_2) \Rightarrow 
+                       (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star, 
+                               (e_1', e_2')^\star)}
+               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
+               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
+                       \star_2, \tau_2, e_2') 
+               &\star = \star_3 \cdot \star_2 \cdot \star_1
+               }
+\end{equation}
+
+\paragraph{Variables}
+Inferring variable requires a bit of care. First of all the variable has to
+be present in $\Gamma$, secondly field selectors need to be respected. To apply
+the field selectors on a type the function \tt{apfs} is used, which maps a 
+type and a field selector to a new type: $\texttt{apfs} : \tau \times 
+\textit{fieldselector} \rightarrow \tau$. 
+
+Note that the inference rule only checks if a field selector can be applied on
+a certain type, and does not use the field selector to infer the type. This means that a program: \tt{f(x)\{ return x.hd; \}} can not be typed, and instead 
+\tt{f} must be explicitly typed as \tt{:: [a] -> a} (or something more 
+specialised) by the programmer. This could be improved by 
+changing the \tt{apfs} function to infer for type variables. 
+
+\begin{equation}
+       \infer[Var]
+               {\Gamma \vdash \textit{id}.\textit{fs}^* \Rightarrow 
+                       (\Gamma, \star_0, \tau', \textit{id}.\textit{fs}^*)}
+               {\Gamma(id) = \lfloor \tau \rfloor
+               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau'
+               }
+\end{equation}
 
 \paragraph{Functions}
+When inferring two functions we distinguish two rules: one for a function which
+is applied without any arguments (Equation~\ref{eq:inferApp0}) and one for when
+a function is applied with arguments (Equation~\ref{eq:inferAppN}). Inferring a
+list of expressions is done by folding the infer function over the expressions
+and accumulating the resulting types, substitutions, etc. 
 
-\paragraph{Variables}
+\begin{equation} \label{eq:inferApp0}
+       \infer[App 0]
+               {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
+                       ((\Gamma^\star, \star, \tau^r, 
+                               \textit{id}().\textit{fs}^*)}
+               {\Gamma(id) = \lfloor \tau^e \rfloor
+               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
+               }
+\end{equation}
+
+\begin{equation} \label{eq:inferAppN}
+       \infer[AppN]
+               {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
+                       ((\Gamma^\star, \star, \tau^r, 
+                               \textit{id}({e^*}').\textit{fs}^*)}
+               {\Gamma(id) = \lfloor \tau^e \rfloor
+               &\Gamma \vdash e^* \Rightarrow 
+                       (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
+               &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*) 
+                       \unif \tau^e = \star_2
+               &\star = \star_2 \cdot \star_1
+               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
+               }
+\end{equation}
 
 \paragraph{Literals}
-The type literals, Ints, Bools, Chars and empty lists, are trivially 
+The types of literals -Ints, Bools, Chars and empty lists- are trivially 
 determined and are shown below. 
 
 \begin{equation}