\documentclass[../main.tex]{subfiles}

\begin{document}
\section{Core Language}%
\label{sec:lang}

\begin{figure}
  \[
    \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}

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}.

\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}{\suball{A}{f}}\).
\end{proposition}

\begin{figure}
  \[
  \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}{\tuple{i,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}

\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 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
form two constructors of this type:
\begin{align*}
  \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*}
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}{\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}\), 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)\\
  \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}{\tuple{i,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*}
\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 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}~(\lambda y. \roll~y)~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 we have been unable to encode the \unroll{} operator
such that \(\unroll~(\roll~t) = t\).

\begin{figure}
  \begin{align*}
    (\lambda x. t)~u &\coloneq \sub{t}{x/u}
    &
    \casetm{\tuple{k, t}}{\tuple{i,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}

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}
