From 4353f331b5ab4af157f576f54b1cc79dd08abb12 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 23 Apr 2025 15:59:22 +0100
Subject: Current state of affairs.

---
 sec/intro.ltx | 96 +----------------------------------------------------------
 1 file changed, 1 insertion(+), 95 deletions(-)

(limited to 'sec/intro.ltx')

diff --git a/sec/intro.ltx b/sec/intro.ltx
index 00a6d5b..0cd7b1d 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -4,100 +4,6 @@
 \section{Introduction}%
 \label{sec:intro}
 
-System~T is an extension of the simply-typed lambda calculus adding natural
-numbers and primitive recursion. This minimality makes it an excellent calculus
-to model, and yet the calculus is expressive enough to perform a wide array of
-useful calculations. This includes most arithmetic, \TODO{middle thing} and even
-rewriting of lambda terms.
-
-The restricted type system of System~T makes expressing complex data difficult.
-Often structured data has to be encoded as naturals or first-order functions.
-Encoding data within a natural number often makes structural recursion
-exceedingly complex. Whilst using first-order functions can make recursion
-easier, it is often the case that passing different arguments can return
-different shapes of data.
-
-Consider the following System~T pseudocode:
-\begin{listing}[H]
-  \begin{systemt}
-  let sum (tree : nat -> nat -> nat -> nat -> nat) : nat =
-    let depth = tree 0 0 0 0 in
-    let root  = tree 1 0 0 0 in
-    let heap  = tree 2 in
-    let go : nat -> nat = primrec depth with
-      Z      => fun i => i
-    | S(acc) => fun i =>
-      let tag = heap i 0 0 in
-      let v   = heap i 1 in
-      if tag == 0 then
-        v 0
-      else
-        acc (v 0) + acc (v 1)
-  \end{systemt}
-  \vspace{-\baselineskip}
-\end{listing}
-From the name and type, one can deduce this performs a sum over some tree
-structure. With some more thought, you may be able to work out that
-\systemtinline{tree} is a binary tree. This information is not at all available
-in its type. It is also unclear why \systemtinline{tree 0 0 0 0} should return
-the depth of the tree and \systemtinline{tree 1 0 0 0} the root.
-
-In other functional programming languages, the same sum function would look
-something like the following OCaml code:
-\begin{listing}[H]
-  \begin{minted}{ocaml}
-  let sum tree = match tree with
-    Leaf(v)             -> v
-  | Branch(left, right) -> sum left + sum right
-  \end{minted}
-  \vspace{-\baselineskip}
-\end{listing}
-In this example it is immediately obvious what the function does. The code is
-first order reducing its complexity and the richer type system makes it easier
-to identify the role of different variables. These additional features of OCaml
-and other such languages improve the closeness of mapping and
-role-expressiveness of the code whilst reducing the error-proneness (\TODO{check
-  this}). This is great for human programmers but this comes at a modelling
-cost. Unlike System~T, most functional languages allow non-termination. For
-example, OCaml would have no issue with us writing
-\mintinline{ocaml}{sum tree + sum right} by mistake.
-
-In this work we present \lang{}, a new intermediate language that compiles into
-System~T. \lang{} extends the simply-typed lambda calculus with the regular
-types~\cite{Squid:unpublished/McBride01}: finite products, finite sums and some
-inductive types.\@ \lang{} has most of the expressive types we are used to from
-functional languages---we can write code similar to the second example---whilst
-still being simple enough to represent within System~T.
-
-The type encodings used to compile \lang{} into System~T are
-well-known~\cites{Squid:online/Kiselyov22}{DBLP:books/sp/LongleyN15}. Encoding
-products and sums relies on C-style union types, which exist due to System~T
-having only naturals and function types. Recursive types are represented using a
-heap with an explicit depth, informally described by
-\textcite{DBLP:books/sp/LongleyN15}. We have written this compilation algorithm
-within \lang{} itself.
-
-To aid in the development of this program, we also constructed a type checker
-for \lang{} in Idris~2~\cite{idris}. The typechecker uses intrisically
-well-scoped syntax. The syntax is represented by an indexed data type
-\texttt{Term}, where the index describes the variables that are in scope. By
-using quantities~\cite{quants} and auto-implicit search, the compiler code is
-written in a named style, yet compiles down to using deBruijn indices. Using
-names helps to reduce errors in the code, and the compilation to deBruijn
-indices means we don't pay any runtime cost.
-
-%% \subsubsection*{Contributions}%
-%% \label{sec:contributions}
-%% \begin{itemize}
-%% \item Design of new intermediate language \lang{}, featuring iso-recursive
-%%   regular types
-%% \item Algorithm for embedding \lang{} into to System~T, implementable within
-%%   \lang{}
-%% \item Case study implementation of a fuelled self-reducer for System~T,
-%%   demonstrating improvements in several cognitive dimensions~\cite{cog-dim} for
-%%   \lang{} compared to working in System~T directly
-%% \item Compiler implemented in Idris 2 with intrinsically well-scoped syntax and
-%%   runtime-erased typechecking proofs.
-%% \end{itemize}
+\TODO{}
 
 \end{document}
-- 
cgit v1.2.3

