sdfsdf

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

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{} 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 AST transformation for lambdas
        \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}

% \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 is higher order functions, this is described
in more detail in Section~\ref{sec:ext}. These require a change to the
type system, which we will already describe here.

Higher order functions require 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                           -- polymorphic type
        | 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{Op2 expressions}
Equation~\ref{eq:inferOp2} shows the inference rule for op2 expressions. 
\textit{op2type} is a function which takes an operator and returns the 
corresponding function type, i.e. $\textit{op2type}(\&\&) = Bool \rightarrow
Bool \rightarrow Bool$. 

\begin{equation} \label{eq:inferOp2}
        \infer[Op2]
                {\Gamma \vdash e_1 \oplus e_2 \Rightarrow 
                        (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus e_2')^\star)}
                {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
                &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
                        \star_2, \tau_2, e_2') 
                &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
                        \textit{op2type}(\oplus) = \star_3
                &\star = \star_3 \cdot \star_2 \cdot \star_1
                }
\end{equation}

\paragraph{Op1 expressions}
\begin{equation} \label{eq:inferOp1}
        \infer[Op1]
                {\Gamma \vdash \ominus e \Rightarrow 
                        (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
                {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1') 
                &(\tau \rightarrow \alpha) \unif
                        \textit{op1type}(\ominus) = \star_2
                &\star = \star_2 \cdot \star_1
                }
\end{equation}

\paragraph{Tuples}
\begin{equation} \label{eq:tuples}
        \infer[Tuple]
                {\Gamma \vdash (e_1, e_2) \Rightarrow 
                        (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star, 
                                (e_1', e_2')^\star)}
                {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
                &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
                        \star_2, \tau_2, e_2') 
                &\star = \star_3 \cdot \star_2 \cdot \star_1
                }
\end{equation}

\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{Literals}
The types of literals -Ints, Bools, Chars and empty lists- are trivially 
determined and are shown below. 

\begin{equation}
        \infer[Int]{\Gamma \vdash n \Rightarrow (\Gamma, \star_0, Int, n)}{}
\end{equation}

\begin{equation}
        \infer[Bool]{\Gamma \vdash b \Rightarrow (\Gamma, \star_0, Bool, b)}{}
\end{equation}

\begin{equation}
        \infer[Char]{\Gamma \vdash c \Rightarrow (\Gamma, \star_0, Char, c)}{}
\end{equation}

\begin{equation}
        \infer[\emptyset]
                {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{}
\end{equation}

\paragraph{If statements}
balbal de if en else mzelfed type, jwz statements hebben he tupen wat ze
returnen.
\begin{equation}
        \infer[If]
                {\Gamma \vdash \underline{\textrm{if }} e 
                        \underline{\textrm{ then }} s_1 
                        \underline{\textrm{ else }} s_2
                        \Rightarrow
                        (\Gamma^\star, \star, \tau_e^\star, \underline{\textrm{if }} e' 
                        \underline{\textrm{ then }} s_1' 
                        \underline{\textrm{ else }} s_2')
                }
                {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
                &\tau_1 \unif \textrm{Bool} = \star_2
                &\Gamma^{\star_2\cdot \star_1} \vdash s_1 \Rightarrow 
                        (\Gamma^{\star_3}, \star_3, \tau_t, s_1')
                &\Gamma^{\star_3} \vdash s_2 \Rightarrow 
                        (\Gamma^{\star_4}, \star_4, \tau_e, s_2')
                &\tau_t \unif \tau_e = \star_5
                }
\end{equation}

\paragraph{While statements}
\begin{equation}
        \infer[While]
                {\Gamma \vdash \underline{\textrm{while }} e \textrm{ } s 
                        \Rightarrow
                        (\Gamma^\star, \star, \tau_s^\star, 
                                \underline{\textrm{while }} e' \textrm{ } s_1')
                }
                {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
                &\tau_1 \unif \textrm{Bool} = \star_2
                &\Gamma^{\star_2\cdot \star_1} \vdash s \Rightarrow 
                        (\Gamma^{\star_3}, \star_3, \tau_t, s')
                &\star = \star_3 \cdot \star_2 \cdot \star_1
                }
\end{equation}

\paragraph{Assignment statement}
blabla unapfs, en extenden van Gamma
\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}

\paragraph{Function Statements}
Blabl, praktisch gelijk aan function call, behalve dat ze altijd Void als
type hebben.

\begin{equation} \label{eq:inferStmtApp0}
        \infer[Stmt App 0]
                {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
                        ((\Gamma^\star, \star, \textrm{Void}, 
                                \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[Stmt AppN]
                {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
                        ((\Gamma^\star, \star, \textrm{Void}, 
                                \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}
blabla, verschil tussen wel en niet iets returnen

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