README.md 24.7 KB
Newer Older
REMY Didier's avatar
REMY Didier committed
1
# Functional programming and type systems (2021-2022)
POTTIER Francois's avatar
POTTIER Francois committed
2

3
4
This page supplements
[the official page of MPRI 2-4](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2).
REMY Didier's avatar
REMY Didier committed
5

REMY Didier's avatar
REMY Didier committed
6
## Location and schedule
REMY Didier's avatar
REMY Didier committed
7

POTTIER Francois's avatar
POTTIER Francois committed
8
The lectures take place at University of Paris,
REMY Didier's avatar
REMY Didier committed
9
Bâtiment Sophie Germain, in room **1002**.
10

POTTIER Francois's avatar
POTTIER Francois committed
11
They are scheduled on **Wednesdays** from 12:45 to 15:30.
12
There is a 15-minute break in the middle of each lecture,
REMY Didier's avatar
REMY Didier committed
13
so each lecture lasts 2h30.
REMY Didier's avatar
REMY Didier committed
14

REMY Didier's avatar
REMY Didier committed
15
16
17
**News**: The [programming project](#project) is expected by Sunday,
February 06. _(A few examples have been [updated](#ppupdated).)_

18

POTTIER Francois's avatar
POTTIER Francois committed
19
## Teachers
POTTIER Francois's avatar
POTTIER Francois committed
20

REMY Didier's avatar
REMY Didier committed
21
* [Metatheory of typed programming languages](#metatheory)
REMY Didier's avatar
REMY Didier committed
22
  ([Didier Rémy](http://cambium.inria.fr/~remy/), *head*)
REMY Didier's avatar
REMY Didier committed
23
* [Interpretation, compilation, and program transformations](#transformation)
POTTIER Francois's avatar
Typos.    
POTTIER Francois committed
24
  ([François Pottier](http://cambium.inria.fr/~fpottier/))
REMY Didier's avatar
REMY Didier committed
25
* [Effects](#effects)
26
  ([Gabriel Scherer](http://www.lix.polytechnique.fr/Labo/Gabriel.Scherer/))
REMY Didier's avatar
REMY Didier committed
27
* [Type-directed programming](#type)
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
28
  ([Pierre-Evariste Dagand](https://www.irif.fr/~dagand/))
REMY Didier's avatar
REMY Didier committed
29
30
* [Rust: programming safely with resources in a modern low-level programming
  language](#rust) ([Jacques-Henri Jourdan](https://jhjourdan.mketjh.fr/)) 
POTTIER Francois's avatar
POTTIER Francois committed
31
32
33
34

## Aims

This course presents the principles and formalisms that underlie many of
REMY Didier's avatar
REMY Didier committed
35
today's typed programming languages.
36
(Here are some [introductory slides](slides/fpottier-00.pdf).)
POTTIER Francois's avatar
POTTIER Francois committed
37

38
This year, the course is reorganized with new material and new teachers.
REMY Didier's avatar
REMY Didier committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
It is composed of five parts and cannot be split.

### Metatheory of Typed Programming Languages

<!-- We focus on the meta-theoretical properties of type systems.  We study
parametric polymorphism (as in System F and ML), data types and type
abstraction. We show syntactic type soundness (via progress and subject
reduction) by reasoning by induction on typing derivations.  We also show
how to obtain semantic properties via logical relations by reasoning by
induction on the structure of types.  Finally, we introduce subtyping, row
polymorphism, and illustrate the problems induced by side effects
(references) and the need for the value restriction.  -->

This part of the course is split in four lectures.  We first introduce the
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
53
_explicitly typed_ version of System F.  We prove its type soundness by
REMY Didier's avatar
REMY Didier committed
54
_subject reduction_ and _progress_.  We discuss _type erasing_ versus _type
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
55
passing_ semantics and derive the _implicitly typed_ version of System
REMY Didier's avatar
REMY Didier committed
56
57
58
59
60
61
62
63
64
F. We present _ML_ as a restriction of _System F_ to prenex polymorphism.
The definition and main properties of System F will also be mechanized in
the Coq proof assistant.

We then extend _System F_ with primitive datatypes, including variants and
records, and show their Church encodings.  We discuss both _iso-recursive_
and _equi-recursive_ types.  We present _existential types_.  _Generalized
Abstract Datatypes (GADTs)_ will just be introduced.

POTTIER Francois's avatar
POTTIER Francois committed
65
We also extend System-F with higher-order kinds and higher-order types,
REMY Didier's avatar
REMY Didier committed
66
which requires computation at the level of types, leading to system _F-omega_.
REMY Didier's avatar
REMY Didier committed
67
68
69
70
71
72
73
74
75
76
77
<!-- We may present _modules_ by elaboration into Fomega. -->

Finally, we introduce logical relations to show parametricity properties of
System F.  Unary relations are used to proof termination as an introduction
to logicial elations.  We cover binary relations in details. They allow to
prove _observational equivalence_ results or study the inhabitants at
certain polymorphic types.  We just introduce _step-indexed_ logical
relations which are needed when the programming language is extended with
constructs that enable unstructured forms of recursion, such as recursive
types at negative occurrences, or references.

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
### Interpretation, Compilation, and Program Transformations

In the first lecture, we discuss several presentations of the *operational
semantics* of a (call-by-value) functional programming language. We explain
why each of these presentations exists and in what sense these presentations
are equivalent. One of these presentations is in fact executable: it is an
interpreter. This interpreter can be implemented in Coq and can be *verified*,
that is, can be proved correct with respect to the other presentations of the
operational semantics. As far as time permits, we will review how lambda-terms
and their operational semantics can be defined in Coq, using a representation
of names as de Bruijn indices. Although Coq is not a prerequisite of the
course, we will at least try to *read and understand Coq definitions and
statements*.

In the next three lectures, we present several classic *program
transformations*, including closure conversion, defunctionalization, the
transformation into continuation-passing style (CPS), and stream fusion. These
program transformations are interesting from two points of view. First, they
are *useful programming techniques*, which can help write or understand
programs. Second, they are used in the *compilation* of functional programming
languages, so they help understand what happens when the machine executes a
program. We discuss how to *prove* that the meaning of programs is preserved
by these transformations, based on an operational semantics. We suggest how
these definitions and theorems can be expressed in a form that a machine can
check (that is, in Coq).

REMY Didier's avatar
REMY Didier committed
104
105
106

### Effects

Gabriel Scherer's avatar
Gabriel Scherer committed
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
In the theory of programming languages, "effects" describe
computational phenomenons that happen "on the side" during the
computation of a program. "While this function runs, it prints
messages / sends emails / displays images / accesses a database / asks
questions to the user, in addition to returning a result." Effects are
of course very important in programs, they are often the main
reason why humans execute programs in the first place!

There is an active research area studying effects: how to model them
mathematically, how to reason about programs containing effects, how
to implement them. Over time researchers realized that we can reuse
the theoretical analysis of effects to provide general mechanisms
letting programmers *implement* effects as libraries, instead of
having only a fixed set of effects supported by the programming
language definition. It is sometimes possible, through careful
refactoring, to take a complex program that computes various things
"directly", turn some of these things into "effects done on the side",
to obtain an equivalent program that looks simpler, is easier to write
and to understand -- with more complex effects on the side.

In this section of the course we will study:

POTTIER Francois's avatar
Typos.    
POTTIER Francois committed
129
- Algebraic structures that capture notions of effects in
Gabriel Scherer's avatar
Gabriel Scherer committed
130
131
132
133
  theory and in practice: monads and applicative functors.

- Effect handlers, a new programming construct that provides another,
  flexible approach to user-defined effects.
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
###  Type-Directed Programming

We revisit the notion of algebraic datatypes through their categorical
semantics as initial algebras (inductive types) and final coalgebras
(coinductive types). We show how recursive program definitions can be
distilled to a handful of recursion/corecursion schemes, thus enabling
general and systematic reasoning about such definitions. We
demonstrate how, in practice, these principles can be used to reason
about pure functional programs as well as derive efficient
implementations from high-level specifications.

We then study type classes, a mechanism that enables the concise
description of programs parameterized over an ad-hoc collection of
types. We provide a formal treatment of ad-hoc polymorphism in a
Haskell-like language. Aside from the foundational aspect, this first
step shall provide some operational intuitions for type classes. We
then explore the benefits of ad-hoc polymorphism from a programming
standpoint. We show how the usual hierarchy of algebraic structures
fits into this framework. We will cover functors (to abstract over
data containers), applicatives and monads (to abstract over effects),
foldable and traversable functors (to abstract over iterators) as well
as Neperian functors and lenses (to abstract over data accessors).

We conclude this journey by entering the realm of type-level
programming, first in a restricted, ML setting and then in a
full-spectrum, dependent type setting. Type-level programming enable
the precise transcription of the invariants of a program into its
type. It is a step toward "correct-by-construction" programming while
allowing the programmer to dispense with dynamic checks (run-time
assertions) in favor of static checks (delegated to the
type-checker). We provide a formal treatment of generalized algebraic
POTTIER Francois's avatar
Typos.    
POTTIER Francois committed
166
data types (GADTs) in an ML-like language. This restricted form of
167
168
169
170
171
172
type-level programming strikes a balance between expressiveness and
decidability. Besides, it is readily available in OCaml, allowing
further experimentation in class. We will develop several examples of
type-level programming, starting with tagless interpreters using GADTs
and gradually moving toward examples involving full-spectrum
dependent-types, as available in Agda or Coq.
POTTIER Francois's avatar
POTTIER Francois committed
173

REMY Didier's avatar
REMY Didier committed
174
175
176

### Rust

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
In this part, we propose to give both a practical and a theoretical
view of the Rust programming language. This new language, developed
during the last decade, aims at modernizing systems programming by
providing a new balance between performance and control on the one
hand, and safety and ease of use on the other hand.

We will first give an overview of the language, from a user's
perspective. Rust got inspiration from many other programming
languages and adapted many well-known mechanisms to its contexts. We
will hence discuss features such as algebraic data types,
polymorphism, type traits (i.e., Rusts' type classes), closures and
subtyping. But Rust also introduced concepts which were only used in
experimental languages, such as ownership and aliasing
control. Finally, we will show how the type system of Rust allows
escaping from the safe fragment and encapsulating these uses of unsafe
features behind safe interfaces. We will study the important example
of interior mutability.

195
Next, we will focus on two recent research subjects on Rust. First, it
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
196
197
198
199
200
201
202
is possible to translate programs written in the safe fragment of Rust
into a functional language, thus completely erasing state. This makes
it possible to ease verification of Rust programs. Second, we will
give an overview of one proof of soundness of the type system of Rust,
which also proves that many libraries written in the unsafe fragment
are, in fact, safe.

REMY Didier's avatar
REMY Didier committed
203

REMY Didier's avatar
REMY Didier committed
204
## <a name="project">Programming Project</a>
POTTIER Francois's avatar
POTTIER Francois committed
205

REMY Didier's avatar
REMY Didier committed
206
Since we are studying programming languages and their formalization,
207
208
209
210
programming is also an important part of the course. We give a mandatory
programming project (around the end of October) which must be completed
roughly by the end of January. The programming project counts for about a
third of the final grade.
REMY Didier's avatar
REMY Didier committed
211

REMY Didier's avatar
REMY Didier committed
212
213
The [programming project](project/2021-2022/) is now available;
read the [assignment](project/2021-2022/sujet.pdf).
214

REMY Didier's avatar
REMY Didier committed
215
The deadline for submitting your project is **Sunday, February 06, 2022**.
216
217
218

Please do not hesitate to ask questions about the project,
of an administrative or technical nature,
REMY Didier's avatar
REMY Didier committed
219
to [Didier Rémy](Didier.Remy@inria.fr).
220

221
Here are some precisions and answers to some of the questions that have been
REMY Didier's avatar
REMY Didier committed
222
223
224
225
226
227
asked:

- <a name="ppupdated">A few modifications have been pushed (more details in
  the assignment and some changes in the output of examples); these are
  minor and should not require any change in your own code. Do `git pull` to
  be sure to be up to date.  (Last modification on `Jan 13`).
REMY Didier's avatar
REMY Didier committed
228

REMY Didier's avatar
REMY Didier committed
229
230
231
232
233
- Can the programming project be done in pairs (en binôme) ?

  No, the programming project and its evaluation are individual.  You may
  discuss it together or help one another if you are stuck, but the code
  should be yours. 
234

235
236
237
238
239
- The behavior of eager mode has been changed (and described accordingly in
  the document) to always force normalization of types of toplevel
  declarations.  This allows for a simpler, more robust specification of the
  expected output of the eager mode.

240
241
242
243
- The behavior of lazy mode has been changed in the case of Pack to return
  the source explicitly given rather than the inferred type, changing the
  output of examples church_bool_T2, chur_sum_T3, and nat_pack_unpack_T3.

244
245
246
247
248
249
250
251
252
253
## Paper discussions (NEW!)

This course will include in-course discussion of research
articles/papers. We will read three papers during the semester. You
will be told about each one several weeks in advance; you have to read
it before the corresponding class, and we will discuss it together
during class. This should give you a glimpse of current topics in the
area, and more generally train you to read research papers and engage
with them.

254
255
256
257
258
259
260
261
262
263
### Some questions of interest

In class we are going to discuss the following questions:
- what are the authors presenting?
- what is the contribution of the paper?
- how did the authors evaluate their work?
- what did you think of the paper (content and presentation)?

### Papers to read:

Gabriel Scherer's avatar
Gabriel Scherer committed
264
- for November 17th, 2021:
265
    “Coordinated Concurrent Programming in Syndicate”, Tony Garnock-Jones and Matthias Felleisen, 2016
266
    TODO:
267
268
269
270

    1. find the paper (mini course on why open access matters)
    2. read the paper
    3. write a short summary (a couple paragraphs) and send it by email to "gabriel.scherer at gmail dot com"
271

Gabriel Scherer's avatar
Gabriel Scherer committed
272
273
- for December 15th, 2021
    "Structuring the Synthesis of Heap-Manipulating Programs", Nadia POlikarpova and Ilya Sergey, 2019
274

275
## Research Internship Proposals
276

277
278
279
We have posted the following internship proposals (possibly more to come):

* [Verifying Tail-Call Optimization Modulo Constructor in Iris](https://cambium.inria.fr/~fpottier/stages/sujet2022-m2.pdf)
280
  (**no longer looking for candidates**, sorry).
281

282
283
284
The internship offers posted by [the Prosecco team](https://team.inria.fr/prosecco/job-offers/)
at Inria Paris are also relevant.

REMY Didier's avatar
REMY Didier committed
285
286
Please do not hesitate to talk to us (during the break or at the end of each
lecture), to contact us by email, or to visit us at our offices.
287

288
289
## Approximate Syllabus

REMY Didier's avatar
REMY Didier committed
290
### <a name="interpretation">Interpretation, Compilation, and Program Transformations (introduction)
REMY Didier's avatar
REMY Didier committed
291

POTTIER Francois's avatar
POTTIER Francois committed
292
* (15/09/2021) Syntax, semantics, and interpreters.
POTTIER Francois's avatar
POTTIER Francois committed
293
294
295
296
297
  * Introduction to this course
      ([slides 00](slides/fpottier-00.pdf)).
  * Operational semantics and reduction strategies
      ([slides 01a](slides/fpottier-01a.pdf)).
  * Towards machine-checked definitions and proofs
POTTIER Francois's avatar
POTTIER Francois committed
298
299
300
301
302
303
      ([slides 01b](slides/fpottier-01b.pdf))
      ([λ-calculus in Coq](coq/DemoSyntaxReduction.v))
      ([λ-calculus in OCaml](ocaml/pottier/Lambda.ml)).
  * From a small-step semantics
    down to an efficient verified interpreter,
    in several stages
POTTIER Francois's avatar
POTTIER Francois committed
304
305
      ([slides 02](slides/fpottier-02.pdf))
      ([Coq repo](coq/)).
REMY Didier's avatar
REMY Didier committed
306

REMY Didier's avatar
REMY Didier committed
307
### <a name="metatheory">Metatheory of Typed Programming Languages
REMY Didier's avatar
REMY Didier committed
308
309

* (22/09/2021)
REMY Didier's avatar
REMY Didier committed
310
311
312
313
314
  [Metatheory of System F](http://cambium.inria.fr/~remy/mpri/slides1.pdf)
  [(handout)](http://cambium.inria.fr/~remy/mpri/handout1.pdf);
  see chap [1,2,3](http://cambium.inria.fr/~remy/mpri/cours1.pdf)
  and [4](http://cambium.inria.fr/~remy/mpri/cours2.pdf)
  of [course notes](http://cambium.inria.fr/~remy/mpri/cours.pdf)).
REMY Didier's avatar
REMY Didier committed
315
  See also _a (slow) walk through the garden of type soundness proofs_
REMY Didier's avatar
REMY Didier committed
316
  in Coq, by François Pottier ([Coq repo](coq/), [html](coq/html/));
REMY Didier's avatar
REMY Didier committed
317
  to view the proofs online, please use the following links:
POTTIER Francois's avatar
POTTIER Francois committed
318
  - Lambda Calculus:
REMY Didier's avatar
REMY Didier committed
319
    [Syntax](http://cambium.inria.fr/~fpottier/mpri/html/LambdaCalculusSyntax.html),
POTTIER Francois's avatar
POTTIER Francois committed
320
    [Values](http://cambium.inria.fr/~fpottier/mpri/html/LambdaCalculusValues.html),
REMY Didier's avatar
REMY Didier committed
321
    [Reduction](http://cambium.inria.fr/~fpottier/mpri/html/LambdaCalculusReduction.html)
REMY Didier's avatar
REMY Didier committed
322
323
324
325
326
327
328
329
330
331
332
  - Simply-typed lambda-calculus:
    [definitions](http://cambium.inria.fr/~fpottier/mpri/html/STLCDefinition.html),
    [lemmas](http://cambium.inria.fr/~fpottier/mpri/html/STLCLemmas.html),
    [type
    soundness](http://cambium.inria.fr/~fpottier/mpri/html/STLCTypeSoundnessComplete.html).
  - The polymorphic lambda-calculus, also known as System F:
    [definitions](http://cambium.inria.fr/~fpottier/mpri/html/SystemFDefinition.html),
    [lemmas](http://cambium.inria.fr/~fpottier/mpri/html/SystemFLemmas.html),
    [type soundness
    ](http://cambium.inria.fr/~fpottier/mpri/html/SystemFTypeSoundnessComplete.html).
* (29/09/2021)
REMY Didier's avatar
REMY Didier committed
333
  [ADTs, existential types, GADTs](http://cambium.inria.fr/~remy/mpri/slides2a.pdf)
REMY Didier's avatar
REMY Didier committed
334
335
336
  ([handout](http://cambium.inria.fr/~remy/mpri/handout2.pdf)
   [without](http://cambium.inria.fr/~remy/mpri/handout2a.pdf) or
   [only](http://cambium.inria.fr/~remy/mpri/handout2b.pdf)
REMY Didier's avatar
REMY Didier committed
337
   the extra material);
REMY Didier's avatar
REMY Didier committed
338
339
  see also [chap 6](http://cambium.inria.fr/~remy/mpri/cours4.pdf)
   of [course notes](http://cambium.inria.fr/~remy/mpri/cours.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
340
* (06/10/21)
REMY Didier's avatar
REMY Didier committed
341
342
  [Higher-Order Types: F-omega](http://cambium.inria.fr/~remy/mpri/slides3.pdf)
  ([handout](http://cambium.inria.fr/~remy/mpri/handout3.pdf).
REMY Didier's avatar
REMY Didier committed
343
* (13/10/2021)
REMY Didier's avatar
REMY Didier committed
344
345
346
347
  [Logical relations](http://cambium.inria.fr/~remy/mpri/slides4.pdf)
  [(handout)](http://cambium.inria.fr/~remy/mpri/handout4.pdf);
  see also [chap 8](http://cambium.inria.fr/~remy/mpri/cours6.pdf)
  of [course notes](http://cambium.inria.fr/~remy/mpri/cours.pdf)).
POTTIER Francois's avatar
POTTIER Francois committed
348

POTTIER Francois's avatar
Tweaks.    
POTTIER Francois committed
349
You may also see [last year's schedule](http://cristal.inria.fr/~remy/mpri/2020/).
350

REMY Didier's avatar
REMY Didier committed
351
### <a name="transformation">Interpretation, Compilation, and Program Transformations ([continued](#interpretation))
352

POTTIER Francois's avatar
POTTIER Francois committed
353
* (20/10/2021) Compiling away first-class functions:
POTTIER Francois's avatar
POTTIER Francois committed
354
355
  closure conversion, defunctionalization
  ([slides 03](slides/fpottier-03.pdf))
356
357
  ([Coq repo](coq/))
  (typed defunctionalization: [exercise](ocaml/pottier/foo.ml), [solution](ocaml/pottier/foo_defunctionalized.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
358
359

* (27/10/2021) Making the stack explicit: the CPS transformation
POTTIER Francois's avatar
README.    
POTTIER Francois committed
360
361
  ([slides 04](slides/fpottier-04.pdf))
  ([Coq repo](coq/)).
POTTIER Francois's avatar
POTTIER Francois committed
362
  * Transforming a call-by-value interpreter
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
363
    ([exercise](ocaml/pottier/EvalCBVExercise.ml), [solution](ocaml/pottier/EvalCBVCPS.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
364
  * Transforming a call-by-name interpreter
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
365
    ([solution](ocaml/pottier/EvalCBNCPS.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
366
  * Transforming a graph traversal
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
367
    ([solution](ocaml/pottier/Graph.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
368

POTTIER Francois's avatar
POTTIER Francois committed
369
370
* (03/11/2021) Some optimisations: constructor specialisation; stream fusion; staging
  ([slides 05](slides/fpottier-05.pdf)).
POTTIER Francois's avatar
README.    
POTTIER Francois committed
371
  * [Staging the power function](metaocaml/pottier/Power.ml).
POTTIER Francois's avatar
README.    
POTTIER Francois committed
372
  * [Staging stream fusion](metaocaml/pottier/StreamFusion.ml).
POTTIER Francois's avatar
POTTIER Francois committed
373
  * Running these examples requires MetaOCaml. Type `opam switch create 4.11.1+BER --no-switch`.
POTTIER Francois's avatar
README.    
POTTIER Francois committed
374
    Then go down into `metaocaml/pottier` and type `make` and `make test`.
POTTIER Francois's avatar
POTTIER Francois committed
375

REMY Didier's avatar
REMY Didier committed
376
### <a name="effects">Effects
377

Gabriel Scherer's avatar
Gabriel Scherer committed
378
379
Slides for the course: [slides.pdf](slides/scherer-2021.pdf).

SCHERER Gabriel's avatar
SCHERER Gabriel committed
380
* (10/11/2021).
381
382
  Primitive effects vs. user-defined effects.
  Direct-style vs. indirect style.
383
  Monads in theory and practice.
Gabriel Scherer's avatar
Gabriel Scherer committed
384
  [live code](ocaml/scherer/cours-2021-00.ml), [exercises](ocaml/scherer/exercises-2021-00.ml)
385
386
* (17/11/2021)
  Paper discussion (1/3): “Coordinated Concurrent Programming in Syndicate”, Tony Garnock-Jones and Matthias Felleisen, 2016
Gabriel Scherer's avatar
Gabriel Scherer committed
387
388
  A continuum of algebraic structures: functors, monads, applicative functors.  
  [applicative-functors.md(slides/scherer-2021-applicative-functors.md)
389
390
391
* (8/12/2021)
  Effect handlers.
  Effects in proofs and logic.
Gabriel Scherer's avatar
Gabriel Scherer committed
392
393
394
395
396
397
398
399
400
401
402

  *Note*: due to the COVID situation, the December 8th lecture will be
  in *hybrid* format, available both on-premises and online (live) at
  the following URL:
  <https://greenlight.virtualdata.cloud.math.cnrs.fr/b/gab-2qz-ph2>

  You are completely free to choose either attendance format; in particular,
  please feel free to stay at home if you are at risk of COVID, or if
  you are in any way stressed by the idea of attending the lecture in
  person.

403
404
405
406
* (15/12/2021)
  Paper discussion (2/3).
  Type systems for effects.

407
408
  *Note*: the course is (of course?) also in hybrid format, same modalities and URL as above.

REMY Didier's avatar
REMY Didier committed
409
### <a name="type">Type-Directed Programming
POTTIER Francois's avatar
POTTIER Francois committed
410

411
412
413
These lectures will involve some hands-on experience and a fair bit of
improvisation. Perhaps not even in that order. To this end, it is
necessary to join the lecture with OCaml installed (say, at least
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
414
415
version 4.11.1).

416
417
Online presence: https://webconf.math.cnrs.fr/b/dag-ddd-p4n

REMY Didier's avatar
REMY Didier committed
418
* (05/01/2022)
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
419
  Overloading ([handout](http://cambium.inria.fr/~remy/mpri/cours5.pdf))
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
420
* (12/01/2022)
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
421
  GADTs & type inference ([handout](http://cambium.inria.fr/~remy/mpri/cours3.pdf))
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
422
* (19/01/2022)
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
423
  Dependent functional programming
424
  ([OCaml warm-up](https://gitlab.com/pedagand/mpri-2.4-nbe-2022),
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
425
426
   [Agda source](agda/02-dependent/Indexed.lagda.rst)
   [Agda online](https://nextjournal.com/pedagand/indexed-functional-programming)).
Pierre-Evariste Dagand's avatar
Pierre-Evariste Dagand committed
427
428
429
430
431
* (26/01/2022)
  Paper discussion (3/3).
  Generic programming
  ([Reading material](https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf),
   [Source](agda/04-generic/Desc.lagda.rst)).
POTTIER Francois's avatar
POTTIER Francois committed
432
433


REMY Didier's avatar
REMY Didier committed
434
### <a name="rust">Rust: programming with resources
REMY Didier's avatar
REMY Didier committed
435

Jacques-Henri Jourdan's avatar
Fix.    
Jacques-Henri Jourdan committed
436
In order to participate to the hands-on exercises of these lectures, the students should install on their computer the following tools:
437
438
439
440
441
442
443
444
445
446
447
448
449
450
* The Rust compiler, version at least 1.41 
* The Cargo package manager, any compatible version
Installing these tools should be easy on any recent Linux distribution using the system's package manager. Alternatively, students can follow the instructions at the following URL: https://rustup.rs/

In order to test the installation, the students are asked to use the Rust compiler on the following program:
```
fn main() {
  let mut f = |x : i32| x;
  let _r : &mut dyn Fn(i32) -> i32 = &mut f;
  println!("{}", f(42))
}
```
If the compiler is correctly installed, then the command `rustc test.rs` should produce an executable.

451
452
Physical presence at the lectures is required, when possible. If the COVID situation makes this impossible, students can follow the course using the following URL: https://webconf.math.cnrs.fr/b/jou-gaq-9gr

453
Lectures:
Jacques-Henri Jourdan's avatar
typo    
Jacques-Henri Jourdan committed
454
* (02/02/2022) Introduction to Rust programming ([slides](slides/jhjourdan-01.pdf)).
455
* (09/02/2022) Introduction to unsafe Rust and interrior mutability ([slides](slides/jhjourdan-02.pdf)), and hands-on session ([exercises](tdtp/jhjourdan1.pdf), [solution](tdtp/jhjourdan1_solution.rs)).
Jacques-Henri Jourdan's avatar
Typo    
Jacques-Henri Jourdan committed
456
* (16/02/2022) Rust and multithreading ([slides](slides/jhjourdan-03.pdf)), and hands-on session ([exercises](tdtp/jhjourdan2.pdf), [template](tdtp/jhjourdan2_template.rs), [solution](tdtp/jhjourdan2_solution.rs)).
457
* (23/02/2022) Formalizing Rust's type system ([slides](slides/jhjourdan-04.pdf)).
REMY Didier's avatar
REMY Didier committed
458

REMY Didier's avatar
REMY Didier committed
459
460
## Evaluation of the course

461
Two written exams and one programming project are used to evaluate the
POTTIER Francois's avatar
POTTIER Francois committed
462
students.
463
By default, the mid-term and final exams will take place on
REMY Didier's avatar
REMY Didier committed
464
**01/12/2021** and **09/03/2022**, respectively.
465
Only course notes and hand-written notes are allowed for the exams.
REMY Didier's avatar
REMY Didier committed
466

REMY Didier's avatar
REMY Didier committed
467
468
Although the course has changed, you may still have a look at previous exams
available with solutions:
REMY Didier's avatar
url    
REMY Didier committed
469

REMY Didier's avatar
REMY Didier committed
470
471
* mid-term exam 2021-2022:
  [Gradual typing](exams/partiel-2021-2022.pdf).
REMY Didier's avatar
REMY Didier committed
472
473
* intermediate exam 2020-2021:
  [Calcul d'objets](exams/intermediaire-2020-2021.pdf).
474
475
* mid-term exam 2020-2021:
  [Delimited control in System F](exams/partiel-2020-2021.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
476
477
* final exam 2019-2020:
  [Gradually-typed functional languages](exams/final-2019-2020.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
478
* mid-term exam 2019-2020:
479
  [A type system for information flow control](exams/partiel-2019-2020.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
480
* final exam 2018-2019:
481
  (not available)
POTTIER Francois's avatar
POTTIER Francois committed
482
* mid-term exam 2018-2019:
483
  [A simple object encoding](exams/partiel-2018-2019.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
484
* final exam 2017-2018:
485
  [Static differentiation](exams/final-2017-2018.pdf).
POTTIER Francois's avatar
POTTIER Francois committed
486
* mid-term exam 2017-2018:
487
488
  [Encoding call-by-name into call-by-value; extensible records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2017-2018.pdf)
  ([Coq solution of part 1](coq/LambdaCalculusEncodingCBNIntoCBV.v)).
REMY Didier's avatar
REMY Didier committed
489

POTTIER Francois's avatar
POTTIER Francois committed
490
491
## Recommended software

492
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
REMY Didier's avatar
REMY Didier committed
493
A recent version is recommended (at the time of writing, 2.0.8).
494
495
If you have installed it already, skip this step.

REMY Didier's avatar
REMY Didier committed
496
Then, install OCaml 4.12.0,
497
[Coq 8.13.2](https://coq.inria.fr),
498
and
499
[AutoSubst](https://github.com/coq-community/autosubst) by executing
500
501
502
503
504
[this script](coq/installation.sh).
This script **does not destroy** your existing installation of
OCaml and Coq. It creates a new "switch" named `mpri24` and installs
appropriate versions of OCaml, Coq, and AutoSubst in it. You can activate
these versions with the following commands:
POTTIER Francois's avatar
POTTIER Francois committed
505

POTTIER Francois's avatar
POTTIER Francois committed
506
```bash
507
  ORIGINAL=$(opam switch show)
508
  opam switch mpri24
POTTIER Francois's avatar
POTTIER Francois committed
509
  eval "$(opam config env)"
POTTIER Francois's avatar
POTTIER Francois committed
510
```
POTTIER Francois's avatar
POTTIER Francois committed
511

512
513
and return to your original working environment with the following
command:
POTTIER Francois's avatar
POTTIER Francois committed
514

515
```bash
516
  opam switch "$ORIGINAL"
POTTIER Francois's avatar
POTTIER Francois committed
517
  eval "$(opam config env)"
518
519
```

520
521
522
In order to use Coq inside `emacs`,
[ProofGeneral](https://proofgeneral.github.io/)
is highly recommended.
523
524
Here is a suggested
[installation script](coq/proofgeneral.sh).
525

526
527
If desired, ProofGeneral can be further
[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
POTTIER Francois's avatar
POTTIER Francois committed
528
529
530

## Bibliography

531
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
POTTIER Francois's avatar
POTTIER Francois committed
532
Benjamin C. Pierce, MIT Press, 2002.
REMY Didier's avatar
REMY Didier committed
533
534

[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),
POTTIER Francois's avatar
POTTIER Francois committed
535
536
537
538
edited by Benjamin C. Pierce, MIT Press, 2005.

[Practical Foundations for Programming Languages, Second Edition](http://www.cs.cmu.edu/~rwh/pfpl.html),
Robert Harper, Cambridge University Press, 2016.