X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=deliverables%2Fp2%2Fp2.tex;h=b7d7639352ea561e0f79cd32ff2306084446d738;hb=1f01e39fb2383aa2c63234d0750c0459fe3de752;hp=09d75d28cf2981765ce4e1b330924faca0d3c02e;hpb=097f4bec1e2f95e2926530fdd1dbee177a9caebc;p=cc1516.git diff --git a/deliverables/p2/p2.tex b/deliverables/p2/p2.tex index 09d75d2..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: @@ -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{flip(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;} @@ -144,7 +146,6 @@ flop(n, l) { \end{itemize} \end{frame} - \begin{frame}[fragile] \frametitle{Mutual Recursion} \begin{itemize} @@ -165,6 +166,143 @@ 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{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} + % - 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?