Revise Core Language.

1 files changed, 58 insertions, 49 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index 1ad22d4..e675a85 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -4,12 +4,6 @@
 \section{Core Language}%
 \label{sec:lang}
 
-\TODO{
-  \begin{itemize}
-    \item introduce core language as STLC with regular types
-  \end{itemize}
-}
-
 \begin{figure}
   \[
     \begin{prooftree}
@@ -41,25 +35,31 @@
   \caption{Well-formedness of \lang{} types}\label{fig:artist-wf}
 \end{figure}
 
-\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
+In this section we introduce \lang{}, a simply-typed lambda calculus
+with \emph{regular types}.  \Cref{fig:artist-wf} shows the
+well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
+that \(A\) is a type using variables from \(\Psi\). 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{proposition}[Type substitution]
+  For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and a
+  substitution from variables \(X \in \Psi\) to types
+  \(\jdgmnt{ty}{\Theta}{f(X)}\), we have
+  \(\jdgmnt{ty}{\Theta}{\submult{A}{f}}\).
+\end{proposition}
 
 \begin{figure}
   \[
@@ -127,13 +127,20 @@ unrepresentable in some models of System~T}.
 \end{figure}
 
 \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\).
+introduction and elimination rules for functions, products and sums
+are standard, as are the rules for variables and let bindings. The two
+new operators, \roll{} and \foldkw{}, introduce values of an inductive
+type \(\mu X. A\). The \roll{} operator takes a vessel of shape \(A\)
+filled with inductive components and rolls it into an inductive
+value. The \foldkw{} operator takes a target inductive value and a
+body, which tranforms the induction hypothesis into a value of the
+motive type. By recursively applying the body to the inductive
+components of the target, the \foldkw{} computes a result.
+
+For those who are categorically minded, \roll{} is an algebraic map
+for a weak initial \(A\)-algebra (viewing \(A\) as an endofunctor) and
+\foldkw{} is the weak universal map. The structure is weak-universal
+as it is not guaranteed to be unique, only to exist.
 
 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
@@ -144,12 +151,14 @@ form two constructors of this type:
 \end{align*}
 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}} \]
+\[ \dofold{t}{x}{\domatch{x}{\tuple{0,\tuple{}}. l; \tuple{1,y}. r~y}} \]
 
-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\).
+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}\), acting on each component
+in the vessel. 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*}
   \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
   \maptm{X}{Y} &\coloneq \lambda f, x. x && (X \neq Y)\\
@@ -169,13 +178,14 @@ The following typing judgement for \mapkw{} is sound.
 \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
+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 operators for constructing
+and folding over inductive values, 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}.
+  \unroll_{\mu X. A}~t \coloneq \dofold{t}{x}{\maptm{X}{A}~(\lambda y. \roll~y)~x}.
 \shortintertext{with the derived typing judgement}
   \begin{prooftree}
     \hypo{\judgement{\Gamma}{t}{\mu X. A}}
@@ -184,10 +194,8 @@ it does not have pattern matching. We can derive pattern matching from the
 \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.
+for our encoding into System~T we have been unable to encode the \unroll{} operator
+such that \(\unroll~(\roll~t) = t\).
 
 \begin{figure}
   \begin{align*}
@@ -202,9 +210,10 @@ do not accidentally depend on an equation that does not hold.
   \caption{The equational theory of \lang{}}\label{fig:lang-theory}
 \end{figure}
 
-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.
+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
+inductive components too.
 
 \end{document}