X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=deliverables%2Fp2%2Fp2.tex;h=9f5fc6564df48088f9550fad971b08661837e4da;hb=7b1d68ab317aaf431d123078daf9bd04f8829de0;hp=0399d8d51fde04146bc252dd7464d802bfc3e08c;hpb=5f216c089cf607cab359f5bc8d5b4ec76bc15a25;p=cc1516.git

diff --git a/deliverables/p2/p2.tex b/deliverables/p2/p2.tex
index 0399d8d..9f5fc65 100644
--- a/deliverables/p2/p2.tex
+++ b/deliverables/p2/p2.tex
@@ -67,6 +67,14 @@ sem :: AST -> SemOutput
 	\pause%
 	\begin{block}{Order?}
 		Does matter for variables, not for functions.
+		\pause
+		\begin{itemize}
+			\item Note that this means that \CI{ones=1:ones} is 
+					not allowed.
+			\pause
+			\item Functions which have not been encountered yet are temporarily
+				typed $\alpha$.
+		\end{itemize}
 	\end{block}
 	\pause%
 	\begin{block}{Mutual recursion?}
@@ -74,7 +82,181 @@ sem :: AST -> SemOutput
 	\end{block}
 	\pause%
 	\begin{block}{Higher order functions?}
-		Hopefully in the future
+		Would be an interesting idea for assignment 4
+	\end{block}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{Mutual Recursion}
+	\begin{itemize}
+		\item Mutual recursion is allowed and type checked, however inference is
+		not complete.
+		\pause
+		\begin{CleanCode}
+flip(n, l) :: Int -> [Int] -> [Int] {
+  if( n <= 0 ) {return l;} 
+  else {return flop(n-1, 0:l);}
+}
+
+flop(n, l) :: Int -> [Int] -> [Int] {
+  return flip(n, 1:l);
+}
+		\end{CleanCode}
+		\pause
+		\item Completely typed specifications are checked correctly.
+	\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{Mutual Recursion}
+	\begin{itemize}
+		\item Mutual recursion is allowed and type checked, however inference is
+		not complete.
+		\begin{CleanCode}
+flip(n, l) :: Int -> [Int] -> [Int] {
+  if( n <= 0 ) {return l;} 
+  else {return flop(n-1, 0:l);}
+}
+
+flop(n, l) :: Int -> [Int] -> Bool {
+  return flip(n, 1:l);
+}
+		\end{CleanCode}
+		\pause
+		\item It is also correctly determined that \CI{Bool} and the return 
+		type of \CI{flop(n,l)} don't match.
+	\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{Mutual Recursion}
+	\begin{itemize}
+		\item Mutual recursion is allowed and type checked, however inference is
+		not complete.
+		\begin{CleanCode}
+flip(n, l) {
+  if( n <= 0 ) {return l;} 
+  else {return flop(n-1, 0:l);}
+}
+
+flop(n, l) {
+  return flip(n, 1:l);
+}
+		\end{CleanCode}
+	\end{itemize}
+\end{frame}
+
+
+\begin{frame}[fragile]
+	\frametitle{Mutual Recursion}
+	\begin{itemize}
+		\item Mutual recursion is allowed and type checked, however inference is
+		not complete.
+		\begin{CleanCode}
+flip(n, l) :: Int -> [Int] -> vTqhp {
+  if( n <= 0 ) {return l;} 
+  else {return flop(n-1, 0:l);}
+}
+
+flop(n, l) :: Int -> [Int] -> HSWdn {
+  return flip(n, 1:l);
+}
+		\end{CleanCode}
+		\item However when no type information is given at all our algorithm 
+		fails to correctly infer the result type of the two function.
+	\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{But wait, there is more!}
+	\framesubtitle{Trouble that is}
+	\begin{itemize}
+		\item Polymorphism is not working great either.
+		\begin{CleanCode}
+id(x) :: a -> a {
+    return x;    
+}
+		\end{CleanCode}
+		\pause
+		\item Is typed fine, but when we introduce: 
+		\begin{CleanCode}
+var x = id(5);
+var y = id(True);
+		\end{CleanCode}
+		\pause
+		\begin{CleanCode}
+2:12 SemError: Cannot unify types. Expected: Int. Given: Bool
+		\end{CleanCode}
+	\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{But wait, there is more!}
+	\framesubtitle{Trouble that is}
+		\begin{block}{Our type inference algorithm is too greedy}
+			It globally types a function once it is applied to a value, even
+			if this types it more specified then needed. 
+		\end{block}
+		\pause
+		\begin{block}{Basically type inference for \CI{VarDecl} works great}
+			All instances of VarDecl work well. Including those where a var is
+			assigned by function application.
+		\end{block}
+		\pause
+		\begin{block}{Inference for functions is a completely different story}
+			\begin{itemize}
+				\item Type checking for functions works very well
+				\item Type inference for functions works spotty at best
+			\end{itemize}
+		\end{block}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{We changed to much from the presented algorithms}
+	\begin{itemize}
+		\item Our type checker is written with the origin algorithm 
+			\emph{in mind}
+		\pause
+		\item We were confident that that would be sufficient and we would be 
+			able to implement type inference this way.
+		\pause
+		\item As it turns out, \emph{we couldn't}!
+	\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{This not a problem for code generation}
+	\begin{block}{Sufficiently typed programs can be generated}
+		When all functions in the SPL program are completely typed then the
+		type inference algorithm yields a fully typed AST.\\  
+		\CI{VarDecls} \emph{types are correctly infered!}
+	\end{block}
+	\begin{block}{We can fix the type inference after code generation}
+		And this time do it right.
+	\end{block}
+\end{frame}
+
+\begin{frame}[fragile]
+	\frametitle{Doing it right}
+	\framesubtitle{How we will redo the type inference}
+	\begin{block}{Properly implement the \emph{exact} algorithm}
+		We will implement the Hindley-Miller algorithm exactly instead of 
+		\emph{``kinda''}
+	\end{block}
+	\begin{block}{Split constraint generation and solving}
+		Hide all the nasty details of constraint generation using a 
+		Reader-Writer-State-Transformer-Monad
+		\begin{description}
+			\item[Reader] Reader environment to read fresh type variable
+			\item[Writer] Write constraints to \CI{Constraint} environment
+			\item[State] Gamma
+			\item[Transformer] (Either SemError) 
+		\end{description}
+		\emph{Sadly these monads are not in the Clean library.}\\  
+		Then solve with a Relatively simple Solver-Monad
+		\begin{CleanCode}
+:: Solve a = StateT Unifier (Either TypeError) a
+		\end{CleanCode}
 	\end{block}
 \end{frame}