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

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

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

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

\begin{figure}
\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)}
\end{align*}
\caption{Definition of \(\mathsf{map}\)}%
\label{fig:lang-map}
\end{figure}

\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}
\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}
\end{align*}
\caption{Equational theory for \lang{}}%
\label{fig:lang-eq}
\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}

\end{document}