%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
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 \tau$ which maps identifiers of functions or variables to types.
+\rightarrow \Sigma$ which maps identifiers of functions or variables to
+type schemes.
-In Clean the type inference functions run in the \tt{Typing} monad, which is
+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}.
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.
+second substitution. We write $\star$ for a substitution and $\star_0$ for the
+empty substitution.
-Unification ($\cup$) takes two types and either provides a substitution which
+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
if the types to be unified are equal.
\begin{equation} \label{eq:unifyId}
- \infer{tv \cup \tau \Rightarrow [tv \mapsto \tau]}
- {tv \notin ftv(\tau)}
+ \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
+hidden in the Typing Monad.
+
+Below we will show the inference rules for expressions and statements. In these
+lowercase Greek letters are always fresh type variables.
+
+\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 (\star_1, \tau_1, e_1')
+ &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\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}
+The inference rule for op1 expressions is very similar to that of op2
+expressions and is shows in Equation~\ref{eq:inferOp1}
+
+\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}
+
+\paragraph{Functions}
+
+\paragraph{Variables}
+
+\paragraph{Literals}
+The type 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}
\ No newline at end of file
repositories / cc1516.git / commitdiff