Before the big rewrite

1 files changed, 226 insertions, 0 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
new file mode 100644
index 0000000..c7851e2
--- /dev/null
+++ b/sec/lang.ltx
@@ -0,0 +1,226 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+\section{Core Language}%
+\label{sec:lang}
+
+In this section, we describe \lang{} a new calculus with higher-order functions
+and regular types~\cite{Squid:unpublished/McBride01}. We start by describing the
+types within the language: products, sums, recursive types and functions. We
+then describe the syntax which is standard for n-ary products and sums. We also
+define a \mapkw{} operation over arbitrary (covariant) functors.\@ \mapkw{} is
+necessary to define the equational theory of \foldkw{}, the eliminator for
+recursive types. The equational theory has \(\beta\) equalities, but no \(\eta\)
+equalities, a consequence of the embedding into System~T.
+
+Types for \lang{}, in \cref{fig:lang-wf}, are given relative to a context of
+type variables. The judgement \(\jdgmnt{ty}{\Theta}{A}\) states that \(A\) is a
+well-formed type in with variables from context \(\Theta\). Products and sums
+are well-formed when each of the n-ary components are well-formed. The recursive
+type \(\mu X. A\) is formed from a type \(A\) in a context extended by \(X\).
+The other type formation rules ensure that \(X\) is used strictly positively,
+and thus that recursive types are well-formed. In particular the rule forming
+function types forbids using any type variables on the left of the arrow. This
+forbids the use of type variables in negative positions. The function type
+formation rule also forbids variables on the right.  This is to forbid types
+such as \(\mu X. 1 + \nat \to X\) of countable trees, as such a type cannot be
+represented by System~T~\cite{proof}. Well-formed types also respect
+substitution:
+\begin{proposition}[Type Substitution]
+Given \(\jdgmnt{ty}{\Theta}{A}\) and \(\jdgmnt{ty}{\Psi}{B_i}\) where \(i\)
+ranges from \(0\) to \(\lvert \Theta \rvert\), we have
+\(\jdgmnt{ty}{\Psi}{\FIXME{\sub{A}{X_i/B_i}}}\).
+\end{proposition}
+
+\begin{figure}
+\[
+\begin{array}{ccccc}
+  \begin{prooftree}
+    \hypo{
+      X \in \Theta
+      \vphantom{\jdgmnt{ty}{\Theta}{A}} %% Spooky formatting phantom
+    }
+    \infer1{\jdgmnt{ty}{\Theta}{X}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\rangeover{\jdgmnt{ty}{\Theta}{A_i}}{i<n}}
+    \infer1{\jdgmnt{ty}{\Theta}{\prod_i^n A_i}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\rangeover{\jdgmnt{ty}{\Theta}{A_i}}{i<n}}
+    \infer1{\jdgmnt{ty}{\Theta}{\sum_i^n A_i}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{
+      \jdgmnt{ty}{\Theta, X}{A}
+      \vphantom{\rangeover{\jdgmnt{ty}{\Theta}{A}}{i<n}} %% Spooky formatting phantom
+    }
+    \infer1{
+      \jdgmnt{ty}{\Theta}{\mu X.A}
+      \vphantom{\jdgmnt{ty}{\Theta}{\sum_i^n A_i}} %% Spooky formatting phantom
+    }
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\jdgmnt{ty}{}{A}}
+    \hypo{\jdgmnt{ty}{}{B}}
+    \infer2{\jdgmnt{ty}{\Theta}{A \to B}}
+  \end{prooftree}
+\end{array}
+\]
+\caption{Well-formedness of \lang{} types}%
+\label{fig:lang-wf}
+\end{figure}
+
+We present terms in \cref{fig:lang-type}. All type variables must be bound
+within recursive types, so there is no type context. The typing rules for
+variables, functions, products and sums are standard. Values of a recursive type
+\(\mu X. A\) are constructed using \emph{rolling}. A value of type
+\(\sub{A}{X/\mu X. A}\) is rolled into one of type \(\mu X. A\). Recursive types
+are eliminated by \emph{folding}. To fold a target of type \(\mu X. A\) into
+type \(B\), it is necessary to describe how to transform \(\sub{A}{X/B}\) into
+\(B\). By only allowing eliminations of this form, we ensure that all recursion
+is well-founded.
+
+\begin{figure}
+\[
+\begin{array}{cc}
+  \begin{prooftree}
+    \hypo{x : A \in \Gamma}
+    \infer1{\judgement{\Gamma}{x}{A}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{x}{A}}
+    \infer1{\judgement{\Gamma}{(x : A)}{A}}
+  \end{prooftree}
+  \\\\
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma, x : A}{t}{B}}
+    \infer1{\judgement{\Gamma}{\lambda x.~t}{A \to B}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{f}{A \to B}}
+    \hypo{\judgement{\Gamma}{t}{A}}
+    \infer2{\judgement{\Gamma}{f~t}{B}}
+  \end{prooftree}
+  \\\\
+  \begin{prooftree}
+    \hypo{\rangeover{\judgement{\Gamma}{t_i}{A_i}}{i<n}}
+    \infer1{\judgement{\Gamma}{\tuple*{\rangeover{t_i}{i<n}}}{\prod_i^n A_i}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{e}{\prod_i^n A_i}}
+    \infer1{\judgement{\Gamma}{e.k}{A_k}}
+  \end{prooftree}
+  \\\\
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{t}{A_k}}
+    \infer1{\judgement{\Gamma}{\tuple{k, t}}{\sum_i^n A_i}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{e}{\sum_i^n A_i}}
+    \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}{B}}{i<n}}
+    \infer2{\judgement{\Gamma}{\casetm{e}{x_i}{t_i}{i}{n}}{B}}
+  \end{prooftree}
+  \\\\
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{t}{\sub{A}{X/\mu X.A}}}
+    \infer1{\judgement{\Gamma}{\mathsf{roll}~t}{A}}
+  \end{prooftree}
+  &
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{e}{\mu X.A}}
+    \hypo{\judgement{\Gamma, x : \sub{A}{X/B}}{t}{B}}
+    \infer2{\judgement{\Gamma}{\foldtm{e}{x}{t}}{B}}
+  \end{prooftree}
+\end{array}
+\]
+\caption{Typing judgements for \lang{}}%
+\label{fig:lang-type}
+\end{figure}
+
+Using these typing rules, we can derive a map operation for any \emph{functor},
+a type with a single free type variable:
+\[
+\begin{prooftree}
+  \hypo{\jdgmnt{ty}{X}{F}}
+  \hypo{\jdgmnt{ty}{}{B}}
+  \hypo{\jdgmnt{ty}{}{C}}
+  \infer3{
+    \judgement
+      {\Gamma}
+      {\maptm{X}{F}^{A, B}}
+      {(A \to B) \to \sub{F}{X/A} \to \sub{F}{X/B}}}
+\end{prooftree}
+\]
+The definition of \mapkw, \cref{fig:lang-map}, proceeds by \TODO{induction}. We
+will elide the superscripts. The hardest case to understand is recursive types
+\(\mu Y. A\). Given a value of type \(\mu Y. \sub{G}{X/B}\), we need to
+construct a value of type \(\mu Y. \sub{G}{X/C}\). By folding over the given
+value, we need to map \(\sub{G}{X/B, Y/\mu Y. \sub{G}{X/C}}\) into \(\mu Y.
+\sub{G}{X/C}\). We can construct such a value by rolling, thus we need to
+produce a value of type \(\sub{G}{X/C, Y/\mu Y.\sub{G}{X/C}}\). Note that our
+given value from the fold and the result we want to roll both agree on the type
+of \(Y\) within \(G\), and only disagree on the type assigned to \(X\). Thus we
+use map recursively.
+
+\begin{figure}
+\begin{align*}
+  \maptm{X}{X}^{A,B}~f~t &= f~t \\
+  \maptm{X}{Y}^{A,B}~f~t &= t \qquad\qquad (Y \neq X) \\
+  \maptm{X}{A \to B}^{C,D}~f~t &= t \\
+  \maptm{X}{\prod_i^n A_i}^{B,C}~f~t &=
+    \tuple*{\rangeover{\maptm{X}{A_i}^{B,C}~f~t.i}{i<n}} \\
+  \maptm{X}{\sum_i^n A_i}^{B,C}~f~t &=
+    \casetm{t}{x_i}{\tuple{i, \maptm{X}{A_i}^{B,C}~f~x_i}}{i}{n} \\
+  \maptm{X}{\mu Y.A}^{B,C}~f~t &=
+    \foldtm{t}{x}{\mathsf{roll}~(\maptm{X}{\sub{A}{Y/\mu Y.\sub{A}{X/C}}}^{B,C}~f~x)}
+\end{align*}
+\caption{Definition of \(\mathsf{map}\)}%
+\label{fig:lang-map}
+\end{figure}
+
+\Cref{fig:lang-eq} shows the equational theory for \lang{}. We have the standard
+\(\beta\) equalities for functions, products and sums. We do not have \(\eta\)
+equalities for products or sums as these are no satisfied by the System~T
+embedding. We also don't have \(\eta\) equalities for functions as our
+equational theory for System~T does not have them either. The \(\beta\) law for
+recursive types depends on the map operation.
+
+\begin{figure}
+\begin{align*}
+  (t : A) &= t \\
+  (\lambda x.~t)~u &= \sub{t}{x/u} \\
+  \tuple*{\rangeover{t_i}{i<n}}.k &= t_k \\
+  \casetm{\tuple{k, t}}{x_i}{u_i}{i}{n} &= \sub{u_k}{x_k/t} \\
+  \foldtm{\mathsf{roll}~t}{x}{u} &=
+    \sub{u}{x/\maptm{X}{A}~(\lambda y.~\foldtm{y}{x}{u})~t}
+\end{align*}
+\caption{Equational theory for \lang{}}%
+\label{fig:lang-eq}
+\end{figure}
+
+\begin{example}
+  We can use folding and \(\mapkw\) do derive an \emph{unrolling} operation
+  \begin{gather*}
+    \mathsf{unroll}_{X. A}~t \coloneq \foldtm{t}{x}{\maptm{X}{A}~\mathsf{roll}~x} \\
+  \shortintertext{with typing rule}
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{\mu X. A}}
+      \infer1{\judgement{\Gamma}{\mathsf{unroll}~t}{\sub{A}{X/\mu X. A}}}
+    \end{prooftree} \\
+  \shortintertext{From the equational theory, we find}
+    \mathsf{unroll}~(\mathsf{roll}~t) =
+      \maptm{X}{A}~\mathsf{roll}~(\maptm{X}{A}~\mathsf{unroll}~t)
+  \end{gather*}
+  which in general doesn't simplify further.
+\end{example}
+
+\end{document}