\section{Semantic analysis}\label{sec:sem}
The semantic analysis phase asses if a -grammatically correct- program is also
semantically correct and decorates the program with extra information it finds
during this checking. The input of the semantic analysis is an \AST{} of the
parsed program, its output is either a semantically correct and completely
typed \AST{} plus the environment in which it was typed (for debug purposes),
or it is an error describing the problem with the \AST{}.

During this analysis \SPLC{} applies two transformation and checks four
properties of the \AST{}:
\begin{enumerate}
	\item That no functions are declared with the same name
	\item That \tt{main} is of type \tt{(-> Void)}
	\item That the program includes a main function
	\item That the program is correctly typed
\end{enumerate}
The first three steps are simple sanity checks which are coded in slightly over
two dozen lines of \Clean{} code. The last step is a \emph{Hindley-Milner} type
inference algorithm, which is a magnitude more complex. This last step also
decorates the \AST{} with inferred type information.

\subsection{\AST{} transformation for lambdas}
Before checking the semantic correctness of the program one small \AST{}
transformations needs to be done. Currently this transformation is build into
the semantic analysis phase, however, it would be more in place as a separate
compiler phase, and if more transformations are needed in the future these will
be placed in a separate phase.

The implementation of lambdas in \SPLC{} is implemented through a clever trick.
All \\
\tt{LambdaExpressions} in the \AST{} are lifted to actual functions. This
transformation is illustrated in Listing~\ref{lst:lambdaLift}. This
has the advantage that, with our support for higher order functions, lambda
functions do not require any special attention after this transformation. One
downside is that in the current implementation lambdas can not access variables
in the scope in which they are declared. This could be solved by adding all
free variables in the lambda expression as parameters to the lifted function.

\begin{lstlisting}[label={lst:lambdaLift},caption={\SPLC{} types},language=SPLCode]
main() {
	var x = \a b -> a + b;
}

// is transformed to:
2lambda_12(a, b) {
	return a + b;
}
main() {
	var x = 2lambda_12;
}
\end{lstlisting}

\subsection{\AST{} transformation for printing}
During type inference and checking it is clear what the type is of all the
functions and thus we can specify the print functions since it is overloaded.
At time of compilation the overloaded print function is changed to the
corresponding specific function. For example \SI{print(True)} is changed to
\SI{1printbool(True)}. Printing is the only overloaded functionality built-in.
While comparison and equality are overloaded too they generate the same
assembly code for different types and thus need not to be specified.

\subsection{Type inference}
\SPLC{} features a \emph{Hindley-Milner} type inference algorithm based on the
algorithm presented in the slides. \SPLC{} supports full polymorphism and can 
infer
omitted types. It does not support multiple recursion and all functions and
identifiers need to be declared before they can be used. In essence the program
is typed as nested \tt{let .. in ..} statements.

\subsubsection{Types}
Listing~\ref{lst:types} shows the \ADT{} representing types in \SPLC{}. Most of
these are self explanatory, however typing of functions requires some special
attention. \SPLC{}s extension of higher order functions requires that the type
system can distinguish if an
expression represents a type $a$ or a function which takes no input and returns
a value of type $a$ (we write: $\rightarrow a$). The latter is represented by
the \CI{FuncType}.

Another important difference with standard \SPL{} is that \SPLC{} supports
currying of functions, functions are not typed with a list of argument types
and a return type, but with just a single argument and return type. This return
type then in itself can be a function.

\begin{lstlisting}[
	label={lst:types},
	caption={SPLC types},
	language=Clean]
:: Type
	= TupleType (Type, Type) 	-- (t1, t2)
	| ListType type 			-- [t]
	| IdType TVar  				-- type variable
	| IntType
	| BoolType
	| CharType
    | VoidType
	| FuncType Type 			-- (-> t)
    | (->>) infixl 7 Type Type 	-- (t1 -> t2)
\end{lstlisting}

\subsubsection{Environment}
As all stages of \SPLC{}, the type inference is programmed in Clean. It takes
an \AST{} and produces either a fully typed \AST{}, or an error if the provided
\AST{} contains type errors. The Program is typed in an environment $\Gamma :
id \rightarrow \Sigma$ which maps identifiers of functions or variables to type
schemes.

In \SPLC{} type inference and unification are done in one pass. They are
unified in the \tt{Typing} monad, which is defined as \CI{Typing a :== StateT
(Gamma, [TVar]) (Either SemError) a}. The carried list of \tt{TVar} is an
infinite list of fresh \tt{TVars}, which are just an alias of \tt{String}.

\subsubsection{Substitution and Unification}
In \SPLC{} substitutions are defined as map from type variables to
types. Composing of substitutions is then simply taking the union of two
substitutions and substituting the first substitution over the types in the
second substitution. We write $\star$ for a substitution and $\star_0$ for the
empty substitution.

Unification ($\unif$) takes two types and either provides a substitution which
could unify them, or an error of the types are not unifiable. The interesting
case of unification is when trying to unify an type variable with a more
specialised type. Equation~\ref{eq:unifyId} shows this. All other cases are
trivially promoting unification to the contained types, or checking directly if
the types to be unified are equal.

\begin{equation} \label{eq:unifyId}
	\infer{\alpha \unif \tau = [\alpha \mapsto \tau]}
			{\alpha \notin ftv(\tau)}
\end{equation}

\subsubsection{Inferring}
Inferring the type of expression or statement yields a 4-tuple of a new Gamma,
Substitution, a Type and an updated version of that element. In the case of
expressions the yielded type is the actual type of the expression. In the case
of statements the yielded type is the type returned by a return statement if
one is present, or Void otherwise.

In the Clean implementation the new Gamma in the result of an inference is
carried through the Typing Monad.

Below we will show the inference rules for expressions and statements. In these
lowercase Greek letters are always fresh type variables.

Section~\ref{sec:infRules} shows all typing inference rules. Below we will show
a few to express the basics and show some interesting cases.

\paragraph{Variables}
Inferring variable requires a bit of care. First of all the variable has to
be present in $\Gamma$, secondly field selectors need to be respected. To apply
the field selectors on a type the function \tt{apfs} is used, which maps a
type and a field selector to a new type: $\texttt{apfs} : \tau \times
\textit{fieldselector} \rightarrow \tau$.

Note that the inference rule only checks if a field selector can be applied on
a certain type, and does not use the field selector to infer the type. This
means that a program: \tt{f(x)\{ return x.hd; \}} can not be typed, and instead
\tt{f} must be explicitly typed as \tt{:: [a] -> a} (or something more
specialised) by the programmer. This could be improved by changing the
\tt{apfs} function to infer for type variables.

\begin{equation}
	\infer[Var]
		{\Gamma \vdash \textit{id}.\textit{fs}^* \Rightarrow
			(\Gamma, \star_0, \tau', \textit{id}.\textit{fs}^*)}
		{\Gamma(id) = \lfloor \tau \rfloor
		&\texttt{fold apfs } \tau \textit{ fs}^* = \tau'
		}
\end{equation}

\paragraph{Functions}
When inferring two functions we distinguish two rules: one for a function which
is applied without any arguments (Equation~\ref{eq:inferApp0}) and one for when
a function is applied with arguments (Equation~\ref{eq:inferAppN}). Inferring a
list of expressions is done by folding the infer function over the expressions
and accumulating the resulting types, substitutions, etc.

\begin{equation} \label{eq:inferApp0}
	\infer[App 0]
		{\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
			((\Gamma^\star, \star, \tau^r,
				\textit{id}().\textit{fs}^*)}
		{\Gamma(id) = \lfloor \tau^e \rfloor
		&\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
		}
\end{equation}

\begin{equation}\label{eq:inferAppN}
	\resizebox{\linewidth}{!}{%
		\infer[AppN]
			{\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
				((\Gamma^\star, \star, \tau^r,
					\textit{id}({e^*}').\textit{fs}^*)}
			{\Gamma(id) = \lfloor \tau^e \rfloor
			&\Gamma \vdash e^* \Rightarrow
				(\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
			&(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
				\unif \tau^e = \star_2
			&\star = \star_2 \cdot \star_1
			&\texttt{fold apfs } \tau^{e \star} \textit{ fs}^* = \tau^r
		}
	}
\end{equation}

\paragraph{Return statements}
Statements are typed with the type they return. The base case for this is
trivially a return statement. An empty return statement is of type \tt{Void}
and other return statements are typed with the type or their expression.

When checking combinations of statements, e.g. if-then-else statements, it is
checked that all branches return the same type, then the type of the
combination is set to this type.

\begin{equation}
	\infer[Return \emptyset]
		{\Gamma \vdash \underline{\textrm{return}} \Rightarrow
			(\Gamma, \star_0, \textrm{Void}, \underline{\textrm{return}})
		}
		{}
\end{equation}

\begin{equation}
	\infer[Return]
		{\Gamma \vdash \underline{\textrm{return }} e \Rightarrow
			(\Gamma^\star, \star, \tau, \underline{\textrm{return }} e')
		}
		{\Gamma \vdash e \Rightarrow (\Gamma^\star, \star, \tau, e')}
\end{equation}

\paragraph{Assignment statement}
When assigning a new value to a variable this variable needs to be present in
Gamma and its type needs to unify with the type of the expression.

One thing that needs to be taken care of when assigning are the field
selectors.  \tt{unapfs} is a function which takes a type and a fieldselector
and returns the type of the variable needed to assign to that fieldselector,
i.e. \CI{unapfs a FieldHd = ListType a}
\begin{equation}
	\resizebox{\linewidth}{!}{%
		\infer[Ass]
			{\Gamma \vdash \textit{id.fs}^* \underline{=} e \Rightarrow
				(\Gamma^\star.k:\tau_r^\star, \star, \textrm{Void},
					\textit{id.fs}^* \underline{=} e')
			}
			{\Gamma(\textit{id}) = \lfloor \tau_e \rfloor
			&\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_g, e')
			&\texttt{fold unapfs } \tau_g \textit{ reverse fs} = \tau^r
			&\tau_e \unif \tau_g = \star_2
			&\star = \star_2 \cdot \star_1
		}
	}
\end{equation}
