Skip to content


Subversion checkout URL

You can clone with
Download ZIP

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
  • 2 commits
  • 1 file changed
  • 0 commit comments
  • 1 contributor
Showing with 31 additions and 62 deletions.
  1. +31 −62 doc/main.tex
93 doc/main.tex
@@ -13,6 +13,7 @@
% things for the semantic package
@@ -117,7 +118,9 @@ \subsection{Type System}
Our type system has variables, arrows, and type environments, as well as
annotations, which is what makes it different from a normal polymorphic type
system. Table \ref{tab:typingelems} and \ref{tab:typing} show the elements of
-the type system.
+the type system. In the var and let/letrec case \emph{inst} and \emph{gen} are mentioned.
+Their definition is identical to the ones found in literature on the standard
+Hindley Milner let-polymorphic type system. The final syntax-directed type system is given in table \ref{tab:typing-rules}.
@@ -149,11 +152,6 @@ \subsection{Type System}
-Next a list of typing judgements will be given. This constitutes the final type
-system. %See weijers fig 5.3 for a reference.
-These rules are formulated in a syntax-directed fashion.
@@ -348,57 +346,6 @@ \subsection{Natural semantics}
-\subsection{Control Flow Analysis}
-We have the usual set of rules including, for example, \emph{cfa-var} or
-\emph{cfa-let}, which has been extended to support lists, see \emph{cfa-nil}
-and \emph{cfa-cons}, the rules specifying list-typing, Table
-\ref{tab:cfa-rules}. CFA judgements look like {$\widehat{\Gamma}\:\vdash_{CFA}
-t : \widehat{\sigma}$}, meaning that some term $t$ has inferred type
-$\widehat{\sigma}$ in context $\widehat{\Gamma}$. See Table 5.2 in \cite{nnh}
-for reference.
- \begin{centering}
- \begin{tabular}{ll}
- \hline
- $ [$\emph{cfa-var}$] $& \inference{\widehat{\Gamma}(x) = \widehat{\sigma}}
-{\widehat{\Gamma} |-_{CFA} x : \widehat{\sigma}} \\
-$[$\emph{cfa-let}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1:\widehat{\sigma}_1
-& \widehat{\Gamma}[x \mapsto \widehat{\sigma}_1] |-_{CFA} t_2 : \widehat{\tau}}
-{\widehat{\Gamma} |-_{CFA}\: \<let>\: x = t_1\: \<in>\: t_2 : \widehat{\tau}} \\
-$[$\emph{cfa-nil}$] $&
-{\widehat{\Gamma} |-_{CFA} [\,] : [\widehat{\sigma}]} \\
-$[$\emph{cfa-cons}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1:\widehat{\sigma}
- \widehat{\Gamma}|-_{CFA} t_2 : [\widehat{\sigma}]}
-{\widehat{\Gamma} |-_{CFA} t_1 \<:> t_2 : [\widehat{\sigma}]} \\
-% $[$\emph{cfa-pair}$] $& \inference{\widehat{\Gamma} |-_{CFA} t_1 : \widehat{\tau}_1 & \widehat{\Gamma} |-_{CFA} t_2 : \widehat{\tau}_2 }
-% {\widehat{\Gamma} |-_{CFA} (t_1,t_2) : \widehat{\tau}_1 \times^\varphi \widehat{\tau}_2 } \\
-% ~&~\\
-% $[$\emph{cfa-case-pair}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : \widehat{\tau}_1 \times^\varphi \widehat{\tau}_2
-% & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-% {\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: (x_1,x_2) \Rightarrow e_1 : \widehat{\tau} } \\
-% ~&~\\
-$[$\emph{cfa-case-nil}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : [\widehat{\tau}_1] & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-{\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: [] \Rightarrow e_1 : \widehat{\tau} }, if $e_0$ empty\\
-$[$\emph{cfa-case-cons}$] $& \inference{\widehat{\Gamma} |-_{CFA} e_0 : [\widehat{\tau}_1] & \widehat{\Gamma} |-_{CFA} e_1 : \widehat{\tau} }
-{\widehat{\Gamma} |-_{CFA} \:\<case>\: e_0\: \<of>\: (x\<:>xs) \Rightarrow e_1 : \widehat{\tau} }, if $e_0$ nonempty\\
- \hline
- \end{tabular}
- \caption{Control Flow Analysis rules. }
- \label{tab:cfa-rules}
- \end{centering}
\section{Program design}
The program compiles to a single executable, named \emph{cfa}. It relies heavily
on the UU Attribute Grammar system. Below is a list with filenames and a short
@@ -437,14 +384,36 @@ \section{Features and Limitations}
how to support it in the generalisation and instantiation functions and which
constraints we should generate for it.
-We are currently also missing support for pairs. Instead, we offer support for
- lists. While pairs pose the problem of potentially having two different types in
-the pair, their fixed size would make them relatively straight-forward to implement.
-Another limitation is that our case blocks only support exactly two alternatives.
+Our case blocks are limited to support for exactly two alternatives.
Generalising to $n$ alternatives would be quite straight-forward, but was dropped
due to time constraints.
+We currently know of one particular case in which our current implementation fails to
+deliver the expected output:
+let f = \lambda x -> x + 1 in
+ let g = \lambda y -> y * 2 in
+ let h = \lambda z -> z 3 in
+ h g + h f
+We expect the result of \emph{h} to be:
+(Nat -> t) ^ {x,y} -> t ^ {z}
+But what we actually get is:
+ (Nat -> t) ^ {x} -> t ^ {z}
+We could not figure out within the time allotted what was causing this to happen. Although
+we suspect that somewhere a substitution is going wrong or a constraint that should have been
+present isn't generated.
\section{Example programs}

No commit comments for this range

Something went wrong with that request. Please try again.