Presentation

[cc1516.git] / deliverables / p2 / p2.tex

diff --git a/deliverables/p2/p2.tex b/deliverables/p2/p2.tex
index 09d75d2..9f5fc65 100644 (file)
--- a/deliverables/p2/p2.tex
+++ b/deliverables/p2/p2.tex
@@ -69,8 +69,11 @@ sem :: AST -> SemOutput
                Does matter for variables, not for functions.
                \pause
                \begin{itemize}
-                       \item Note that this means that \texttt{ones=1:ones} is 
+                       \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%
@@ -120,8 +123,8 @@ flop(n, l) :: Int -> [Int] -> Bool {
 }
                \end{CleanCode}
                \pause
-               \item It is also correctly determined that \texttt{Bool} and the return 
-               type of \texttt{flop(n,l)} don't match.
+               \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}
 
@@ -130,7 +133,6 @@ flop(n, l) :: Int -> [Int] -> Bool {
        \begin{itemize}
                \item Mutual recursion is allowed and type checked, however inference is
                not complete.
-               \pause
                \begin{CleanCode}
 flip(n, l) {
   if( n <= 0 ) {return l;} 
@@ -165,6 +167,99 @@ flop(n, l) :: Int -> [Int] -> HSWdn {
        \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}
+
 % - Can functions that are defined later in a file call earlier defined functions?
 % - Can local variables be defined in terms of other local variables?
 % - How do you deal with assignments?