\frame{\titlepage}
\begin{frame}[fragile]
- \frametitle{\textsc{SPLS}}
+ \frametitle{\textsc{SPLT}}
\begin{block}{Features}
\begin{itemize}
\item Implementation language:
\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?}
\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}