dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Revisions

Browse Source
This commit is contained in:
Daniel Hillerström
2020-02-24 22:27:53 +00:00
parent ba1ea599d8
commit 753996ae9f
1 changed files with 14 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
thesis.tex
View File

@@ -207,7 +207,7 @@ callcc, J, catchcont, etc.
\part{Design} \part{Design}
\chapter{A ML-flavoured programming language based on rows} \chapter{An ML-flavoured programming language based on rows}
\label{ch:base-language} \label{ch:base-language}
In this chapter we introduce a core calculus, \BCalc{}, which we shall In this chapter we introduce a core calculus, \BCalc{}, which we shall
@@ -218,11 +218,11 @@ multi-tier web-programming language
\Links{}~\cite{CooperLWY06}. \Links{} belongs to the \Links{}~\cite{CooperLWY06}. \Links{} belongs to the
ML-family~\cite{MilnerTHM97} of programming languages as it features ML-family~\cite{MilnerTHM97} of programming languages as it features
typical characteristics of ML languages such as a static type system typical characteristics of ML languages such as a static type system
supporting parametric polymorphism with type inference support (in supporting parametric polymorphism with type inference (in fact Links
fact Links supports first-class polymorphism), and its evaluation supports first-class polymorphism), and its evaluation semantics is
semantics is strict. However, \Links{} differentiates itself from the strict. However, \Links{} differentiates itself from the rest of the
rest of the ML-family by making crucial use of \emph{row polymorphism} ML-family by making crucial use of \emph{row polymorphism} to support
to support extensible records, variants, and tracking of computational extensible records, variants, and tracking of computational
effects. Thus \Links{} has a rather strong emphasis on structural effects. Thus \Links{} has a rather strong emphasis on structural
types rather than nominal types. types rather than nominal types.
@@ -247,9 +247,9 @@ and programming with computational effects.
\section{Syntax and static semantics} \section{Syntax and static semantics}
\label{sec:syntax-base-language} \label{sec:syntax-base-language}
In \BCalc{}, types are precursory to terms, as it is intrinsically As \BCalc{} is intrinsically typed, we begin by presenting the syntax
typed. Thus we begin by presenting the syntax of its kind and type of kinds and types in
structure in Section~\ref{sec:base-language-types}. Subsequently in Section~\ref{sec:base-language-types}. Subsequently in
Section~\ref{sec:base-language-terms} we present the term syntax, Section~\ref{sec:base-language-terms} we present the term syntax,
before presenting the formation rules for types in before presenting the formation rules for types in
Section~\ref{sec:base-language-type-rules}. Section~\ref{sec:base-language-type-rules}.
@@ -449,10 +449,11 @@ $\cdot$ for closed rows.
% %
\paragraph{Kinds} \paragraph{Kinds}
The kinds comprise $\Type$ for regular type variables, $\Presence$ for The kinds classify the different categories of types. The $\Type$ kind
presence variables, $\Comp$ for computation type variables, $\Effect$ classifies for value types, $\Presence$ classifies presence
for effect variables, and lastly $\Row_{\mathcal{L}}$ for row annotations, $\Comp$ classifies computation types, $\Effect$
variables. classifies effect types, and lastly $\Row_{\mathcal{L}}$ classifies
rows.
% %
The formation rules for kinds are given in The formation rules for kinds are given in
Figure~\ref{fig:base-language-kinding}. The kinding judgement Figure~\ref{fig:base-language-kinding}. The kinding judgement