diff options
Diffstat (limited to 'sec/systemt.ltx')
| -rw-r--r-- | sec/systemt.ltx | 330 |
1 files changed, 249 insertions, 81 deletions
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} |