\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_\ell}}{\ell}}
      \infer1{\jdgmnt{ty}{\Psi}{\prod_{\ell \in I} A_\ell}}
    \end{prooftree}
    \quad
    \begin{prooftree}
      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_\ell}}{\ell}}
      \infer1{\jdgmnt{ty}{\Psi}{\sum_{\ell \in I} A_\ell}}
    \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:lang-wf}
\end{figure}

In this section we introduce \lang{}, a simply-typed lambda calculus
with \emph{regular types}.  \Cref{fig:lang-wf} shows the
well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
that \(A\) is a type using variables from \(\Psi\). We have labelled
\(n\)-ary products and sums, where the set of labels is finite. Types
satisfy the following substitution lemma:
\begin{proposition}[Type substitution]
  For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and any type
  environment \(\alpha\) that assigns each variable \(X \in \Psi\) to a type
  \(\jdgmnt{ty}{\Theta}{\alpha(X)}\), we have \(\jdgmnt{ty}{\Theta}{\suball{A}{\alpha}}\).
\end{proposition}

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. The \(\mathsf{Set}\) model has 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 would 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{figure}
  \[
  \begin{array}{ccc}
    \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_\ell}{A_\ell}}{\ell}}
      \infer1{\judgement{\Gamma}{\tuple{\rangeover{\ell: t_\ell}{\ell}}}{\prod_{\ell \in I} A_\ell}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement{\Gamma}{t}{\prod_{\ell \in I} A_\ell}}
      \infer1{\judgement{\Gamma}{t.\hat{\ell}}{A_{\hat{\ell}}}}
    \end{prooftree}
    \\\\
    \begin{prooftree}
      \hypo{\judgement{\Gamma}{t}{A_{\hat{\ell}}}}
      \infer1{\judgement{\Gamma}{\hat{\ell}~t}{\sum_{\ell \in I} A_\ell}}
    \end{prooftree}
    &
    \multicolumn{2}{c}{
    \begin{prooftree}
      \hypo{\judgement{\Gamma}{t}{\sum_{\ell \in I} A_\ell}}
      \hypo{\rangeover{\judgement{\Gamma, x_\ell : A_\ell}{t_\ell}{B}}{\ell}}
      \infer2{\judgement{\Gamma}{\casetm{t}{\ell~x_\ell}{t_\ell}{\ell}}{B}}
    \end{prooftree}
    }
    \\\\
    \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:lang-ty}
\end{figure}

\Cref{fig:lang-ty} 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 value and a body which
transforms an 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.

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~(\mathsf{Leaf}~\tuple{}) &&: \mathsf{Tree} \\
  \mathsf{branch} &\coloneq \lambda x. \roll~(\mathsf{Branch}~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}{\mathsf{Leaf}~\tuple{}. l; \mathsf{Branch}~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 a vessel. We define \(\maptm{X}{A}\) (shown in \cref{fig:map}) by
induction on a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), with
our chosen variable \(X \in \Psi\).

\begin{figure}
  \begin{align*}
    \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
    \maptm{X}{Y} &\coloneq \lambda f, x. x \qquad (X \neq Y)\\
    \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
    \maptm{X}{\prod_{\ell \in I} A_\ell} &\coloneq \lambda f, x. \tuple{\rangeover{\ell : \maptm{X}{A_\ell}~f~x.\ell}{\ell}} \\
    \maptm{X}{\sum_{\ell \in I} A_\ell} &\coloneq
      \lambda f, x. \casetm{x}{\ell~x_\ell}{\ell~(\maptm{X}{A_i}~f~x_\ell)}{\ell} \\
    \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{Definition of the \mapkw{} meta-operator.}\label{fig:map}
\end{figure}

\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 &= \sub{t}{x/u}
    &
    \casetm{\hat{\ell}~t}{\ell~x_\ell}{u_\ell}{\ell} &= \sub{u_{\hat{\ell}}}{x_{\hat{\ell}}/t}
    \\
    \tuple{\rangeover{\ell : t_\ell}{\ell}}.\hat{\ell} &= t_{\hat{\ell}}
    &
    \dofold{\roll~t}{x}{u} &= \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 recursively folding on
all inductive components too.

\end{document}