%&p2
\begin{document}
\frame{\titlepage}

\begin{frame}[fragile]
	\frametitle{\textsc{SPLT}}
	\begin{block}{Features}
		\begin{itemize}
			\item Implementation language:
				Clean ({\tiny\url{http://clean.cs.ru.nl}})
			\pause%
			\item State transformer monad\pause%
				\begin{CleanCode}
:: Gamma :== (Map String Type, [String])
:: Env a :== StateT Gamma (Either SemError) a
				\end{CleanCode}
			\item Preferably we want to have an \CI{Either} monad transformer
				but clean does not have that\ldots
		\end{itemize}
	\end{block}
\end{frame}

\begin{frame}[fragile]
	\frametitle{Grammar changes}

	\begin{itemize}
		\item Function type:\pause%
			\begin{CleanCode}
<FunType>  ::= <VoidType> ['->' <FunType>]
<VoidType> ::= <Void> | Type
			\end{CleanCode}
		\pause Example%
			\begin{CleanCode}
append(l1, l2) :: [t] -> [t] -> [t] {
    ...
}
			\end{CleanCode}
		\pause\item We check in the semantic analysis that \CI{Void} is only in
			the last type.
		\pause\item This is for future higher-order functions
	\end{itemize}
\end{frame}

\begin{frame}[fragile]
	\frametitle{What do we analyze exactly?}
	\begin{CleanCode}
:: Pos = {line :: Int, col :: Int}
:: SemOutput :== Either [SemError] (AST, Gamma)
:: SemError 
    = ParseError Pos String                     // Post-parse errors
    | UnifyError Pos Type Type                  // Unification
    | FieldSelectorError Pos Type FieldSelector // hd, tail, fst, snd
    | OperatorError Pos Op2 Type                // 'a' == 5
    | UndeclaredVariableError Pos String        // Variable ordering
    | Error String

sem :: AST -> SemOutput
	\end{CleanCode}
\end{frame}

\begin{frame}[fragile]
	\frametitle{Analyses}
	\pause%
	\begin{block}{Scoping?}
		Local variables get a new name and are changed in the function body.
	\end{block}
	\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?}
		Yep!
	\end{block}
	\pause%
	\begin{block}{Higher order functions?}
		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}

% - 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?
% - Tell us if and how you include the value restriction.
%- How do you deal with recursion?
%- How do you deal with multiple recursion?
%- If you forbid multiple recursion, how do you do so?
% - Does your language support higher-order functions?
% - How do you deal with polymorphism?
% - How do you deal with overloading?
% - How does the absence/presence of type signatures influence your type
%  checker?
\end{document}
