deliverables/report/sem.tex

   1 \section{Semantic analysis}\label{sec:sem}
   2 The semantic analysis phase asses if a -grammatically correct- program is also
   3 semantically correct and decorates the program with extra information it finds
   4 during this checking. The input of the semantic analysis is an \AST{} of the
   5 parsed program, its output is either a semantically correct and completely
   6 typed \AST{} plus the environment in which it was typed (for debug purposes),
   7 or it is an error describing the problem with the \AST{}.
   8
   9 During this analysis \SPLC{} applies one \AST{} transformation and checks four
  10 properties of the program:
  11 \begin{enumerate}
  12         \item That no functions are declared with the same name
  13         \item That \tt{main} is of type \tt{(-> Void)}
  14         \item That the program includes a main function
  15         \item That the program is correctly typed
  16 \end{enumerate}
  17 The first three steps are simple sanity checks which are coded in slightly over
  18 two dozen lines of \Clean{} code. The last step is a \emph{Hindley-Milner} type
  19 inference algorithm, which is a magnitude more complex. This last step also
  20 decorates the \AST{} with inferred type information.
  21
  22 \subsection{\AST{} transformation for lambdas}
  23 Before checking the semantic correctness of the program one small \AST{}
  24 transformations needs to be done. Currently this transformation is build into
  25 the semantic analysis phase, however, it would be more in place as a separate
  26 compiler phase, and if more transformations are needed in the future these will
  27 be placed in a separate phase.
  28
  29 The implementation of lambdas in \SPLC{} is implemented through a clever trick.
  30 All \\
  31 \tt{LambdaExpressions} in the \AST{} are lifted to actual functions. This
  32 transformation is illustrated in Listing~\ref{lst:lambdaLift}. This
  33 has the advantage that, with our support for higher order functions, lambda
  34 functions do not require any special attention after this transformation. One
  35 downside is that in the current implementation lambdas can not access variables
  36 in the scope in which they are declared. This could be solved by adding all
  37 free variables in the lambda expression as parameters to the lifted function.
  38
  39 \begin{lstlisting}[
  40         label={lst:lambdaLift},
  41         caption={SPLC types},
  42         language=SPLCode]
  43 main() {
  44         var x = \a b -> a + b;
  45 }
  46
  47 // is transformed to:
  48 2lambda_12(a, b) {
  49         return a + b;
  50 }
  51 main() {
  52         var x = 2lambda_12;
  53 }
  54 \end{lstlisting}
  55
  56 \subsection{\AST{} transformation for printing}
  57 During type inference and checking it is clear what the type is of all the
  58 functions and thus we can specify the print functions since it is overloaded.
  59 At time of compilation the overloaded print function is changed to the
  60 corresponding specific function. For example \SI{print(True)} is changed to
  61 \SI{1printbool(True)}. Printing is the only overloaded functionality built-in.
  62 While comparison and equality are overloaded too they generate the same
  63 assembly code for different types and thus need not to be specified.
  64
  65 \subsection{Type inference}
  66 \SPLC{} features a \emph{Hindley-Milner} type inference algorithm based on the
  67 algorithm presented in the slides. It supports full polymorphism and can infer
  68 omitted types. It does not support multiple recursion and all functions and
  69 identifiers need to be declared before they can be used. In essence the program
  70 is typed as nested \tt{let .. in ..} statements.
  71
  72 \subsubsection{Types}
  73 Listing~\ref{lst:types} shows the \ADT{} representing types in \SPLC{}. Most of
  74 these are self explanatory, however typing of functions requires some special
  75 attention. \SPLC{}s extension of higher order functions requires that the type
  76 system can distinguish if an
  77 expression represents a type $a$ or a functions which takes no input and returns
  78 a value of type $a$ (we write: $\rightarrow a$). The latter is represented by
  79 the \CI{FuncType}.
  80
  81 Another important difference with standard \SPL{} is that \SPLC{} supports
  82 currying of functions, functions are not typed with a list of argument types
  83 and a return type, but with just a single argument and return type. This return
  84 type then in itself can be a function.
  85
  86 \begin{lstlisting}[
  87         label={lst:types},
  88         caption={SPLC types},
  89         language=Clean]
  90 :: Type
  91         = TupleType (Type, Type)        -- (t1, t2)
  92         | ListType type                         -- [t]
  93         | IdType TVar                           -- type variable
  94         | IntType
  95         | BoolType
  96         | CharType
  97     | VoidType
  98         | FuncType Type                         -- (-> t)
  99     | (->>) infixl 7 Type Type  -- (t1 -> t2)
 100 \end{lstlisting}
 101
 102 \subsubsection{Environment}
 103 As all stages of \SPLC{}, the type inference is programmed in Clean. It takes
 104 an \AST{} and produces either a fully typed \AST{}, or an error if the provided
 105 \AST{} contains type errors. The Program is typed in an environment $\Gamma :
 106 id \rightarrow \Sigma$ which maps identifiers of functions or variables to type
 107 schemes.
 108
 109 In \SPLC{} type inference and unification are done in one pass. They are
 110 unified in the \tt{Typing} monad, which is defined as \CI{Typing a :== StateT
 111 (Gamma, [TVar]) (Either SemError) a}. The carried list of \tt{TVar} is an
 112 infinite list of fresh \tt{TVars}, which are just an alias of \tt{String}.
 113
 114 \subsubsection{Substitution and Unification}
 115 In \SPLC{} substitutions are defined as map from type variables to concrete
 116 types. Composing of substitutions is then simply taking the union of two
 117 substitutions and substituting the first substitution over the types in the
 118 second substitution. We write $\star$ for a substitution and $\star_0$ for the
 119 empty substitution.
 120
 121 Unification ($\unif$) takes two types and either provides a substitution which
 122 could unify them, or an error of the types are not unifiable. The interesting
 123 case of unification is when trying to unify an type variable with a more
 124 specialised type. Equation~\ref{eq:unifyId} shows this. All other cases are
 125 trivially promoting unification to the contained types, or checking directly if
 126 the types to be unified are equal.
 127
 128 \begin{equation} \label{eq:unifyId}
 129         \infer{\alpha \unif \tau = [tv \mapsto \tau]}
 130                         {\alpha \notin ftv(\tau)}
 131 \end{equation}
 132
 133 \subsubsection{Inferring}
 134 Inferring the type of expression or statement yields a 4-tuple of a new Gamma,
 135 Substitution, a Type and an updated version of that element. In the case of
 136 expressions the yielded type is the actual type of the expression. In the case
 137 of statements the yielded type is the type returned by a return statement if
 138 one is present, or Void otherwise.
 139
 140 In the Clean implementation the new Gamma in the result of an inference is
 141 carried through the Typing Monad.
 142
 143 Below we will show the inference rules for expressions and statements. In these
 144 lowercase Greek letters are always fresh type variables.
 145
 146 Section~\ref{sec:infRules} shows all typing inference rules. Below we will show
 147 a few to express the basics and show some interesting cases.
 148
 149 \paragraph{Variables}
 150 Inferring variable requires a bit of care. First of all the variable has to
 151 be present in $\Gamma$, secondly field selectors need to be respected. To apply
 152 the field selectors on a type the function \tt{apfs} is used, which maps a
 153 type and a field selector to a new type: $\texttt{apfs} : \tau \times
 154 \textit{fieldselector} \rightarrow \tau$.
 155
 156 Note that the inference rule only checks if a field selector can be applied on
 157 a certain type, and does not use the field selector to infer the type. This
 158 means that a program: \tt{f(x)\{ return x.hd; \}} can not be typed, and instead
 159 \tt{f} must be explicitly typed as \tt{:: [a] -> a} (or something more
 160 specialised) by the programmer. This could be improved by changing the
 161 \tt{apfs} function to infer for type variables.
 162
 163 \begin{equation}
 164         \infer[Var]
 165                 {\Gamma \vdash \textit{id}.\textit{fs}^* \Rightarrow
 166                         (\Gamma, \star_0, \tau', \textit{id}.\textit{fs}^*)}
 167                 {\Gamma(id) = \lfloor \tau \rfloor
 168                 &\texttt{fold apfs } \tau \textit{ fs}^* = \tau'
 169                 }
 170 \end{equation}
 171
 172 \paragraph{Functions}
 173 When inferring two functions we distinguish two rules: one for a function which
 174 is applied without any arguments (Equation~\ref{eq:inferApp0}) and one for when
 175 a function is applied with arguments (Equation~\ref{eq:inferAppN}). Inferring a
 176 list of expressions is done by folding the infer function over the expressions
 177 and accumulating the resulting types, substitutions, etc.
 178
 179 \begin{equation} \label{eq:inferApp0}
 180         \infer[App 0]
 181                 {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
 182                         ((\Gamma^\star, \star, \tau^r,
 183                                 \textit{id}().\textit{fs}^*)}
 184                 {\Gamma(id) = \lfloor \tau^e \rfloor
 185                 &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
 186                 }
 187 \end{equation}
 188
 189 \begin{equation} \label{eq:inferAppN}
 190         \infer[AppN]
 191                 {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
 192                         ((\Gamma^\star, \star, \tau^r,
 193                                 \textit{id}({e^*}').\textit{fs}^*)}
 194                 {\Gamma(id) = \lfloor \tau^e \rfloor
 195                 &\Gamma \vdash e^* \Rightarrow
 196                         (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
 197                 &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
 198                         \unif \tau^e = \star_2
 199                 &\star = \star_2 \cdot \star_1
 200                 &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
 201                 }
 202 \end{equation}
 203
 204 \paragraph{Return statements}
 205 Statements are typed with the type they return. The base case for this is
 206 trivially a return statement. An empty return statement is of type \tt{Void}
 207 and other return statements are typed with the type or their expression.
 208
 209 When checking combinations of statements, e.g. if-then-else statements, it is
 210 checked that all branches return the same type, then the type of the
 211 combination is set to this type.
 212
 213 \begin{equation}
 214         \infer[Return \emptyset]
 215                 {\Gamma \vdash \underline{\textrm{return}} \Rightarrow
 216                         (\Gamma, \star_0, \textrm{Void}, \underline{\textrm{return}})
 217                 }
 218                 {}
 219 \end{equation}
 220
 221 \begin{equation}
 222         \infer[Return]
 223                 {\Gamma \vdash \underline{\textrm{return }} e \Rightarrow
 224                         (\Gamma^\star, \star, \tau, \underline{\textrm{return }} e')
 225                 }
 226                 {\Gamma \vdash e \Rightarrow (\Gamma^\star, \star, \tau, e')}
 227 \end{equation}
 228
 229 \paragraph{Assignment statement}
 230 When assigning a new value to a variable this variable needs to be present in
 231 Gamma and its type needs to unify with the type of the expression.
 232
 233 One thing that needs to be taken care of when assigning are the field
 234 selectors.  \tt{unapfs} is a function which takes a type and a fieldselector
 235 and returns the type of the variable needed to assign to that fieldselector,
 236 i.e. \CI{unapfs a FieldHd = ListType a}
 237 \begin{equation}
 238         \infer[Ass]
 239                 {\Gamma \vdash \textit{id.fs}^* \underline{=} e \Rightarrow
 240                         (\Gamma^\star.k:\tau_r^\star, \star, \textrm{Void},
 241                                 \textit{id.fs}^* \underline{=} e')
 242                 }
 243                 {\Gamma(\textit{id}) = \lfloor \tau_e \rfloor
 244                 &\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_g, e')
 245                 &\texttt{fold unapfs } \tau_g \textit{ reverse fs} = \tau^r
 246                 &\tau_e \unif \tau_g = \star_2
 247                 &\star = \star_2 \cdot \star_1
 248                 }
 249 \end{equation}