summaryrefslogtreecommitdiff
path: root/sec/lang.ltx
blob: e675a853cecc21f991a358e5cbecbaba75b658ef (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
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
211
212
213
214
215
216
217
218
219
\documentclass[../main.tex]{subfiles}

\begin{document}
\section{Core Language}%
\label{sec:lang}

\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}

In this section we introduce \lang{}, a simply-typed lambda calculus
with \emph{regular types}.  \Cref{fig:artist-wf} shows the
well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
that \(A\) is a type using variables from \(\Psi\). 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}.

\begin{proposition}[Type substitution]
  For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and a
  substitution from variables \(X \in \Psi\) to types
  \(\jdgmnt{ty}{\Theta}{f(X)}\), we have
  \(\jdgmnt{ty}{\Theta}{\submult{A}{f}}\).
\end{proposition}

\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}{\tuple{i,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 two
new operators, \roll{} and \foldkw{}, introduce values of an inductive
type \(\mu X. A\). The \roll{} operator takes a vessel of shape \(A\)
filled with inductive components and rolls it into an inductive
value. The \foldkw{} operator takes a target inductive value and a
body, which tranforms the induction hypothesis into a value of the
motive type. By recursively applying the body to the inductive
components of the target, the \foldkw{} computes a result.

For those who are categorically minded, \roll{} is an algebraic map
for a weak initial \(A\)-algebra (viewing \(A\) as an endofunctor) and
\foldkw{} is the weak universal map. The structure is weak-universal
as it is not guaranteed to be unique, only to exist.

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}{\tuple{0,\tuple{}}. l; \tuple{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}\), acting on each component
in the vessel. 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}{\tuple{i,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 operators for constructing
and folding over inductive values, 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}~(\lambda y. \roll~y)~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 we have been unable to encode the \unroll{} operator
such that \(\unroll~(\roll~t) = t\).

\begin{figure}
  \begin{align*}
    (\lambda x. t)~u &\coloneq \sub{t}{x/u}
    &
    \casetm{\tuple{k, t}}{\tuple{i,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
inductive components too.

\end{document}