X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=deliverables%2Fp2%2Fp2.tex;h=b7d7639352ea561e0f79cd32ff2306084446d738;hb=HEAD;hp=0399d8d51fde04146bc252dd7464d802bfc3e08c;hpb=4d2ac25a8c57caa5b68770b22a784c30fe0a794d;p=cc1516.git diff --git a/deliverables/p2/p2.tex b/deliverables/p2/p2.tex index 0399d8d..b7d7639 100644 --- a/deliverables/p2/p2.tex +++ b/deliverables/p2/p2.tex @@ -3,7 +3,7 @@ \frame{\titlepage} \begin{frame}[fragile] - \frametitle{\textsc{SPLS}} + \frametitle{\textsc{SPLT}} \begin{block}{Features} \begin{itemize} \item Implementation language: @@ -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,224 @@ 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{flip(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{It is not all trouble} + \begin{block}{A lot of functionality works correctly} + \begin{itemize} + \item Typing of \CI{VarDecls} + \pause + \item Typing of type chains: + \begin{CleanCode} +id_poly_wtf(x) :: a -> a +{ + var a = x; + var b = a; + var c = b; + return c; +} + \end{CleanCode} + \end{itemize} + \end{block} +\end{frame} + +\begin{frame}[fragile] + \frametitle{It is not all trouble} + \begin{block}{A lot of functionality works correctly} + \begin{itemize} + \item Typing of \CI{VarDecls} + \item Typing of type chains: + \begin{CleanCode} +id_poly_wtf(x) :: a -> a +{ + a a = x; + a b = a; + a c = b; + return c; +} + \end{CleanCode} + \pause + \item Typing \CI{var l = 1:2:[];} succeeds \\ + while. \CI{var l = []; var x = True:l; var y = 1:l;} fails + \end{itemize} + \end{block} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Why is there so much trouble?} + \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} + \pause + \begin{block}{Split constraint generation and solving} + Hide all the nasty details of constraint generation using a + Reader-Writer-State-Transformer-Monad + \pause + \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{\small Sadly these monads are not in the Clean library.}\\ + \pause + Then solve with a Relatively simple Solver-Monad + \begin{CleanCode} +:: Solve a = StateT Unifier (Either TypeError) a + \end{CleanCode} \end{block} \end{frame}