Current state of affairs.

1 files changed, 186 insertions, 202 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index c7851e2..3b0134a 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -4,223 +4,207 @@
 \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}
+\TODO{
+  \begin{itemize}
+    \item introduce core language as STLC with regular types
+  \end{itemize}
+}
 
 \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}
+  \[
+    \begin{prooftree}
+      \hypo{X \in \Psi}
+      \infer1{\jdgmnt{ty}{\Psi}{X}}
+    \end{prooftree}
+    \quad
+    \begin{prooftree}
+      \hypo{\jdgmnt{ty}{}{A}}
+      \hypo{\jdgmnt{ty}{}{B}}
+      \infer2{\jdgmnt{ty}{\Psi}{A \to B}}
+    \end{prooftree}
+    \quad
+    \begin{prooftree}
+      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}}
+      \infer1{\jdgmnt{ty}{\Psi}{\prod_i A_i}}
+    \end{prooftree}
+    \quad
+    \begin{prooftree}
+      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}}
+      \infer1{\jdgmnt{ty}{\Psi}{\sum_i A_i}}
+    \end{prooftree}
+    \quad
+    \begin{prooftree}
+      \hypo{\jdgmnt{ty}{\Psi, X}{A}}
+      \infer1{\jdgmnt{ty}{\Psi}{\mu X. A}}
+    \end{prooftree}
+  \]
+  \caption{Well-formedness of \lang{} types}\label{fig:artist-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.
+\Cref{fig:artist-wf} shows the well-formedness judgement for types. Notice that
+for arrow types, the variable context is empty for both premises. Allowing
+variables on the left of arrows leads to non-strictly positive types, which in
+general are impossible to locally encode in System~T. Consider for example the
+positive type \(\mu X. (X \to \nat) \to \nat\). In the \(\mathsf{Set}\) model of
+System~T, this type must be represented by an infinite set containing its power
+set. There is no System~T type with this property, thus we should forbid this
+type. We also forbid variables on the right of arrows. For example, consider the
+type \(\mu X. 1 + (\nat \to X)\) of countable trees. None of the general encoding
+strategies work for this type; G\"odel and heap encodings both require
+constructors that perform infinite work, whilst Church and codata encodings
+would be global\footnote{\textcite{DBLP:books/sp/LongleyN15} claim the type
+unrepresentable in some models of System~T}.
+
+\TODO{
+  \begin{itemize}
+    \item state that type substitution preserves well-formedness
+  \end{itemize}
+}
 
 \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}
+  \[
+  \begin{array}{cccc}
+    \begin{prooftree}
+      \hypo{x : A \in \Gamma}
+      \infer1{\judgement{\Gamma}{x}{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{\judgement{\Gamma}{t}{A}}
+      \hypo{\judgement{\Gamma, x : A}{u}{B}}
+      \infer2{\judgement{\Gamma}{\lettm{t}{x}{u}}{B}}
+    \end{prooftree}
+    \\\\
+    \begin{prooftree}
+      \hypo{\rangeover{\judgement{\Gamma}{t_i}{A_i}}{i}}
+      \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}{\prod_i A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{\prod_i A_i}}
+      \infer1{\judgement{\Gamma}{t.i}{A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{A_i}}
+      \infer1{\judgement{\Gamma}{\tuple{i, t}}{\sum_i A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{\sum_i A_i}}
+      \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}{B}}{i}}
+      \infer2{\judgement{\Gamma}{\casetm{t}{x_i}{t_i}{i}}{B}}
+    \end{prooftree}
+    \\\\
+    \multicolumn{2}{c}{
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{\sub{A}{X/\mu X. A}}}
+      \infer1{\judgement{\Gamma}{\roll~t}{\mu X. A}}
+    \end{prooftree}
+    }
+    &
+    \multicolumn{2}{c}{
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}{\mu X. A}}
+      \hypo{\judgement{\Gamma, x : \sub{A}{X/B}}{u}{B}}
+      \infer2{\judgement{\Gamma}{\foldtm{t}{x}{u}}{B}}
+    \end{prooftree}
+    }
+  \end{array}
+  \]
+  \caption{Typing judgements for \lang{}}\label{fig:artist-types}
 \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.
+\Cref{fig:artist-types} gives the typing judgements for \lang{}. The
+introduction and elimination rules for functions, products and sums are
+standard, as are the rules for variables and let bindings. The \roll{} operator
+introduces an inductive type \(\mu X. A\), by acting as the algebraic map for the
+weak initial \(A\)-algebra. The only eliminator for inductive types is \foldkw{}.
+Given a target of type \(\mu X. A\), the body of the fold is an \(A\)-algebraic
+map. Because \(\mu X. A\) is the weak initial \(A\)-algebra, we can thus construct
+an inhabitant of \(B\).
 
-\begin{figure}
+As a concrete example, consider the type \(\mathsf{Tree} \coloneq \mu X. 1 + (X \times
+X)\) of unlabeled binary trees. By combining injections with \roll{}, we can
+form two constructors of this type:
 \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)}
+  \mathsf{leaf} &\coloneq \roll~\tuple{0, \tuple{}} &&: \mathsf{Tree} \\
+  \mathsf{branch} &\coloneq \lambda x. \roll~\tuple{1, x} &&: \mathsf{Tree} \times \mathsf{Tree} \to \mathsf{Tree}
 \end{align*}
-\caption{Definition of \(\mathsf{map}\)}%
-\label{fig:lang-map}
-\end{figure}
+and given a base case \(l : A\) and accumulator \(r : A \times A \to A\), we
+can fold over a tree \(t\) with the term
+\[ \dofold{t}{x}{\domatch{x}{0,\tuple{}. l; 1,y. r~y}} \]
 
-\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}
+From the core of \lang{} we can further derive a number of useful operators. One
+of these is \mapkw, which lifts a function from type \(B \to C\) to \(\sub{A}{X/B}
+\to \sub{A}{X/C}\). We define \(\maptm{X}{A}\) by induction on the well-formedness
+derivation \(\jdgmnt{ty}{\Psi}{A}\), with our chosen variable \(X \in \Psi\).
 \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}
+  \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
+  \maptm{X}{Y} &\coloneq \lambda f, x. x && (X \neq Y)\\
+  \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
+  \maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\
+  \maptm{X}{\sum_i A_i} &\coloneq
+    \lambda f, x. \casetm{x}{x_i}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
+  \maptm{X}{\mu Y. A} &\coloneq
+  \lambda f, x.
+    \dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)}
 \end{align*}
-\caption{Equational theory for \lang{}}%
-\label{fig:lang-eq}
+\begin{proposition}
+The following typing judgement for \mapkw{} is sound.
+\begin{prooftree*}
+  \hypo{\jdgmnt{ty}{X}{A}}
+  \infer1{\judgement{\Gamma}{\maptm{X}{A}}{(B \to C) \to \sub{A}{X/B} \to \sub{A}{X/C}}}
+\end{prooftree*}
+\end{proposition}
+
+In \cref{subsec:encoding-strategies} we claimed that the three important operations
+for inductive types are constructors, folding and pattern matching. The core of
+\lang{} has constructors via the \roll{} operator and folding via \foldkw{}, yet
+it does not have pattern matching. We can derive pattern matching from the
+\unroll{} operator, defined as
+\begin{gather*}
+  \unroll_{\mu X. A}~t \coloneq \dofold{t}{x}{\maptm{X}{A}~\roll~x}.
+\shortintertext{with the derived typing judgement}
+  \begin{prooftree}
+    \hypo{\judgement{\Gamma}{t}{\mu X. A}}
+    \infer1{\judgement{\Gamma}{\unroll~t}{\sub{A}{X/\mu X. A}}}
+  \end{prooftree}
+\end{gather*}
+where variable \(x\) has type \(\sub{A}{X/\sub{A}{X/\mu X. A}}\). We have
+decided against adding \unroll{} to the core language. The main reason is that
+for our encoding into System~T, it is difficult to encode the \unroll{} operator
+such that \(\unroll~(\roll~t) = t\). The best encodings we found were
+contextually equivalent, so we exclude \unroll{} from the core language so users
+do not accidentally depend on an equation that does not hold.
+
+\begin{figure}
+  \begin{align*}
+    (\lambda x. t)~u &\coloneq \sub{t}{x/u}
+    &
+    \casetm{\tuple{k, t}}{x_i}{u_i}{i} &\coloneq \sub{u_k}{x_k/t}
+    \\
+    \tuple{\rangeover{t_i}{i}}.k &\coloneq t_k
+    &
+    \dofold{\roll~t}{x}{u} &\coloneq \sub{u}{x/\mapkw{}~(\lambda y. \dofold{y}{x}{u})~t}
+  \end{align*}
+  \caption{The equational theory of \lang{}}\label{fig:lang-theory}
 \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}
+The equational theory for \lang{} is shown in \cref{fig:lang-theory}. The
+equations for functions, products and sums are standard \(\beta\)-reductions.
+Reducing inductive types requires the \mapkw{} operator, as folding a
+value requires folding on all recursive values too.
 
 \end{document}