From d4f7f8a85340037727fe79c23050cc7546769182 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 16 Dec 2019 19:15:28 +0000 Subject: [PATCH] On the syntax of types and terms. --- macros.tex | 43 +++++++++++++++++++++++++++++------ thesis.tex | 67 +++++++++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 95 insertions(+), 15 deletions(-) diff --git a/macros.tex b/macros.tex index f0bd912..faa4992 100644 --- a/macros.tex +++ b/macros.tex @@ -9,12 +9,6 @@ %% %% Calculi terms and types type-setting. %% -\newcommand{\slab}[1]{\textrm{#1}} -\newcommand{\semlab}[1]{\text{\scshape{S-#1}}} -\newcommand{\tylab}[1]{\text{\scshape{T-#1}}} -\newcommand{\mlab}[1]{\text{\scshape{M-#1}}} -\newcommand{\siglab}[1]{\text{\scshape{Sig-#1}}} -\newcommand{\klab}[1]{#1} \newcommand{\revto}{\ensuremath{\leftarrow}} \newcommand{\dec}[1]{\mathsf{#1}} @@ -69,6 +63,8 @@ \newcommand{\True}{\mathsf{true}} \newcommand{\False}{\mathsf{false}} +\newcommand{\eff}{!} + %% Handler projections. \newcommand{\hret}{H^{\mathrm{val}}} \newcommand{\hval}{\hret} @@ -78,4 +74,37 @@ \newcommand{\alertbox}[2]{{\par\noindent\small\color{red} \framebox{\parbox{\dimexpr\linewidth-2\fboxsep-2\fboxrule}{\textbf{#1:} #2}}}} \newcommand{\todo}[1]{\alertbox{TODO}{#1}} -\newcommand{\dhil}[1]{\alertbox{Daniel}{#1}} \ No newline at end of file +\newcommand{\dhil}[1]{\alertbox{Daniel}{#1}} + +%% +%% Labels +%% +\newcommand{\slab}[1]{\textrm{#1}} +\newcommand{\semlab}[1]{\text{\scshape{S-#1}}} +\newcommand{\tylab}[1]{\text{\scshape{T-#1}}} +\newcommand{\mlab}[1]{\text{\scshape{M-#1}}} +\newcommand{\siglab}[1]{\text{\scshape{Sig-#1}}} + +%% +%% Lindley's array stuff. +%% +\newcommand{\ba}{\begin{array}} +\newcommand{\ea}{\end{array}} + +\newcommand{\bl}{\ba[t]{@{}l@{}}} +\newcommand{\el}{\ea} + + +%% +%% Lindley's syntax, reductions, equations, and derivation environments. +%% +\newenvironment{syntax}{\[\ba{@{}l@{\quad}r@{~}c@{~}l@{}}}{\ea\]\ignorespacesafterend} +\newenvironment{reductions}{\[\ba{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}}{\ea\]\ignorespacesafterend} + +\newenvironment{eqs}{\ba{@{}r@{~}c@{~}l@{}}}{\ea} +\newenvironment{equations}{\[\ba{@{}r@{~}c@{~}l@{}}}{\ea\]\ignorespacesafterend} +\newenvironment{derivation}{\begin{displaymath}\ba{@{}r@{~}l@{}}}{\ea\end{displaymath}\ignorespacesafterend} +\newcommand{\reason}[1]{\quad (\text{#1})} + + +\newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 7170184..1ef2e09 100644 --- a/thesis.tex +++ b/thesis.tex @@ -18,6 +18,8 @@ \usepackage{array} \usepackage{float} % Float control \usepackage{caption,subcaption} % Sub figures support +\DeclareCaptionFormat{underlinedfigure}{#1#2#3\hrulefill} +\captionsetup[figure]{format=underlinedfigure} \usepackage[T1]{fontenc} % Fixes font issues %\usepackage{lmodern} \usepackage[activate=true, @@ -195,12 +197,13 @@ multi-tier web-programming language \Links{}~\cite{CooperLWY06}. \Links{} belongs to the ML-family~\cite{MilnerTHM97} of programming languages as it features typical characteristics of ML languages such as a static type system -supporting parametric polymorphism and type inference, and its -evaluation semantics is strict. However, \Links{} differentiates -itself from the rest of the ML-family by making crucial use of -\emph{row polymorphism} to support extensible records, variants, and -tracking of computational effects. Thus \Links{} has a rather strong -emphasis on structural types rather than nominal types. +supporting parametric polymorphism with type inference support (in +fact Links supports first-class polymorphism), and its evaluation +semantics is strict. However, \Links{} differentiates itself from the +rest of the ML-family by making crucial use of \emph{row polymorphism} +to support extensible records, variants, and tracking of computational +effects. Thus \Links{} has a rather strong emphasis on structural +types rather than nominal types. \CoreLinks{} captures all of these properties of \Links{}. Our calculus \BCalc{} differs in several aspects from \CoreLinks{}. For @@ -223,14 +226,62 @@ and programming with computational effects. \section{Syntax and static semantics} \label{sec:syntax-base-language} +Typically the presentation of a programming language begins with its +syntax. If the language is typed there are two possible starting +points: Either one presents the term syntax first, or alternatively, +the type syntax first. Although the choice may seem rather benign +there is, however, a philosophical distinction to be drawn between +them. Terms are, on their own, entirely meaningless, whilst types +provide, on their own, an initial approximation of the semantics of +terms. This is particularly true in an intrinsic typed system perhaps +less so in an extrinsic typed system. In an intrinsic system types +must necessarily be precursory to terms, as terms ultimately depend on +the types. Following this argument leaves us with no choice but to +first present the type syntax of \BCalc{} and subsequently its term +syntax. + +\subsection{Types, kinds, and their environments} +\label{sec:base-language-types} + +Figure~\ref{fig:base-language-types} depicts the syntax for types of +\BCalc{}. + +\begin{figure} + \begin{syntax} + \slab{Value types} &A,B &::= & A \to C + \mid \alpha + \mid \forall \alpha^K.C + \mid \Record{R} + \mid [R]\\ +\slab{Computation types} + &C,D &::= & A \eff E \\ +\slab{Effect types} &E &::= & \{R\}\\ +\slab{Row types} &R &::= & \ell : P;R \mid \rho \mid \cdot \\ +\slab{Presence types} &P &::= & \Pre{A} \mid \Abs \mid \theta\\ +%\slab{Labels} &\ell & & \\ +\slab{Handler types} &F &::= & C \Rightarrow D \\ +\slab{Types} &T &::= & A \mid C \mid E \mid R \mid P \mid F \\ +\slab{Kinds} &K &::= & \Type \mid \Row_\mathcal{L} \mid \Presence + \mid \Comp \mid \Effect \mid \Handler \\ +\slab{Label sets} &\mathcal{L} &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\ +%\slab{Type variables} &\alpha, \rho, \theta& \\ +\slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\ +\slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K + \end{syntax} + \caption{Syntax of types in \BCalc{}}\label{fig:base-language-types} +\end{figure} + +\subsection{Terms} +\label{sec:base-language-terms} + +\section{Dynamic semantics} + \section{Type and effect inference} \dhil{While I would like to detail the type and effect inference, it may not be worth the effort. The reason I would like to do this goes back to 2016 when Richard Eisenberg asked me about how we do effect inference in Links.} -\section{Dynamic semantics} - \chapter{Unary handlers} \label{ch:unary-handlers}