repositories
/
cc1516.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
7c11c79
)
small fix eval
author
pimjager
<pim@pimjager.nl>
Sun, 19 Jun 2016 12:10:12 +0000
(14:10 +0200)
committer
pimjager
<pim@pimjager.nl>
Sun, 19 Jun 2016 12:10:12 +0000
(14:10 +0200)
deliverables/report/sem.tex
patch
|
blob
|
history
diff --git
a/deliverables/report/sem.tex
b/deliverables/report/sem.tex
index
9aa5af9
..
67d74db
100644
(file)
--- a/
deliverables/report/sem.tex
+++ b/
deliverables/report/sem.tex
@@
-6,8
+6,8
@@
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{}.
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
:
+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)}
\begin{enumerate}
\item That no functions are declared with the same name
\item That \tt{main} is of type \tt{(-> Void)}
@@
-61,7
+61,8
@@
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
\subsection{Type inference}
\SPLC{} features a \emph{Hindley-Milner} type inference algorithm based on the
-algorithm presented in the slides. It supports full polymorphism and can infer
+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.
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.
@@
-71,7
+72,7
@@
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
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
s
which takes no input and returns
+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}.
a value of type $a$ (we write: $\rightarrow a$). The latter is represented by
the \CI{FuncType}.
@@
-109,7
+110,7
@@
unified in the \tt{Typing} monad, which is defined as \CI{Typing a :== StateT
infinite list of fresh \tt{TVars}, which are just an alias of \tt{String}.
\subsubsection{Substitution and Unification}
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
+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
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
@@
-123,7
+124,7
@@
trivially promoting unification to the contained types, or checking directly if
the types to be unified are equal.
\begin{equation} \label{eq:unifyId}
the types to be unified are equal.
\begin{equation} \label{eq:unifyId}
- \infer{\alpha \unif \tau = [
tv
\mapsto \tau]}
+ \infer{\alpha \unif \tau = [
\alpha
\mapsto \tau]}
{\alpha \notin ftv(\tau)}
\end{equation}
{\alpha \notin ftv(\tau)}
\end{equation}
@@
-195,7
+196,7
@@
and accumulating the resulting types, substitutions, etc.
&(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
\unif \tau^e = \star_2
&\star = \star_2 \cdot \star_1
&(\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
+ &\texttt{fold apfs } \tau
^e \textit{ fs}^* = \tau^r
}
}
\end{equation}
}
}
\end{equation}