blob: 84ec4a5775a35e99faf9fa8d66ab8c0cbd70f007 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
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}
|
