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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
|
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Core Language}%
\label{sec:lang}
\TODO{
\begin{itemize}
\item introduce core language as STLC with regular types
\end{itemize}
}
\begin{figure}
\[
\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}
\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}{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}
\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\).
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*}
\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*}
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}} \]
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*}
\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*}
\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}
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}
|
