[cc1516.git] / deliverables / report / sem.tex

\section{Semantic analysis}\label{sec:sem}
%The grammar used to parse
%SPL
%, if it is di erent from the given grammar.
%{
%The scoping rules you use and check in your compiler.
%{
%The typing rules used for
%SPL
%.
%{
%A brief guide telling what each of the examples tests (see next point).
%{
%A concise but precise description of how the work was divided amongst the
%members of
%the team.

\newcommand{\unif}{{\scriptscriptstyle\cup}}
%\subsubsection{Anonymous functions}
%When the programmers wants to use small functions that consist of one line to
%for example use the operators in a functional way the programmer has to make a
%named function for every operator. In some cases it is easy to do this inline
%using anonymous functions. A small syntactic sugar has been added that will
%inline anonymous functions to non-anonymous functions during the parsing phase.
%The following snippet is an example of a filter on even values before and after
%transformation.
%
%\begin{SPLCode}
%//Before transformation
%main(){
%       var a = filter(\x->x % 2 == 0, 1 : 2 : 3 : 4 : 5 : []);
%}      
%
%//After transformation
%1lambda_23(x){
%       return x % 2 == 0;
%}
%
%main(){
%       var a = filter(1lambda_23, 1 : 2 : 3 : 4 : 5 : []);
%}      
%\end{SPLCode}

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 one \AST{} transformation and checks four 
properties of the program:
\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 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=Clean]
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{Sanity checks}
% The sanity checks are defined as simple recursive functions over the function
% declarations in the \AST. We will very shortly describe them here.

% \begin{description}
%       \item [No duplicate functions] This function checks that the program does 
%               not contain top level functions sharing the same name. Formally:
%               $ \forall f \in \textrm{functions} \ldotp \neg 
%                       \exists g \in \textrm{functions} \setminus \{f\} \ldotp 
%                       f.\textrm{name} = g.\textrm{name}$
%       \item [\tt{main} should have type \tt{->Void}] Our semantics of \SPL{} 
%               require the main function to take no arguments and to not return a 
%               value. Formally: $\forall f \in \textrm{functions} \ldotp 
%                       f.\textrm{name} = \textrm{'main'} \Rightarrow
%                       \textit{typeof}\textrm{(main)} = \rightarrow\textrm{Void} $
%       \item [The program should have a main function] $\exists f \in 
%               \textrm{functions} \ldotp f.\textrm{name} = \textrm{'main'}$
% \end{description}

\subsection{Type inference}
\SPLC{} features a Hindley-Milner type inference algorithm based on the
algorithm presented in the slides. It 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 functions 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 concrete
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 = [tv \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}
        \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 \textit{ fs}^* = \tau^e
                }
\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}
        \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}