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

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

\TODO{
  \begin{itemize}
    \item introduce core language as STLC with regular types
  \end{itemize}
}

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

\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}{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 \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\).

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}{0,\tuple{}. l; 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\).
\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 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}}{\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 recursive values too.

\end{document}