diff options
| -rw-r--r-- | lexer.py | 4 | ||||
| -rw-r--r-- | main.bib | 8 | ||||
| -rw-r--r-- | main.tex | 136 | ||||
| -rw-r--r-- | sec/compiler.ltx | 25 | ||||
| -rw-r--r-- | sec/embedding.ltx | 65 | ||||
| -rw-r--r-- | sec/encoding.ltx | 132 | ||||
| -rw-r--r-- | sec/intro.ltx | 96 | ||||
| -rw-r--r-- | sec/lang.ltx | 388 | ||||
| -rw-r--r-- | sec/reducer.ltx | 35 | ||||
| -rw-r--r-- | sec/related.ltx | 1 | ||||
| -rw-r--r-- | sec/systemt.ltx | 330 |
11 files changed, 734 insertions, 486 deletions
@@ -7,9 +7,9 @@ from pathlib import Path class SystemTLexer(OcamlLexer): name = 'System T' aliases = ['syst'] - filenames = ['*.syst'] # just to have one if you whant to use + filenames = ['*.syst'] - EXTRA_KEYWORDS = ['primrec', 'prl', 'prr', 'fold'] + EXTRA_KEYWORDS = ['primrec', 'fold', 'foldmatch', 'roll'] def get_tokens_unprocessed(self, text): for index, token, value in OcamlLexer.get_tokens_unprocessed(self, text): @@ -59,6 +59,14 @@ urldate = {2024-09-16} } +@unpublished{Squid:unpublished/Bauer17, + author = {Andrej Bauer}, + title = {On Self-Interpreters for {System~T} and Other Typed \(\lambda\)-Calculi}, + year = {2026}, + url = {http://math.andrej.com/wp-content/uploads/2016/01/self-interpreter-for-T.pdf}, + urldate = {2025-04-02} +} + @book{DiscoverEd:book/oc/Cantor52, author = {Cantor, Georg}, title = {Contributions to the Founding of the Theory of Transfinite Numbers}, @@ -37,6 +37,7 @@ \usepackage{hyperref} %% hyperlinks within document \usepackage{mathtools} %% matrix alignment \usepackage[outputdir=build]{minted} %% code formatting +\usepackage{pifont} %% Check and cross marks \usepackage{stackrel} %% Annotating judgements \usepackage{subcaption} %% subfigures with captions \usepackage{subfiles} %% splitting file into sections @@ -166,40 +167,127 @@ %%% Term syntax -%% Godel encoding +%% Let +\newcommand\letkw{\ensuremath{\mathsf{let}}} +\newcommand\lettm[3]{\letkw~{#2} \coloneq {#1}~\mathsf{in}~{#3}} +\ExplSyntaxOn +\NewDocumentCommand \squid_letpart {m m} + { \letkw & {#1} = \cr + & {#2} \cr + \mathsf{in} & + } +\NewDocumentCommand \squid_contlet {> {\SplitArgument{1}{=}} m} + { \squid_letpart #1 \squid_checklet [\cr] + } +\NewDocumentCommand \squid_checklet {o s m} + { \IfBooleanTF{#2} + { \IfNoValueF{#1}{#1} & {#3} + \end{array} + \wlog{End~let} + } + { \IfNoValueF{#1}{#1} \squid_contlet {#3} + } + } +\NewDocumentCommand \dolet {O{t}} + { \arraycolsep=0.2em + \wlog{Begin~let} + \begin{array}[#1]{ll} + \squid_checklet + } +\ExplSyntaxOff + +%% Encoding \newcommand\encode[1]{\llcorner {#1} \lrcorner} %% Tuples \DeclarePairedDelimiter\tuple{\langle}{\rangle} -\newcommand\lettm[3]{\mathsf{let}~{#1} \coloneq {#2}~\mathsf{in}~{#3}} %% Naturals -\newcommand\nat{\mathsf{N}} +\newcommand\nat{\ensuremath{\mathsf{N}}} \newcommand\zero{\ensuremath{\mathsf{zero}}} \newcommand\suc{\ensuremath{\mathsf{suc}}} \newcommand\primreckw{\ensuremath{\mathsf{primrec}}} -\NewDocumentCommand\primrec{m m g}{% - \primreckw~{#1}~{#2}\IfValueT{#3}{~{#3}}% - } - -\newcommand\pairingkw{\ensuremath{\mathsf{pair}}} -\NewDocumentCommand\pairing{m m}{% - \pairingkw~{#1}~{#2}% - } +\newcommand\primrec[3]{\primreckw~{#1}~{#2}~{#3}} %% Functors \newcommand\mapkw{\ensuremath{\mathsf{map}}} % e.g. \maptm{X}{1 + X} \newcommand\maptm[2]{\mapkw_{\Lambda {#1}.{#2}}} +%% Arbitrary values +\newcommand\arb{\ensuremath{\mathsf{arb}}} + %% Recursive types +\newcommand\roll{\ensuremath{\mathsf{roll}}} +\newcommand\unroll{\ensuremath{\mathsf{unroll}}} \newcommand\foldkw{\ensuremath{\mathsf{fold}}} \newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}} +\ExplSyntaxOn +\NewDocumentCommand \squid_foldpart:nn {m m m} + { {#2}. \IfBooleanT{#1}{\\ &} {# 3} + } +\NewDocumentCommand \dofold {s m m m} + { \IfBooleanTF{#1} + { \begin{aligned} + \MoveEqLeft + { \foldkw \nobreakspace + {#2} \nobreakspace + \mathsf{with} \nobreakspace + {#3} . + } \\ + & {#4} + \end{aligned} + } + { \foldtm{#2}{#3}{#4} } + } +\ExplSyntaxOff + %% Sums \newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}} -\newcommand\casetm[5]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{{#4}<{#5}}}} +\newcommand\casetm[4]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{#4}}} + +\ExplSyntaxOn +\NewDocumentCommand \squid_matchpart:nn {m m m} + { \IfBooleanT{#1}{\quad} \tuple{#2}. \IfBooleanTF{#1}{&}{\nobreakspace} {#3} + } +\NewDocumentCommand \squid_contmatch:n {m m > {\SplitArgument{1}{.}} m} + { \squid_matchpart:nn {#1} #3 \squid_checkmatch {#1} {#2} {#2} + } +\NewDocumentCommand \squid_checkmatch {m m m g} + { \IfValueTF{#4} + {#2 \squid_contmatch:n {#1} {#3} {#4}} + {\IfBooleanT{#1}{\end{array}}} + } +%% Arguments are kw; multiline; alignment; target +\NewDocumentCommand \squid_startmatch {m m m m} + { \IfBooleanTF{#2} + {\arraycolsep=0.2em + \begin{array}[#3]{ll} + \multicolumn{2}{l}{ + {#1} \nobreakspace + {#4} \nobreakspace + \mathsf{with} + } + \squid_checkmatch {#2} {\\} {\\} + } + { {#1} \nobreakspace + {#4} \nobreakspace + \mathsf{with} \nobreakspace + \squid_checkmatch {#2} {} {;} + } + } +\NewDocumentCommand \domatch {s O{t} m > {\SplitList{;}} m} + { \squid_startmatch {\mathsf{match}} {#1} {#2} {#3} #4 } +\NewDocumentCommand \dofoldmatch {s O{t} m > {\SplitList{;}} m} + { \squid_startmatch {\mathsf{fold}} {#1} {#2} {#3} #4 } +\NewDocumentCommand \doprimrec {s O{t} m m m m} + { \squid_startmatch {\mathsf{primrec}} {#1} {#2} {#3} + {\zero. {#4}} + {\suc \nobreakspace {#5}. {#6}} + } +\ExplSyntaxOff %%% Substitution \ExplSyntaxOn @@ -207,17 +295,14 @@ \NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m} { \squid_subpart:nn #1 \squid_checksub } -\NewDocumentCommand \squid_checksub {O{\parallel}} +\NewDocumentCommand \squid_checksub {O{\parallel} g} { - \peek_meaning_ignore_spaces:NTF \bgroup - {#1 \squid_contsub:n} + \IfValueTF{#2} + {#1 \squid_contsub:n {#2}} {]} } -\NewDocumentCommand \squid_startsub:n {m} - { {#1} [ \squid_checksub [] - } \NewDocumentCommand \sub {m > {\SplitList{,}} m} - { \squid_startsub:n {#1} #2 + { {#1} [ \squid_checksub [] #2 } \ExplSyntaxOff @@ -230,14 +315,7 @@ \fi \begin{abstract} -G\"odel's System T is a simple calculus that performs computation. The absence -of any type abstractions, such as products or sums, along with the limited form -of recursion makes using System T as a target language difficult. In this paper -we introduce \lang{}, a new intermediate language. One can compile \lang{} into -System~T using well-known type encodings, and we have written this algorithm -within \lang{} itself. We also describe a compiler for \lang{} written in Idris -2, featuring an intrinsically well-scoped AST and runtime-erased type-checking -proofs. +\TODO{} \end{abstract} \ifacmart @@ -249,9 +327,9 @@ proofs. \subfile{sec/intro.ltx} \subfile{sec/systemt.ltx} \subfile{sec/lang.ltx} -\subfile{sec/embedding.ltx} -\subfile{sec/reducer.ltx} +\subfile{sec/encoding.ltx} \subfile{sec/compiler.ltx} +\subfile{sec/reducer.ltx} \subfile{sec/related.ltx} \printbibliography{} diff --git a/sec/compiler.ltx b/sec/compiler.ltx index dde2856..2cfde8e 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -6,12 +6,25 @@ \TODO{ \begin{itemize} - \item QTT basics - \item intrinsically well-scoped AST - \item bidirectional judgement - \item well-typed data types - \item type checking function - \item irrelevant pattern matching + \item describe that I have a type checker and compiler implemented in Idris + \item explain what intentionally well-scoped syntax is + \item justify why I used intentionally well-scoped syntax + \item describe how type checking produces a derivation + \item explain the derivation is runtime erased + \item justify the derivation having no runtime cost + \item describe why knowing there is a derivation is necessary + \item explain why these extra features do not guarantee compiler correctness + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item justify how dynamic types make Scheme a good compilation target + \item describe how products are compiled to assoc-lists + \item describe how sums are compiled to tagged values + \item describe how dynamic typing removes the need for roll + \item explain why fold needs to know the term has a valid type + \item explain why fold must be compiled recursively with map \end{itemize} } 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} diff --git a/sec/encoding.ltx b/sec/encoding.ltx new file mode 100644 index 0000000..84ec4a5 --- /dev/null +++ b/sec/encoding.ltx @@ -0,0 +1,132 @@ +\documentclass[../main.tex]{subfiles} + +\begin{document} +\section{Encoding Artist}% +\label{sec:embedding} + +\TODO{ + \begin{itemize} + \item remind the reader why encoding into System~T is useful + \end{itemize} +} + +There are seven phases in the encoding process. In general, each phase removes a +specific type constructor until only naturals and function types remain. +Sometimes removing types requires introducing others; we will introduce lists of +naturals and C-style unions, which we will later need to remove. The full list +of seven phases are: +\begin{enumerate} +\item changing the type of the \roll{} operator so that all recursive arguments + are collected together in a list. +\item using a list-indexed heap encoding to represent inductive types. +\item using an eliminator encoding to represent lists. +\item introducing unions to represent sums as a tagged union. +\item encoding products as an indexed union. +\item exploiting argument form of types to represent unions. +\item removing syntactic sugar we introduced, such as the \arb{} operator that + represents an arbitrary value of a given type. +\end{enumerate} + +We will give two running examples throughout, both with regards to the binary +tree type \(\mu X. (\nat \to \nat) + X \times X\), with leaves labelled by +functions natural to natural. In our first example we construct a balanced +binary tree of depth \(n + 1\), with leaves filled by \systemtinline{f}: +\begin{listing}[H] +\begin{systemt} +let balanced n f = primrec n with + Zero => roll (Leaf f) +| Suc tree => roll (Branch (tree, tree)) +\end{systemt} +\vspace{-\baselineskip} +\end{listing} + +Our other example composes the leaves of the tree into a single function, +starting by applying the right-most leaf to the input value: +\begin{listing}[H] +\begin{systemt} +let compose tree = foldmatch tree with + Leaf f => f +| Branch (f, g) => fun x => f (g x) +\end{systemt} +\end{listing} + +\TODO{ + \begin{itemize} + \item state that the initial type of roll makes it hard to encode + \item explain that there could be an arbitrary number of recursive arguments + scattered in a term + \item describe that collecting them into one location makes future encoding + steps easier + \item justify why I add lists as a built-in type former + \item describe the strength function, the key step in this phase + \item state it is defined by induction on the outer functor + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we encode inductive types as nat-list-indexed heaps + \item describe that storing higher-order data makes G\"odel encodings + impractical + \item describe that the need for local encodings rules out Church encodings + \item describe that the need for fold invalidates using codata encodings + \item explain that using nat-list indices reflects the structure of terms + \item give the encoding of roll + \item give the encoding of fold + \item justify the max operator + \item justify the head operator + \item justify the snoc operator + \item justify the arb operator + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we encode lists using their eliminators + \item explain why a list is a pair of length and index function + \item give the encoding of cons + \item give the encoding of snoc + \item give the encoding of max + \item give the encoding of head + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we encode sums as tagged C-style unions + \item explain the operations and equations of unions + \item justify why sums are tagged unions + \item justify adding union types + \item justify the case operator on naturals + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we encode products as functions from naturals to unions + \item explain that products are heterogenous vectors + \item justify implementing products as homogenous functional vectors + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we encode unions as functions with possibly unused + arguments + \item define the union on types in argument form + \item define the put operator + \item define the get operator + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item state that we desugar other operators last + \item define desugaring of arb + \item define desugaring of case + \item define desugaring of map + \item define desugaring of let + \end{itemize} +} + +\end{document} 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} diff --git a/sec/lang.ltx b/sec/lang.ltx index c7851e2..3b0134a 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -4,223 +4,207 @@ \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} +\TODO{ + \begin{itemize} + \item introduce core language as STLC with regular types + \end{itemize} +} \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} + \[ + \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} -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. +\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}{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} + \[ + \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}{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} -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. +\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\). -\begin{figure} +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*} - \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)} + \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*} -\caption{Definition of \(\mathsf{map}\)}% -\label{fig:lang-map} -\end{figure} +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}} \] -\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} +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*} - (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} + \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}{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*} -\caption{Equational theory for \lang{}}% -\label{fig:lang-eq} +\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}}{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} -\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} +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} diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 8cd19f0..d48e600 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -1,16 +1,39 @@ \documentclass[../main.tex]{subfiles} \begin{document} -\section{Fuelled Self-Reducer for System T}% +\section{Writing ARTiST Programs}% \label{sec:reducer} \TODO{ \begin{itemize} - \item fuelled self-reducer - \item high-level strategy - \item example: case distinction - \item qualitative comparison - \item quantitative comparison (dLoC) + \item state I have written two non-trivial programs in ARTiST + \item briefly describe the fuelled reducer and encoder + \item describe the syntactic sugar I have added + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item describe the operation of the fuelled reducer + \item explain why fuel is necessary for the reducer + \item show some example snippets + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item describe the inputs to the embedding + \item describe the output of the embedding + \item show a ``non-destructive'' fold + \item justify use of destructive folds + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item describe why encoded terms have lots of beta redices + \item describe potential benefit of composing two programs + \item explain the limitiations of the reducer (e.g. eta and bools) \end{itemize} } diff --git a/sec/related.ltx b/sec/related.ltx index caeed41..bd21c96 100644 --- a/sec/related.ltx +++ b/sec/related.ltx @@ -9,4 +9,5 @@ \item Hagino 1987 \end{itemize} } + \end{document} diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 12b1ed2..7881396 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -4,32 +4,23 @@ \section{System T}% \label{sec:systemt} -G\"odel's System~T extends the simply-typed lambda calculus by adding natural -numbers and the primitiver recursor. The type formers are \(\nat\) for natural -numbers and arrows \(A \to B\) for functions. - -\Cref{fig:systemt-type} shows the typing rules for System~T terms. On top of the -usual abstraction and application rules, we can construct unary natural numbers -using the operators \(\zero\) and \(\suc\). Natural numbers are eliminated using -the primitive recursor \primreckw. Given a base case, update function and target -\(n\), the primitive recursor applies the update function to the target \(n\) -times. We will abuse notation and treat the \(\suc\) and \primreckw operators as -functions. +System~T is a simply-typed lambda calculus. The types are naturals \nat{} and +functions \(A \to B\), and on top of function abstraction and application, we +have \zero{} and \suc{} for zero and successor, as well as \primreckw{}, the +primitive recursor. \Cref{fig:syst-typing} shows the typing judgements and +\cref{fig:syst-eq} the equational theory. \begin{figure} \[ \begin{array}{ccc} \begin{prooftree} - \hypo{ - x : A \in \Gamma - \vphantom{\judgement[T]{}{}{}} %% Spooky formatting phantom - } + \hypo{x : A \in \Gamma} \infer1{\judgement[T]{\Gamma}{x}{A}} \end{prooftree} & \begin{prooftree} - \hypo{\judgement[T]{\Gamma, x \colon A}{t}{B}} - \infer1{\judgement[T]{\Gamma}{\lambda x.~t}{A \to B}} + \hypo{\judgement[T]{\Gamma, x : A}{t}{B}} + \infer1{\judgement[T]{\Gamma}{\lambda x. t}{A \to B}} \end{prooftree} & \begin{prooftree} @@ -37,11 +28,9 @@ functions. \hypo{\judgement[T]{\Gamma}{t}{A}} \infer2{\judgement[T]{\Gamma}{f~t}{B}} \end{prooftree} - \\ - \\ + \\\\ \begin{prooftree} - \hypo{\vphantom{\judgement[T]{}{}{}}} %% Spooky formatting phantom - \infer1{\judgement[T]{\Gamma}{\zero}{\nat}} + \infer0{\judgement[T]{\Gamma}{\zero}{\nat}} \end{prooftree} & \begin{prooftree} @@ -50,81 +39,260 @@ functions. \end{prooftree} & \begin{prooftree} - \hypo{\judgement[T]{\Gamma}{z}{A}} - \hypo{\judgement[T]{\Gamma}{s}{A \to A}} \hypo{\judgement[T]{\Gamma}{t}{\nat}} - \infer3{\judgement[T]{\Gamma}{\primrec{z}{s}{t}}{A}} + \hypo{\judgement[T]{\Gamma}{u}{A}} + \hypo{\judgement[T]{\Gamma, x : A}{v}{A}} + \infer3{\judgement[T]{\Gamma}{\primrec{t}{u}{(x.v)}}{A}} \end{prooftree} \end{array} \] - \caption{Typing judgements for System~T}% - \label{fig:systemt-type} + \caption{Typing judgements for System~T}\label{fig:syst-typing} \end{figure} -The equational theory is defined in \cref{fig:systemt-eq}. We have the standard -\(\beta\)-reduction for functions. When we apply the primitve recursor to target -zero, we get the base case. When the recursor is applied to target \(\suc~t\), -we apply the update function to the result of applying \primreckw{} recursively. -An alternative theory would instead apply the update function directly to the -base case instead of to the overall result of the recursion. Whilst this has -little impact for System~T (and operationally corresponds to tail recursion) the -alternative rule does not generalise to the more complex recursive types found -in \lang{}. - \begin{figure} \begin{align*} - (\lambda x.~t)~u &= \sub{t}{x/u} & - \primrec{z}{s}{\zero} &= z & - \primrec{z}{s}{(\suc~t)} &= s~(\primrec{z}{x}{s}{t}) + (\lambda x. t)~u &= \sub{t}{x/u} \\ + \primrec{\zero}{u}{(x.v)} &= u \\ + \primrec{(\suc~t)}{u}{(x.v)} &= \sub{v}{x/\primrec{t}{u}{(x.v)}} \end{align*} - \caption{Equational theory for System~T. \TODO{add eta for unions}}% - \label{fig:systemt-eq} + \caption{Equational theory for System~T}\label{fig:syst-eq} \end{figure} -The primitive recursor is named as such because it generalises the first-order -primitive recursive functions. For example, we can define addition as -\[ -k + n = \primrec{n}{\suc}{k}. -\] -Despite its name, the primitive recursor can compute more than the primitive -recursive functions. By exploiting the higher-order nature of System~T, one can -define the Ackermann-P\'eter function~\cite{semantic-domain} as +Types in System~T are usually presented as binary trees, with branches +representing arrows and leaves being \(\nat\). An alternative presentation is +\emph{argument form}~\cite{DBLP:books/sp/LongleyN15}. Notice that all types can +be written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some unique list of argument +types \(A_i\). We can therefore represent a type by its list of arguments. For +example, the type \(\nat\) has argument form \(\epsilon\), and the type \(\nat \to \nat \to +(\nat \to \nat) \to \nat\) has argument form \([\epsilon, \epsilon, [\epsilon]]\). + +Argument form makes it obvious that all types in System~T are inhabited. For +example, we can use the constantly zero function as an arbitrary inhabitant. + +\subsection{Strategies for Encoding Inductive Types}% +\label{subsec:encoding-strategies} + +Inductive types are a useful programming abstraction that is missing from +System~T. If we are to effectively encode an inductive type, there are three +operations we would like to use: +\begin{enumerate} + \item constructors + \item folding + \item pattern matching +\end{enumerate} +We need constructors else we cannot write values of the inductive type. We need +folding so we can fully consume the inductive type in a total way. We need +pattern matching so we can iterate over multiple values. As a concrete example, +consider the pseudocode in \cref{lst:tree-eq} for comparing whether two binary +trees are equal. We use a fold to create an equality predicate out of +\systemtinline{tree1}. When \systemtinline{tree1} is a leaf, we pattern match on +the other tree to see if it is also a leaf. If \systemtinline{tree1} is instead +a branch, we obtain equality predicates for its two subtrees by its induction +principal. We again pattern match on the other tree to see if it also a branch, +and test equality recursively. + +\begin{listing} + \begin{systemt} + let equal tree1 tree2 = + let go = fold tree1 with + Leaf k => fun t => match t with + Leaf n => k == n + | Branch _ _ => false + | Branch eql eqr => fun t => match t with + Leaf _ => false + | Branch l r => eql l && eqr r + in + go tree2 + \end{systemt} + \caption{Pseudocode for determining equality of two binary trees.}\label{lst:tree-eq} +\end{listing} + +In the remainder of the section we outline four different strategies for +encoding inductive types within System~T. We judge each encoding on whether it +is a local, simply-typed transformation as well as how easy it is to hand write +the three fundamental operators. As you can see from the summary in +\cref{tbl:encodings}, each strategy is lacking in some regard. + +\begin{table} + \caption{Comparison of encoding strategies for inductive types within + System~T. The first column assesses if the strategy is a local, simply-typed + transformation. The remainder indicate whether it is ``easy'' to hand write + the constructors, fold and pattern matching + respectively.}\label{tbl:encodings} + \begin{tabular}{lcccc} + \toprule + Strategy & Local & Constructors & Fold & Pattern Match \\ + \midrule + G\"odel & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\ + Church & \ding{55} & \ding{51} & \ding{51} & \ding{55} \\ + Eliminator & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\ + Heap & \ding{51} & \ding{55} & \ding{51} & \ding{51} \\ + \bottomrule + \end{tabular} +\end{table} + +\subsubsection*{G\"odel Encodings} + +G\"odel encodings represent inductive data types as natural numbers. It is +well-known that there are pairing functions, bijections from \(\mathbb{N} \times +\mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use these +functions to encode inductive data types as pairs of tags and values. Writing +\(\tuple{\cdot, \cdot}\) for the pairing function, we can encode the binary +tree constructors as +\begin{align*} + \mathsf{leaf}(n) &\coloneq \tuple{0, n} \\ + \mathsf{branch}(l, r) &\coloneq \tuple{1, \tuple{l, r}}. +\end{align*} +Pattern matching on G\"odel encodings is achieved by using the unpairing part of +the bijection to determine the specific constructor and its payload. + +One major limitation of G\"odel encodings is that they cannot represent +higher-order data such as functions. The defining trait of G\"odel encodings is +that they represent data by natural numbers, and as function types cannot be +encoded as naturals, we cannot encode functions. We also cannot use a syntactic +representation of functions; \textcite{Squid:unpublished/Bauer17} proves there +is no System~T term that can recover a function from its syntax. + +Another difficulty with G\"odel encodings is implementing the fold operation. +We require our choice of pairing function to be monotonic so that an encoded +value is ``large enough'' to iterate over. The fold with motive type \(A\) then +proceeds with a primitive recursion over the successor of the natural +representing the target with motive type \(\nat \to A\). The intent is that the +\((n+1)\)-th stage of recursion will correctly fold a target with encoding +\(n\). There are no expectations for the base case for the recursion, so we can +use an arbitrary value. For the successor case, we use pattern matching to +deconstruct the input encoded value into its constructor and payload. We can use +the inductive argument to fold over recursive values in the payload, and as the +pairing function is monotonic, these values must be smaller than the current +case, so the resulting value is correct. We then apply the appropriate case for +the fold. Below is the fold over binary trees. \[ -\lambda k, m.~\primrec{\suc}{(\lambda f.~\primrec{(\lambda n.~n)}{(\lambda g, n.~f~(g~n))})}{k}~m. + \dofoldmatch*[t]{t}{ + \mathsf{leaf}(n). f(n); + \mathsf{branch}(x, y). g(x, y) + } \coloneq + \dolet{ + go = \doprimrec*{t}{\arb}{h}{ + \lambda i. \domatch*{i}{ + \mathsf{leaf}(n). f(n); + \mathsf{branch}(l, r). g(h(l), h(r))}} + }*{go~t} \] -Any countable set can be encoded by natural numbers. For inductively defined -sets, such as lists or abstract syntax trees for programs, one can use a G\"odel -encoding to represent values as natural numbers. This depends on a pairing -function \(\pairingkw : \nat \to \nat \to \nat\) that is a (curried) -bijection \(\nat \times \nat \to -\nat\)~\cites{DiscoverEd:book/oc/Cantor52}{szudzik}. As some examples, we can -encode lists of natural numbers as +\subsubsection*{Church Encodings} + +Typically used in untyped settings, Church encodings represent data by their +fold operation. For example binary trees are Church encoded by the type \(\forall A. +(\nat \to A) \to (A \to A \to A) \to A\). The first argument describes how to deconstruct +leaves, and the second applies the inductive step on branches. This encoding +makes implementing fold trivial. Constructors for the inductive types are also +simple to encode, as demonstrated by the following example: +\begin{align*} + \mathsf{leaf}(n) &\coloneq \lambda l, b.~l~n + & + \mathsf{branch}(x, y) &\coloneq \lambda l, b.~b~(x~l~b)~(y~l~b) +\end{align*} + +Whilst Church encodings are great for representing folds and constructors, +pattern matching becomes more challenging. The most general strategy is to use +the fold to recover a sum over the possible constructors, and then eliminate +this using the clauses of the pattern match. For example, we would fold a binary +tree into the sum \(\nat + T \times T\), representing leaves and branches +respectively, and then case split on this sum. We detail this in \cref{fig:church-pm} + +\begin{figure} + \[ + \domatch*[t]{t}{ + \mathsf{leaf}(n). f(n); + \mathsf{branch}(x,y). g(x, y) + } \coloneq + \dolet[t]{ + \roll = \lambda x. \domatch*[t]{x}{ + \mathsf{Left}(n). \mathsf{leaf}(n); + \mathsf{Right}(x, y). \mathsf{branch}(x, y) + } + }{ + x = \dofoldmatch*{t}{ + \mathsf{leaf}(n). \mathsf{Left}(n); + \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y) + } + }*{ + \domatch*{x}{ + \mathsf{Left}(n). f(n); + \mathsf{Right}(x, y). g(x, y) + } + } + \] + \caption{How to perform pattern matching on binary trees for Church encodings. + We assume we have an encoding for sums with pattern matching.}\label{fig:church-pm} +\end{figure} + +You may have noticed that this encoding included a type quantification---in +general, one must use polymorphism to fully represent Church encodings. To avoid +polymorphism requires a global analysis, replacing the polymorphic bound with a +(hopefully) finite product of possible consumers. + +\subsubsection*{Eliminator Encodings} + +This encoding strategy generalises Church encodings. Rather than encoding +inductive types by their folds, eliminator encodings represent inductive types +as a product of all their (contravariant) consumers. For example, if we know the +only operations we will perform on a binary tree are finding the sum of all +leaves and the depth of the tree. We can encode the binary tree as a pair \(\nat +\times \nat\), where the first value is the sum and the second is the depth. + +In this encoding, the constructors eagerly compute the eliminated values. With +our sum and depth example, we encode the constructors by \begin{align*} - \encode{\epsilon} &\coloneq \pairing{0}{0} & - \encode{n, l} &\coloneq \pairing{1}{(\pairing{n}{\encode{l}})} \\ - \shortintertext{and System~T terms (using deBruijn indices) as} - \encode{x_i} &\coloneq \pairing{0}{i} & - \encode{\zero} &\coloneq \pairing{3}{0} \\ - \encode{\lambda~t} &\coloneq \pairing{1}{\encode{t}} & - \encode{\suc~t} &\coloneq \pairing{4}{\encode{t}} \\ - \encode{t~u} &\coloneq \pairing{2}{(\pairing{\encode{t}}{\encode{u}})} & - \encode{\primrec{z}{s}{t}} &\coloneq - \pairing{5}{(\pairing{\encode{z}}{(\pairing{\encode{s}}{\encode{t}})})}. + \mathsf{leaf}(n) &\coloneq \tuple{n, 1} + & + \mathsf{branch}(x, y) &\coloneq \tuple{x.0 + y.0, \suc~(x.1 \sqcup y.1)} \end{align*} -In general, each constructor has a unique tag and this is paired with an -encoding for each subterm. We can analyse an encoded term by reverting the -pairing function and inspecting the tag. For an invalid tag (for our encoding of -lists this is anything greater than 2) we can return an arbitrary value. -Performing recursion on G\"odel encodings is difficult, particularly for values -with more than one recursive argument. - -An alternative encoding strategy uses functions to encode data. One example we -have already given is our encoding of binary trees, from the introduction. -Another functional encoding is to represent lists as functions \(\nat \to -\nat\). Giving the function \zero{} will return the length of the list, and the -values are 1-indexed. This strategy doesn't require a pairing function, but -values no longer have a unique representation. For example, the functions -\(\lambda n.~n + n\) and \(\lambda n. \zero\) both represent the empty list. +using \(k \sqcup n\) to compute the maximum of two naturals. We can easily encode the +specified eliminators too; simply take the corresponding projection from the +product. + +Another benefit of eliminator encodings are that the constructors are +extensible. As no information about exactly which constructor was used remains +in the encoded type, we are free to add some interesting constructors. For +example, we can add the constructor \(\mathsf{double}\) that doubles the value +of each leaf: +\[ +\mathsf{double}(x) \coloneq \tuple{2 \cdot x.0, x.1} +\] + +Eliminator encodings inherit the weaknesses of Church encodings. Defining an +arbitrary fold requires polymorphism. Pattern matching is also impossible in the +general case. With our sum and depth example, we have no way of knowing whether +the value representing a tree came from a leaf or branch as we deliberately +forget this information. + +\subsubsection*{Heap Encodings} + +This encoding strategy is a crude approximation of a heap of memory. Given an +indexing type \(I\), an inductive type is a triple of a \emph{recursive depth}, +a \emph{root index}, and an \(I\)-indexed \emph{heap} of values. Instead of +storing recursive values ``in-line'', one stores an index to its place in the heap. + +Consider the binary tree \(\mathsf{branch}(\mathsf{branch}(\mathsf{leaf}(1), +\mathsf{leaf}(2)), \mathsf{branch}(\mathsf{leaf}(3), +\mathsf{branch}(\mathsf{leaf}(4), \mathsf{leaf}(5))))\), depicted +diagramatically in \cref{fig:box-pointer:tree}. The recursive depth of the tree +is three, as there are at most three nested constructors (e.g.\ the path from +root to the value four). + + +%% This encoding strategy is a crude approximation of a heap of memory. +%% Implementing this strategy requires choosing a (first-order) indexing type. Due +%% to G\"odel encodings, \nat{} is sufficient. In \cref{subsec:encode-inductive} we +%% use lists of naturals to better reflect the tree-like structure of inductive +%% values. + +\TODO{ + \begin{itemize} + \item describe with a box-and-pointer diagram + \item explain briefly how to fold and roll + \end{itemize} +} \end{document} |