From: pimjager <pim@pimjager.nl>
Date: Fri, 10 Jun 2016 19:43:40 +0000 (+0200)
Subject:  Work in progress inference
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=935119844729f6ff3f030fc38d89d1bebff17ab8;p=cc1516.git

 Work in progress inference
---

diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index f3325b2..3687777 100644
--- 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}