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/embedding.ltx | 65 -------------------------------------------------------
 1 file changed, 65 deletions(-)
 delete mode 100644 sec/embedding.ltx

(limited to 'sec/embedding.ltx')

diff --git a/sec/embedding.ltx b/sec/embedding.ltx
deleted file mode 100644
index 722eff1..0000000
--- a/sec/embedding.ltx
+++ /dev/null
@@ -1,65 +0,0 @@
-\documentclass[../main.tex]{subfiles}
-
-\begin{document}
-\section{Embedding in System T}%
-\label{sec:embedding}
-
-A major motivation for \lang{} is the ability to write terms with regular types
-and embed them in System~T. We explain how the embedding works, which encodes
-products, sums and recursive types as System~T types.
-
-Every pair of System~T types has a union (in the sense of C). The union has
-injections into it and projections out of it. The specification of the union
-type, \(A \sqcup B\) for types is:
-\[
-  \begin{array}{cc}
-    \mathsf{inl} : A \to A \sqcup B &
-    \mathsf{inr} : B \to A \sqcup B \\
-    \mathsf{prl} : A \sqcup B \to A &
-    \mathsf{prr} : A \sqcup B \to B \\
-    \mathsf{prl}~(\mathsf{inl}~t) = t &
-    \mathsf{prr}~(\mathsf{inr}~t) = t
-  \end{array}
-\]
-\Cref{fig:union-impl} shows \posscite{Squid:online/Kiselyov22} implementation of
-unions. We can extend this to n-ary unions \(\bigsqcup_i^n A_i\) in the usual
-way. We pick \(\nat\) to represent the empty union arbitrarily.
-
-With unions, it becomes easy to encode products.
-\textcite{Squid:online/Kiselyov22} uses the functional encoding \(\prod_i^n A_i
-\coloneq \nat \to \bigsqcup_i^n A_i\), representing the product as a
-heterogeneous vector. The \(k\)th component of the product is accessed by
-applying the product to \(k\). Tupling does a case analysis of the argument,
-returning the corresponding value.
-
-\textcite{Squid:online/Kiselyov22} also describes how to encode sums using
-products and unions. A sum is encoded as a tagged union \(\sum_i^n A_i \coloneq
-\nat \times \bigsqcup_i^n A_i\), where the tag indicates which case of the sum
-is being stored. Case analysis first inspects the tag to decide which branch to
-take, downcasts the value to the correct type, and then performs the branch
-action. Note this encoding is not consistent: the empty type is necessarily
-inhabited, as all System~T types are. This inconsistency is necessary for the
-encoding of recursive types.
-
-Recursive types are the most difficult to encode.
-\textcite{DBLP:books/sp/LongleyN15} describe one strategy: represent values as a
-heap. We have the encoding \(\mu X. A \coloneq \nat \times \nat \times (\nat \to
-\sub{A}{X/\nat})\). The first component is the ``depth'' of the heap: an upper
-bound on the number of pointers to follow on any arbitrary path. The second
-component represents the root index of the heap---the address where the data
-structure starts. The final component is the heap itself. Each location stores
-data associated with its value. Any recursion is replaced with a pointer to a
-different location in the heap.
-
-\TODO{example}
-
-Folding is easier to compute than rolling. The precise encoding is given below.
-We compute the fold across the heap in parallel, iteratively increasing the
-depth of paths we can safely use. The initial result is arbitrary: we don't have
-any data to operate on.
-
-\begin{multline*}
-\TODO{fold}
-\end{multline*}
-
-\end{document}
-- 
cgit v1.2.3