From 2d22389bce81f4c8f89d065b0428505455bd54a6 Mon Sep 17 00:00:00 2001 From: pimjager Date: Sun, 19 Jun 2016 14:10:12 +0200 Subject: [PATCH] small fix eval --- deliverables/report/sem.tex | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex index 9aa5af9..67d74db 100644 --- 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{}. -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)} @@ -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 -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. @@ -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 -expression represents a type $a$ or a functions 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}. @@ -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} -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 @@ -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} - \infer{\alpha \unif \tau = [tv \mapsto \tau]} + \infer{\alpha \unif \tau = [\alpha \mapsto \tau]} {\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 apfs } \tau \textit{ fs}^* = \tau^e + &\texttt{fold apfs } \tau^e \textit{ fs}^* = \tau^r } } \end{equation} -- 2.20.1