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

\begin{frame}[fragile]
	\frametitle{\textsc{SPLS}}
	\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 \texttt{ones=1:ones} is 
					not allowed.
		\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 \texttt{Bool} and the return 
		type of \texttt{flop(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.
		\pause
		\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}

% - 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}
