← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to notes/typechecking/algorithm.tex

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
notes/typechecking/algorithm.tex
1
 
\documentclass[a4paper,11pt]{article}
2
 
 
3
 
\usepackage[OT1]{fontenc}
4
 
\usepackage[latin1]{inputenc}
5
 
\usepackage{amsmath,amssymb,amsfonts}
6
 
 
7
 
\usepackage{proof}
8
 
 
9
 
\newcommand\keyword[1]{\mathbf{#1}}
10
 
\newcommand\Coloneqq{\mathrel{::=}}
11
 
\newcommand\OR{~~|~~}
12
 
\newcommand\Hid[1]{\{#1\}}
13
 
\newcommand\lam[1]{\lambda#1.\,}
14
 
\newcommand\hlam[1]{\lam{\Hid{#1}}}
15
 
\newcommand\tlam[2]{\lam{(#1:#2)}}
16
 
\newcommand\thlam[2]{\lam{\Hid{#1:#2}}}
17
 
\newcommand\ePi[3]{(#1:#2)\to#3}
18
 
\newcommand\ehPi[3]{\{#1:#2\}\to#3}
19
 
\newcommand\vPi[2]{\Pi#1:#2.\,}
20
 
\newcommand\vhPi[2]{\Pi\{#1:#2\}.\,}
21
 
\newcommand\vPiTel[1]{\Pi#1.\,}
22
 
\newcommand\vhPiTel[1]{\vPiTel{\{#1\}}}
23
 
\newcommand\Let[2]{\keyword{let}~#1~\keyword{in}~#2}
24
 
\newcommand\Set[1]{\mathsf{Set}_{#1}}
25
 
\newcommand\Prop{\mathsf{Prop}}
26
 
\newcommand\el{\mathsf{El}}
27
 
\newcommand\El[1]{\el_{#1}\,}
28
 
\newcommand\lub{\sqcup}
29
 
 
30
 
\newcommand\APP[2]{\mathsf{app}(#1,#2)}
31
 
\newcommand\HAPP[2]{\mathsf{happ}(#1,#2)}
32
 
\newcommand\Subst[3]{#1[#2/#3]}
33
 
 
34
 
\newcommand\GetSort[1]{\mathsf{sortof}(#1)}
35
 
 
36
 
% Judgement forms
37
 
\renewcommand\Check[5]{#1\,;\,#2\vdash#3\uparrow#4:#5}
38
 
\newcommand\Infer[5]{#1\,;\,#2\vdash#3\downarrow#4:#5}
39
 
\newcommand\IsType[4]{#1\,;\,#2\vdash#3\uparrow#4~\mathbf{type}}
40
 
\newcommand\Equal[5]{#1\,;\,#2\vdash#3=#4:#5}
41
 
\newcommand\TEqual[4]{#1\,;\,#2\vdash#3=#4}
42
 
\newcommand\Expand[6]{#1\,;\,#2\vdash#3:#4\prec#5:#6}
43
 
\newcommand\CheckDecl[4]{#1\,;\,#2\vdash#3\to#4}
44
 
 
45
 
\newcommand\AddGlobalMeta[4]{#1\,;\,#2\vdash{#3}:#4}
46
 
\newcommand\AddLocalMeta[4]{#1\,;\,#2\vdash{#3}:#4}
47
 
 
48
 
\title{Agda II Type Checking Algorithm}
49
 
\author{Ulf Norell}
50
 
 
51
 
\begin{document}
52
 
\maketitle
53
 
 
54
 
\section{Introduction}
55
 
 
56
 
    Write something nice here.
57
 
 
58
 
\section{Syntax}
59
 
 
60
 
\subsection{Expressions}
61
 
 
62
 
    Expressions have been scope checked, but not type checked. Hence the mix
63
 
    between terms, types and sorts.
64
 
 
65
 
    \[\begin{array}{lcl}
66
 
        e & \Coloneqq & x \OR c \OR l \OR ? \OR \_ \\
67
 
          & \OR & \lam xe \OR \hlam xe \OR \tlam xee \OR \thlam xee \\
68
 
          & \OR & e\,e \OR e\,\Hid e \OR \Let{\vec\delta}e \\
69
 
          & \OR & \ePi xee \OR \ehPi xee \OR \Set n \OR \Prop \\
70
 
        l & \Coloneqq & \mathit{integer} \OR \mathit{float} \OR \mathit{string} \OR \mathit{character} \\
71
 
    \end{array}\]
72
 
 
73
 
    Constants ($c$) are names of constructors, defined functions, postulates and datatypes.
74
 
 
75
 
\subsection{Declarations}
76
 
 
77
 
    \[\begin{array}{lcl}
78
 
        \delta & \Coloneqq & \ldots
79
 
    \end{array}\]
80
 
 
81
 
\subsection{Terms}
82
 
 
83
 
    Terms are type checked versions of expressions (that aren't types). The
84
 
    type checking algorithm produces one of these when type checking. The
85
 
    implementation uses deBruijn variables, but to simplify the presentation
86
 
    we don't do that here.
87
 
 
88
 
    \[\begin{array}{lcl}
89
 
        s,t & \Coloneqq & x \OR c \OR l \OR ?_i \\
90
 
            & \OR & \lam xt \OR \hlam xt \OR s\,t \OR s\,\Hid t
91
 
    \end{array}\]
92
 
 
93
 
    Worth noting is that meta variables are now named and that there are no
94
 
    typed lambdas left.
95
 
 
96
 
    Terms are supposed to always be on normal form. We do some work in the
97
 
    rules to ensure that this is the case.
98
 
 
99
 
\subsection{Types and Sorts}
100
 
 
101
 
    After type checking we distinguish between terms, types and sorts.
102
 
 
103
 
    \[\begin{array}{lcl}
104
 
        A,B & \Coloneqq & \El\alpha t \OR \vPi xAB \OR \vhPi xAB \OR \alpha \\
105
 
        \alpha,\beta & \Coloneqq & \Set n \OR \Prop \\
106
 
    \end{array}\]
107
 
 
108
 
    In some presentation of the system design we had type and sort meta
109
 
    variables. I will try to do without them. What this means is that we can't,
110
 
    for instance, infer the type of a domain-free lambda by introducing a meta
111
 
    variable for the domain type.
112
 
 
113
 
    The reason for not having type meta variables is that I'm not sure how they
114
 
    interact with coercions.  Depending on the order you solve constraints you
115
 
    might end up with different instantiations (since different coercions were
116
 
    applied).  It might be that it doesn't matter, but until we're sure I
117
 
    prefer to err on the side of caution.
118
 
 
119
 
    If $x\notin\mathit{FV}(B)$ I will sometimes write $A\to B$ for $\vPi xAB$.
120
 
 
121
 
\section{Judgement forms}
122
 
 
123
 
    In the judgement forms below $\Sigma$ is the signature and contains the
124
 
    type and definition (if any) of the constants currently in scope. $\Gamma$
125
 
    is the context and contains the types of the bound variables.
126
 
 
127
 
    \[\begin{array}{ll}
128
 
        \Check\Sigma\Gamma etA      & \mbox{Type checking, computes $t$.} \\
129
 
        \Infer\Sigma\Gamma etA      & \mbox{Type inference, computes $t$ and $A$.} \\
130
 
        \IsType\Sigma\Gamma eA      & \mbox{Checking that $e$ is a type, computes $A$.} \\
131
 
        \Equal\Sigma\Gamma stA      & \mbox{Typed conversion.} \\
132
 
%       \TEqual\Sigma\Gamma AB      & \mbox{Type conversion.} \\
133
 
        \Expand\Sigma\Gamma sAtB    & \mbox{Coercing conversion, computes $t$.} \\
134
 
        \CheckDecl\Sigma\Gamma\delta{\Sigma'} & \mbox{Checking declarations, computes $\Sigma'$.}
135
 
    \end{array}\]
136
 
 
137
 
    The only non-standard judgement is the coercing conversion which replaces
138
 
    the convertibility judgement for types. The purpose of this judgement form
139
 
    is to insert things that have been hidden. For instance, suppose that
140
 
    $f:\vhPi A{\Set0}\vPi xAA$ in $\Sigma$ and we want to check
141
 
    $\Check\Sigma\Gamma ft{\vPi xBB}$. This should succeed with $t =
142
 
    f\,\Hid{B}$. The reason it does succeed is because we can coerce $f$ to
143
 
    have the desired type:
144
 
    \[
145
 
        \Expand\Sigma\Gamma f{\vhPi A{\Set0}\vPi xAA}{f\,\Hid{B}}{\vPi xBB}
146
 
    \]
147
 
 
148
 
\section{Judgements}
149
 
 
150
 
\subsection{Checking}
151
 
 
152
 
    Type checking is used only as a last resort. If we can infer the type,
153
 
    that's what we do.
154
 
 
155
 
    \[\begin{array}{c}
156
 
        \infer{ \Check\Sigma\Gamma etB }
157
 
        { \Infer\Sigma\Gamma esA
158
 
        & \Expand\Sigma\Gamma sAtB
159
 
        }
160
 
    \end{array}\]
161
 
 
162
 
    The coercing conversion inserts any hidden lambdas or applications that are
163
 
    missing from $s$.
164
 
 
165
 
    We can't infer the type of domain free lambdas.
166
 
 
167
 
    \[\begin{array}{c}
168
 
        \infer{ \Check\Sigma\Gamma{\lam xe}{\lam xt}{\vPi xAB} }
169
 
              { \Check\Sigma{\Gamma,x:A}etB }
170
 
        \\{}\\
171
 
        \infer{ \Check\Sigma\Gamma{\hlam xe}{\hlam xt}{\vhPi xAB} }
172
 
              { \Check\Sigma{\Gamma,x:A}etB }
173
 
    \end{array}\]
174
 
 
175
 
    If we're checking a non-hidden lambda against a hidden function type we
176
 
    should insert the appropriate number of hidden lambdas. There is some
177
 
    abuse of notation to make the rule more readable: If $\Delta =
178
 
    (x_1:A_1)\ldots(x_n:A_n)$, then $\hlam\Delta t$ means $\hlam{x_1}\ldots\hlam{x_n}t$ and
179
 
    $\vhPiTel\Delta B$ means $\vhPi{x_1}{A_1}\ldots\vhPi{x_n}{A_n}B$.
180
 
 
181
 
    \[\begin{array}{c}
182
 
        \infer{ \Check\Sigma\Gamma{\lam xe}{\hlam\Delta\lam xt}{\vhPiTel\Delta\vPi xAB} }
183
 
        { \Check\Sigma{\Gamma,\Delta,x:A} etB
184
 
        }
185
 
    \end{array}\]
186
 
 
187
 
    The type of meta variables can't be inferred either.
188
 
 
189
 
    \[\begin{array}{ccc}
190
 
        \infer[\AddGlobalMeta\Sigma\Gamma{?_i}A]{\Check\Sigma\Gamma{{?}}{{?_i}}A}{}
191
 
            &&
192
 
        \infer[\AddLocalMeta\Sigma\Gamma{?_i}A]{\Check\Sigma\Gamma\_{{?_i}}A}{}
193
 
    \end{array}\]
194
 
 
195
 
    Let bindings can be inferred only if the body can be inferred, so we need a
196
 
    checking rule in case it can't.
197
 
 
198
 
    \[\begin{array}{c}
199
 
        \infer{ \Check\Sigma\Gamma{\Let\delta e}tA }
200
 
        { \CheckDecl\Sigma\Gamma\delta{\Sigma'}
201
 
        & \Check{\Sigma'}\Gamma etA
202
 
        }
203
 
    \end{array}\]
204
 
 
205
 
    An alternative approach would be to infer the type of everything, inserting
206
 
    meta variables when we don't know.  This would require type and sort meta
207
 
    variables, though.
208
 
 
209
 
\subsection{Inference}
210
 
 
211
 
    Inferring the type of a variable or a constant amounts to looking it up in
212
 
    the context or signature. This will never fail, since the expressions have
213
 
    been scope checked prior to type checking.
214
 
 
215
 
    \[\begin{array}{ccc}
216
 
        \infer{\Infer\Sigma\Gamma xx{\Gamma(x)}}{} &&
217
 
        \infer{\Infer\Sigma\Gamma cc{\Sigma(x)}}{}
218
 
    \end{array}\]
219
 
 
220
 
    Literals have predefined types.
221
 
    \[\begin{array}{c}
222
 
        \infer{\Infer\Sigma\Gamma ll{\mathsf{typeof}(l)}}{}
223
 
    \end{array}\]
224
 
 
225
 
    There are three rules for application. The first two are for the easy cases
226
 
    where all implicit arguments have been made explicit.
227
 
    \[\begin{array}{c}
228
 
        \infer{ \Infer\Sigma\Gamma{e_1\,e_2}{\APP st}{\Subst Btx} }
229
 
        { \Infer\Sigma\Gamma{e_1}s{\vPi xAB}
230
 
        & \Check\Sigma\Gamma{e_2}tA
231
 
        }
232
 
        \\{}\\
233
 
        \infer{ \Infer\Sigma\Gamma{e_1\,\Hid{e_2}}{\HAPP st}{\Subst Btx} }
234
 
        { \Infer\Sigma\Gamma{e_1}s{\vhPi xAB}
235
 
        & \Check\Sigma\Gamma{e_2}tA
236
 
        }
237
 
    \end{array}\]
238
 
    The functions $\APP --$ and $\HAPP --$ perform $\beta$-reductions and
239
 
    definition unfolding if necessary, to make sure that terms are on normal
240
 
    form. The third rule handles the case when you apply a function expecting
241
 
    hidden arguments to a non-hidden argument, in which case we have to fill in
242
 
    the hidden arguments with meta variables.
243
 
    \[\begin{array}{c}
244
 
        \infer[\AddLocalMeta\Sigma\Gamma{\vec ?}\Delta]
245
 
        { \Infer\Sigma\Gamma{e_1\,e_2}{\APP{\HAPP{s}{\vec{?}}}t}{B[\vec{?}/\Delta,t/x]} }
246
 
        { \Infer\Sigma\Gamma{e_1}s{\vhPiTel\Delta\vPi xAB}
247
 
        & \Check\Sigma\Gamma{e_2}t{\Subst A{\vec ?}\Delta}
248
 
        }
249
 
    \end{array}\]
250
 
    A consequence of these rules is that when you give a hidden argument
251
 
    explicitly it is always interpreted as the left-most hidden argument, so
252
 
    $f\,\Hid{x}\,y$ is the same as $f\,\Hid{x}\,\Hid{\_}\,y$ for an $f$ of the
253
 
    appropriate type.
254
 
 
255
 
    The inference rule for let is the same as the checking rule.
256
 
    \[\begin{array}{c}
257
 
        \infer{ \Infer\Sigma\Gamma{\Let\delta e}tA }
258
 
        { \CheckDecl\Sigma\Gamma\delta{\Sigma'}
259
 
        & \Infer{\Sigma'}\Gamma etA
260
 
        }
261
 
    \end{array}\]
262
 
 
263
 
\subsection{Computing sorts}
264
 
 
265
 
    Types contain enough information to retrieve the sort.
266
 
 
267
 
    \[\begin{array}{lcl}
268
 
        \GetSort{\El\alpha t} & = & \alpha \\
269
 
        \GetSort{\vPi xAB} & = & \GetSort A\lub\GetSort B \\
270
 
        \GetSort{\vhPi xAB} & = & \GetSort A\lub\GetSort B \\
271
 
        \GetSort{\Set n} & = & \Set{n+1} \\
272
 
        \GetSort{\Prop} & = & \Set1 \\
273
 
        {}\\
274
 
        \Set n\lub\Set m & = & \Set{\mathsf{max}(n,m)} \\
275
 
        \Prop\lub\Prop & = & \Prop \\
276
 
        \Prop\lub\Set n & = & \Set1\lub\Set n \\
277
 
        \Set n\lub\Prop & = & \Set n\lub\Set 1 \\
278
 
    \end{array}\]
279
 
 
280
 
    In PTS terms we have the rule $(\alpha,\beta,\alpha\lub\beta)$.
281
 
    We might want to consider having $(\Set0,\Prop,\Prop)$ as well.
282
 
 
283
 
\subsection{Is type}
284
 
 
285
 
    The {\em is type} judgement checks that an expression is a valid type and
286
 
    returns that type.  It could also compute its sort but since we can easily get the
287
 
    sort of a type, it isn't necessary.
288
 
 
289
 
    \[\begin{array}{c}
290
 
        \infer
291
 
        { \IsType\Sigma\Gamma e{\El\alpha t} }
292
 
        { \Infer\Sigma\Gamma et\alpha }
293
 
    \end{array}\]
294
 
    
295
 
    \[\begin{array}{c}
296
 
        \infer
297
 
        { \IsType\Sigma\Gamma{\ePi x{e_1}{e_2}}{\vPi xAB} }
298
 
        { \IsType\Sigma\Gamma{e_1}A
299
 
        & \IsType\Sigma{\Gamma,x:A}{e_2}B
300
 
        } \\{}\\
301
 
        \infer
302
 
        { \IsType\Sigma\Gamma{\ehPi x{e_1}{e_2}}{\vhPi xAB} }
303
 
        { \IsType\Sigma\Gamma{e_1}A
304
 
        & \IsType\Sigma{\Gamma,x:A}{e_2}B
305
 
        }
306
 
    \end{array}\]
307
 
 
308
 
    \[\begin{array}{c}
309
 
        \infer
310
 
        { \IsType\Sigma\Gamma\alpha{\GetSort\alpha} }
311
 
        {}
312
 
    \end{array}\]
313
 
 
314
 
\subsection{Coercing conversion}
315
 
 
316
 
    The coercing conversion $\Expand\Sigma\Gamma sAtB$ computes a $t$ of type
317
 
    $B$ given an $s$ of type $A$, by adding hidden applications or lambdas to
318
 
    $s$ until the types $A$ and $B$ match.
319
 
 
320
 
%     In the following two rules $C$ should not be a hidden function space
321
 
%     ($\vhPi xAB$).
322
 
    \[\begin{array}{c}
323
 
        \infer[\AddLocalMeta\Sigma\Gamma{?_i}A]
324
 
        { \Expand\Sigma\Gamma s{\vhPi xAB}tC }
325
 
        { \Expand\Sigma\Gamma{\HAPP s{?_i}}{\Subst B{?_i}x}tC }
326
 
        \\{}\\
327
 
        \infer
328
 
        { \Expand\Sigma\Gamma sC{\hlam xt}{\vhPi xAB} }
329
 
        { \Expand\Sigma{\Gamma,x:A}sCtB }
330
 
    \end{array}\]
331
 
    The first rule applies when $C$ is not a hidden function space, and the
332
 
    second rule is applicable for any $C$. This has the effect of
333
 
    $\eta$-expanding functions with hidden arguments. This allows, for
334
 
    instance, $s:\vhPiTel{A,B:\Set0}A\to B\to A$ to be coerced to $\hlam
335
 
    As\,\Hid A\,\Hid A : \vhPi A{\Set0}A\to A\to A$.
336
 
 
337
 
    If both types are normal function spaces we $\eta$-expand.
338
 
    \[\begin{array}{c}
339
 
        \infer
340
 
        { \Expand\Sigma\Gamma s{\vPi xAB}{\lam ys'}{\vPi y{A'}B'} }
341
 
        { \Expand\Sigma{\Gamma,y:A'}y{A'}tA
342
 
        & \Expand\Sigma{\Gamma,y:A'}{s\,t}{\Subst Btx}{s'}{B'}
343
 
        }
344
 
    \end{array}\]
345
 
    This allows us to perform coercions in higher order functions. For instance, 
346
 
    \[
347
 
        \Expand\Sigma\Gamma f{(B\to B)\to C}
348
 
            {\lam xf\,(x\,\Hid{B})}
349
 
            {(\vhPi A{\Set0}A\to A)\to C}
350
 
    \]
351
 
    The last two cases are when the types are $\el$s or sorts. In neither case
352
 
    are there any coercions.
353
 
    \[\begin{array}{ccc}
354
 
        \infer
355
 
        { \Expand\Sigma\Gamma t\alpha t\alpha }
356
 
        {}
357
 
        &&
358
 
        \infer
359
 
        { \Expand\Sigma\Gamma s{\El\alpha t_1}s{\El\alpha t_2} }
360
 
        { \Equal\Sigma\Gamma{t_1}{t_2}\alpha }
361
 
    \end{array}\]
362
 
 
363
 
\subsection{Conversion}
364
 
 
365
 
    The conversion checking is type directed. This gives us $\eta$-equality for
366
 
    functions in a nice way. It also makes it possible to introduce proof
367
 
    irrelevance with a rule like this:
368
 
    \[\left(\begin{array}{c}
369
 
        \infer
370
 
        { \Equal\Sigma\Gamma pqP }
371
 
        { \GetSort{P} = \Prop }
372
 
    \end{array}\right)\]
373
 
    We don't do that at this point though, but only make use of the types in the
374
 
    function case:
375
 
    \[\begin{array}{c}
376
 
        \infer
377
 
        { \Equal\Sigma\Gamma st{\vPi xAB} }
378
 
        { \Equal\Sigma{\Gamma,x:A}{\APP sx}{\APP tx}B
379
 
        }
380
 
        \\{}\\
381
 
        \infer
382
 
        { \Equal\Sigma\Gamma st{\vhPi xAB} }
383
 
        { \Equal\Sigma{\Gamma,x:A}{\HAPP sx}{\HAPP tx}B
384
 
        }
385
 
    \end{array}\]
386
 
 
387
 
    There are a number of notation abuses in the following two rules. Firstly,
388
 
    $\Equal\Sigma\Gamma{\vec s}{\vec t}\Delta$ denotes the extension of the
389
 
    conversion judgement to sequences of terms. I am also a bit sloppy with the
390
 
    hiding: in $\vPiTel\Delta A$, $\Delta$ can contain both hidden and non-hidden
391
 
    things. Consequently when I say $x\,\vec s$ it includes hidden applications.
392
 
    \[\begin{array}{c}
393
 
        \infer
394
 
        { \Equal\Sigma\Gamma{x\,\vec s}{x\,\vec t}A }
395
 
        { x:\vPiTel\Delta A'\in\Gamma
396
 
        & \Equal\Sigma\Gamma{\vec s}{\vec t}\Delta
397
 
        }
398
 
        \\{}\\
399
 
        \infer
400
 
        { \Equal\Sigma\Gamma{c\,\vec s}{c\,\vec t}A }
401
 
        { c:\vPiTel\Delta A'\in\Sigma
402
 
        & \Equal\Sigma\Gamma{\vec s}{\vec t}\Delta
403
 
        }
404
 
    \end{array}\]
405
 
    
406
 
 
407
 
\subsection{Declarations}
408
 
 
409
 
\end{document}