← Back to branch summary

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

« back to all changes in this revision

Viewing changes to notes/talks/video060510/talk.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/talks/video060510/talk.tex
1
 
\documentclass{beamer}
2
 
 
3
 
\usetheme{JuanLesPins}
4
 
%\usetheme{Darmstadt}
5
 
 
6
 
\usepackage{beamerthemesplit}
7
 
\usepackage{pxfonts}
8
 
\usepackage{proof}
9
 
%\usepackage{fleqn}
10
 
 
11
 
\title{Agda II -- Take One}
12
 
\author{Ulf Norell}
13
 
\date{\today}
14
 
 
15
 
\newcommand\PI[2]{(#1:#2)\to{}}
16
 
\newcommand\hPI[2]{\{#1:#2\}\to{}}
17
 
\newcommand\Fun[2]{#1\to#2}
18
 
\newcommand\lam[1]{\lambda #1\to{}}
19
 
\newcommand\Cons{\mathrel{::}}
20
 
 
21
 
\newcommand\To{\Rightarrow}
22
 
\newcommand\GoFig{\_}
23
 
 
24
 
\newcommand\Data[3]{\ensuremath{
25
 
    \mathbf{data}~#1 : #2~\mathbf{where} \\
26
 
    \quad\begin{array}{lcl}
27
 
        #3
28
 
    \end{array}
29
 
}}
30
 
\newcommand\Module[2]{\ensuremath{
31
 
    \mathbf{module}~#1~\mathbf{where} \\
32
 
    \quad\begin{array}{l}
33
 
        #2
34
 
    \end{array}
35
 
}}
36
 
 
37
 
\newenvironment{code}{
38
 
\begin{block}{}\(\begin{array}{l}
39
 
}{
40
 
\end{array}\)\end{block}
41
 
}
42
 
 
43
 
\renewcommand\Bar{~~|~~}
44
 
 
45
 
\begin{document}
46
 
 
47
 
\frame{\titlepage}
48
 
 
49
 
\section{Introduction}
50
 
\frame{\tableofcontents}
51
 
 
52
 
\subsection{Motivation}
53
 
\frame{
54
 
    \frametitle{What's the point?}
55
 
 
56
 
    \begin{itemize}
57
 
        \item of Agda II
58
 
        \begin{itemize}
59
 
            \item Solid theoretical foundation (lacking in Agda)
60
 
            \begin{itemize}
61
 
            \item Small well-defined core language with nice metatheory.
62
 
            \item Transparent translation from the full language to the core language.
63
 
            \end{itemize}
64
 
        \end{itemize}
65
 
        \item of this talk
66
 
        \begin{itemize}
67
 
            \item Present the (full) language from a user's perspective.
68
 
        \end{itemize}
69
 
    \end{itemize}
70
 
}
71
 
 
72
 
\subsection{The Basics}
73
 
\frame{
74
 
    \frametitle{The Logical Framework}
75
 
 
76
 
    {\small \begin{block}{The Basic Language}\(\begin{array}{llcl}
77
 
        \mbox{(Terms)} & s, t & \Coloneqq & x \Bar c \Bar f \Bar s\,t \Bar \lam xt \Bar \lam{(x:A)}t \\
78
 
        \mbox{(Types)} & A, B & \Coloneqq & \PI xAB \Bar A\to B \Bar t \Bar \alpha \\
79
 
        \mbox{(Sorts)} & \alpha, \beta & \Coloneqq & Set_i \Bar Set \Bar Prop \\
80
 
        \end{array}\)
81
 
    \end{block}}
82
 
 
83
 
    \begin{itemize}
84
 
        \item Note: $Set \neq Prop$.
85
 
    \end{itemize}
86
 
 
87
 
    {\small\begin{block}{Example: polymorphic identity}\(\begin{array}{l}
88
 
        id : \PI A{Set} A\to A \\
89
 
        id = \lam{(A:{Set})(x:A)}x
90
 
    \end{array}\)\end{block} }
91
 
}
92
 
 
93
 
\subsection{Features and Not}
94
 
 
95
 
\frame{
96
 
    \frametitle{What's there and what's not}
97
 
 
98
 
    \begin{itemize}
99
 
        \item Features
100
 
        \begin{itemize}
101
 
            \item Inductive datatypes
102
 
            \item Functions by pattern matching
103
 
            \item Implicit arguments
104
 
            \item Module system
105
 
        \end{itemize}
106
 
    ~
107
 
        \item Not Yet Features
108
 
        \begin{itemize}
109
 
            \item $\Pi$ in Set
110
 
            \item Signatures and structures
111
 
            \item Inductive families
112
 
        \end{itemize}
113
 
    \end{itemize}
114
 
}
115
 
 
116
 
\section{Not Yet Features}
117
 
 
118
 
\subsection{Pi in Set}
119
 
 
120
 
\frame{
121
 
    \frametitle{$\Pi$ in Set}
122
 
 
123
 
    \begin{itemize}
124
 
        \item What does it mean?
125
 
        \begin{block}{We don't have}\[
126
 
            \infer{\Gamma\vdash\PI xAB:{Set}}
127
 
                { \Gamma\vdash A:{Set}
128
 
                & \Gamma,x:A\vdash B:{Set}
129
 
                }
130
 
        \]\end{block}
131
 
 
132
 
        \item Consequences:
133
 
            {\small \begin{block}{We can't do}\(\begin{array}{l}
134
 
                    Rel~A = A\to A\to{Prop} \\
135
 
                    apply : List~(Nat\to Nat)\to List~Nat\to List~Nat \\
136
 
            \end{array}\)\end{block} }
137
 
    \end{itemize}
138
 
}
139
 
 
140
 
\frame{
141
 
    \frametitle{$\Pi$ in Set}
142
 
    \begin{itemize}
143
 
        \item Why don't we have it?
144
 
            \begin{itemize}
145
 
                \item Ask Thierry... (The metatheory gets tricky when you combine
146
 
                      $\eta$-equality and $\Pi$ in ${Set}$.)
147
 
            \end{itemize}
148
 
        ~
149
 
        \item What to do about it:
150
 
        \begin{itemize}
151
 
            \item Get the metatheory straightened out (e.g. $\eta$-equality for datatypes).
152
 
            \item Abandon $\eta$-equality.
153
 
            \item Abandon $\Pi$ in ${Set}$.
154
 
        \end{itemize}
155
 
    \end{itemize}
156
 
}
157
 
 
158
 
\subsection{Signatures and Structures}
159
 
 
160
 
\frame{
161
 
    \frametitle{Signatures and Structures}
162
 
 
163
 
    \begin{itemize}
164
 
        \item What does it mean?
165
 
        \begin{itemize}
166
 
            \item In Agda you can say (something like)
167
 
                {\small \begin{code}
168
 
                    Pair~A~B = \mathbf{sig}\begin{array}[t]{lcl}
169
 
                            fst & : & A \\
170
 
                            snd & : & B \\
171
 
                        \end{array} \\
172
 
                    p : Pair~Nat~Nat \\
173
 
                    p = \mathbf{struct}\begin{array}[t]{lcl}
174
 
                            fst & = & 3 \\
175
 
                            snd & = & 7 \\
176
 
                        \end{array} \\
177
 
                    three = p.fst
178
 
                \end{code} }
179
 
        \end{itemize}
180
 
        \item Why don't we have it?
181
 
        \begin{itemize}
182
 
            \item We want to start simple.
183
 
            \item Signatures and structures will appear in Agda II -- Take Two
184
 
            (but probably not in the same form as in Agda).
185
 
        \end{itemize}
186
 
    \end{itemize}
187
 
}
188
 
 
189
 
\subsection{Inductive Families}
190
 
 
191
 
\frame{
192
 
    \frametitle{Inductive Families}
193
 
 
194
 
    \begin{itemize}
195
 
        \item What does it mean?
196
 
        \begin{itemize}
197
 
            \item For instance:
198
 
            \begin{code}
199
 
                \Data{Vec~(A:{Set})}{Nat\to{Set}}{
200
 
                    vnil  & : & Vec~A~zero \\
201
 
                    vcons & : & \PI n{Nat}A\to Vec~A~n\to Vec~A~(suc~n) \\
202
 
                }
203
 
            \end{code}
204
 
        \end{itemize}
205
 
        \item Why don't we have it?
206
 
        \begin{itemize}
207
 
            \item The inductive families in Agda are very limited in terms of
208
 
                  what you can do with them.
209
 
            \item We want something better, which will require some thinking.
210
 
        \end{itemize}
211
 
    \end{itemize}
212
 
}
213
 
 
214
 
\section{Features}
215
 
 
216
 
\subsection{Datatypes}
217
 
 
218
 
\frame{
219
 
    \frametitle{Datatypes}
220
 
 
221
 
    \begin{itemize}
222
 
        \item Standard, garden-variety, strictly positive datatypes:
223
 
        {\small \begin{code}
224
 
            \Data{Nat}{Set}{
225
 
                zero & : & Nat \\
226
 
                suc & : & Nat\to Nat \\
227
 
            } \\{}\\
228
 
            \Data{Exist~(A:{Set})~(P:A\to{Prop})}{Prop}{
229
 
                witness & : & \PI xA P~x\to Exist~A~P
230
 
            } \\{}\\
231
 
            \Data{Acc~(A:{Set})~((<):A\to A\to{Prop})~(x:A)}{Prop}{
232
 
                acc & : & (\PI yA y<x\to Acc~A~(<)~y)\to Acc~A~(<)~x
233
 
            }
234
 
        \end{code} }
235
 
        \item Note that $\mathbf{data}\ldots$ is a declaration (not a term or type).
236
 
    \end{itemize}
237
 
}
238
 
 
239
 
\subsection{Definitions by Pattern Matching}
240
 
 
241
 
\frame{
242
 
    \frametitle{Definitions by Pattern Matching}
243
 
 
244
 
    \begin{itemize}
245
 
        \item Functions are defined by pattern matching
246
 
        \begin{itemize}
247
 
            \item Arbitrarily nested, exhaustive, possibly overlapping patterns.
248
 
            \item No case expressions!
249
 
            {\small \begin{code}
250
 
                \begin{array}{lclcl}
251
 
                \multicolumn5l{(+) : Nat\to Nat\to Nat} \\
252
 
                zero &+& m &=& m \\
253
 
                suc~n &+& m &=& suc~(n + m) \\
254
 
                \end{array}\\
255
 
                {}\\
256
 
                \begin{array}{lllcl}
257
 
                eqNat : &Nat\to&Nat\to&&Bool \\
258
 
                eqNat&zero&zero &=& true \\
259
 
                eqNat&(suc~n)&(suc~m) &=& eqNat~n~m \\
260
 
                eqNat&\_&\_ &=& false \\
261
 
                \end{array}
262
 
            \end{code} }
263
 
        \end{itemize}
264
 
    \end{itemize}
265
 
}
266
 
 
267
 
\frame{
268
 
    \frametitle{Mutual induction-recursion}
269
 
 
270
 
    \begin{itemize}
271
 
        \item You can have mutually inductive-recursive definitions:
272
 
        {\small \begin{code}
273
 
            \mathbf{mutual} \\
274
 
            \quad\begin{array}{llcl}
275
 
                even : &Nat\to&&Bool \\
276
 
                even&zero &=& true \\
277
 
                even&(suc~n) &=& odd~n \\
278
 
                \\
279
 
                odd : &Nat\to&&Bool \\
280
 
                odd&zero &=& false \\
281
 
                odd&(suc~n) &=& even~n \\
282
 
            \end{array}
283
 
        \end{code} }
284
 
        \item I'd show the standard universe construction example of
285
 
              induction-recursion, but you need $\Pi$ in ${Set}$ for that.
286
 
    \end{itemize}
287
 
 
288
 
}
289
 
 
290
 
\frame{
291
 
    \frametitle{Local functions}
292
 
 
293
 
    \begin{itemize}
294
 
        \item Functions (and datatypes) can be local to a definition:
295
 
        {\small \begin{code}
296
 
            reverse : (A:{Set})\to List~A\to List~A \\
297
 
            reverse~A~xs = rev~xs~nil \\
298
 
            \quad\mathbf{where} \\
299
 
            \qquad\begin{array}[t]{lllcl}
300
 
                    rev : &List~A\to&List~A\to&&List~A \\
301
 
                    rev&nil&ys & = & ys \\
302
 
                    rev&(x\Cons xs)&ys & = & rev~xs~(x\Cons ys) \\
303
 
                \end{array}
304
 
        \end{code} }
305
 
    \end{itemize}
306
 
}
307
 
 
308
 
\frame{
309
 
    \frametitle{Termination}
310
 
 
311
 
    \begin{itemize}
312
 
        \item We allow general recursion.
313
 
        \item Termination checking is done separately (as in Agda).
314
 
        \item Example:
315
 
        {\small \begin{code}\begin{array}{llcl}
316
 
            qsort : &List~Nat\to&&List~Nat \\
317
 
            qsort &nil &=& nil \\
318
 
            qsort &(x\Cons xs) &=& filter~(\lam yy<x)~xs\mathrel{++} \\
319
 
            &&& x\Cons filter~(\lam yy\geq x)~xs
320
 
        \end{array}\end{code} }
321
 
    \end{itemize}
322
 
}
323
 
 
324
 
\subsection{Implicit Arguments}
325
 
 
326
 
\frame{
327
 
    \frametitle{Meta Variables}
328
 
 
329
 
    \begin{itemize}
330
 
        \item There are two kinds of meta variables (only one in Agda):
331
 
        \begin{itemize}
332
 
            \item Interaction points: $?$ and $\{!~\ldots~!\}$
333
 
            \item Go figure\footnote{Conorism}: $\GoFig$
334
 
        \end{itemize}
335
 
        \item The type checker should be able to figure out the value of a go
336
 
              figure without user intervention...
337
 
        \item ...whereas the value of an interaction point is supplied by the user.
338
 
        \item We use go figures to implement implicit arguments.
339
 
    \end{itemize}
340
 
 
341
 
}
342
 
 
343
 
\frame{
344
 
    \frametitle{Implicit Arguments}
345
 
    \begin{itemize}
346
 
        \item Curly braces $\{~\}$ are used to indicate implicitness:
347
 
        {\small \begin{block}{Syntax}\(\begin{array}{lcl}
348
 
            s,t & \Coloneqq & \ldots \Bar s~\{t\} \Bar \lam{\{x\}}t \Bar \lam{\{x:A\}}t \Bar \GoFig \\
349
 
            A,B & \Coloneqq & \ldots \Bar \hPI xAB \Bar \{A\}\to B \\
350
 
        \end{array}\)\end{block} }
351
 
        {\small \begin{code}
352
 
            id~:~\hPI A{Set} A\to A \\
353
 
            id~\{A\}~x = x \\
354
 
            zero' = id~\{Nat\}~zero \\
355
 
        \end{code} }
356
 
        \item Implicit arguments can be omitted: $id~x$ means $id~\{\GoFig\}~x$.
357
 
        \item Both in left-hand-sides and right-hand-sides:
358
 
        {\small \begin{code}
359
 
            id~:~\hPI A{Set} A\to A \\
360
 
            id~x = x \\
361
 
        \end{code} }
362
 
    \end{itemize}
363
 
}
364
 
 
365
 
\frame{
366
 
    \frametitle{Example}
367
 
 
368
 
    \begin{code}
369
 
        \begin{array}{l}
370
 
            \Data{List~(A:{Set})}{Set}{
371
 
                nil & : & List~A \\
372
 
                (\Cons) & : & A\to List~A\to List~A \\
373
 
            }
374
 
        \end{array} \\{}\\
375
 
        \begin{array}{lclcl}
376
 
        \multicolumn5l{(++) : \hPI A{Set} List~A\to List~A\to List~A} \\
377
 
        nil & ++ & ys &=& ys \\
378
 
        (x::xs) & ++ & ys &=& x::(xs \mathrel{++} ys) \\
379
 
        \end{array}
380
 
    \end{code}
381
 
    \begin{itemize}
382
 
        \item Note that constructors are polymorphic:
383
 
        \begin{itemize}
384
 
            \item $\vdash nil : List~A$, for any $A$
385
 
            \item $\not\vdash nil : \hPI A{Set}List~A$.
386
 
        \end{itemize}
387
 
    \end{itemize}
388
 
}
389
 
 
390
 
\subsection{Module System}
391
 
 
392
 
\frame{
393
 
    \frametitle{Module System}
394
 
 
395
 
    \begin{itemize}
396
 
        \item Purpose:
397
 
        \begin{itemize}
398
 
            \item Control the scope of names.
399
 
            \item (Not to model algebraic structures.)
400
 
        \end{itemize}
401
 
        \item Guiding principle:
402
 
        \begin{itemize}
403
 
            \item Scope checking should not require type
404
 
              checking or computation.
405
 
        \end{itemize}
406
 
        \item Consequence:
407
 
        \begin{itemize}
408
 
            \item Modules are not first class.
409
 
        \end{itemize}
410
 
    \end{itemize}
411
 
}
412
 
 
413
 
\frame{
414
 
    \frametitle{Submodules}
415
 
 
416
 
    \begin{itemize}
417
 
        \item Each source file contains a single module, which in turn can
418
 
        contain any number of submodules:
419
 
        {\small \begin{code}
420
 
            \Module{Prelude}{
421
 
                \Module{Nat}{\ldots} \\
422
 
                \Module{List}{
423
 
                    \ldots \\
424
 
                    \Module{Fold}{\ldots} \\
425
 
                    \ldots \\
426
 
                } \\
427
 
            }
428
 
        \end{code} }
429
 
    \end{itemize}
430
 
}
431
 
 
432
 
\frame{
433
 
    \frametitle{Accessing the Module Contents}
434
 
 
435
 
    \begin{itemize}
436
 
        \item To use a module from a file the module has to be {\em imported}\\
437
 
        \begin{code}
438
 
            \mathbf{import}~Prelude
439
 
        \end{code}
440
 
        \item We can then use the names in the module fully qualified
441
 
        \begin{code}
442
 
            one = Prelude.Nat.suc~Prelude.Nat.zero
443
 
        \end{code}
444
 
        \item Or we can {\em open} a module
445
 
        \begin{code}
446
 
            \mathbf{open}~Prelude.Nat \\
447
 
            one = suc~zero
448
 
        \end{code}
449
 
    \end{itemize}
450
 
}
451
 
 
452
 
\frame{
453
 
    \frametitle{Controlling what is imported}
454
 
    \begin{itemize}
455
 
        \item We can exercise finer control over what is imported or opened.
456
 
        \begin{code}
457
 
            \mathbf{import}~Prelude~as~P \\
458
 
            \mathbf{open}~P.Nat,~hiding~(+),~renaming~(zero~to~z) \\
459
 
            \mathbf{open}~P.List,~using~(replicate) \\
460
 
            zz : P.List.List~Nat \\
461
 
            zz = replicate~(suc~(suc~z))~z
462
 
        \end{code}
463
 
    \end{itemize}
464
 
}
465
 
 
466
 
\frame{
467
 
    \frametitle{Controlling what is exported}
468
 
    \begin{itemize}
469
 
        \item Private things are not exported.
470
 
        {\small \begin{code}
471
 
            \Module{BigProof}{
472
 
                \mathbf{private}~minorLemma = \ldots \\
473
 
                mainTheorem : P == NP \\
474
 
                mainTheorem = \ldots minorLemma \ldots
475
 
            }
476
 
        \end{code} }
477
 
        \item Abstract things export only their type.
478
 
        {\small \begin{code}
479
 
            \Module{Stack}{
480
 
                \mathbf{abstract} \\
481
 
                \quad\begin{array}{l}
482
 
                    Stack : Set\to Set \\
483
 
                    Stack = List \\
484
 
                \end{array} \\
485
 
            }
486
 
        \end{code} }
487
 
        \item Private things still reduce, abstract things don't.
488
 
    \end{itemize}
489
 
}
490
 
 
491
 
\frame{
492
 
    \frametitle{Parameterised Modules}
493
 
 
494
 
    \begin{itemize}
495
 
        \item Modules can be parameterised.
496
 
        {\small \begin{code}
497
 
            \mathbf{module}~Monad\begin{array}[t]{l}
498
 
                    (M:Set\to Set) \\
499
 
                    (return:\hPI{A}{Set}A\to M~A) \\
500
 
                    ((>>=):\hPI{A,B}{Set}M~A\to(A\to M~B)\to M~B)
501
 
                \end{array} \\
502
 
                ~~~\mathbf{where} \\
503
 
                \quad\begin{array}{l}
504
 
                    liftM : \hPI{A,B}{Set}(A\to B)\to M~A\to M~B \\
505
 
                    liftM~f~m = m \mathrel{>>=} \lam x return~(f~x)
506
 
                \end{array}
507
 
        \end{code}}
508
 
        \item And instantiated
509
 
        {\small \begin{code}
510
 
            \mathbf{module}~MonadList = Monad~List~singleton~(flip~concatMap) \\
511
 
            lemma : \begin{array}[t]{l}
512
 
                    \hPI{A,B}{Set}\PI{f}{A\to B}\PI{xs}{List~A} \\
513
 
                    map~f~xs == MonadList.liftM~f~xs \\
514
 
                \end{array}
515
 
        \end{code} }
516
 
        \item You need to instantiate a parameterised module to use it.
517
 
    \end{itemize}
518
 
}
519
 
 
520
 
\section{Conclusions}
521
 
 
522
 
\frame{
523
 
    \frametitle{That's it folks}
524
 
 
525
 
    \begin{itemize}
526
 
        \item Agda II is very much work in progress.
527
 
        \item At this point very little is set in stone, so if you think things
528
 
              should be a different way now is the time to speak up.
529
 
        \item Most of what you've seen will be available for use during the 4th
530
 
              Agda Implementors Meeting starting next week in Japan.
531
 
    \end{itemize}
532
 
}
533
 
% \section{Examples}
534
 
% 
535
 
% \frame{
536
 
% }
537
 
 
538
 
\end{document}
539