README.md 12.2 KB
Newer Older
REMY Didier's avatar
REMY Didier committed
1
# Functional programming and type systems (2018-2019)
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

6 7 8 9 10 11 12
## Research internship proposals

The following internship proposals have been posted by the teachers
of this course:

  * [How to be an Effective Liar: Higher-Order Memoization
    Algorithms in Iris](http://gallium.inria.fr/~fpottier/stages/sujet2019-m2.pdf),
13
    by François Pottier, Inria Paris. (**This offer is closed.**)
14 15
  * [Effectful programs and their proofs in a dependently-typed setting](https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/internship-2018-mpri-monad/sep-monad.pdf)
    by Pierre-Évariste Dagand, CNRS -- Inria Paris -- LIP6
Yann REGIS-GIANAS's avatar
Yann REGIS-GIANAS committed
16 17
  * [Différences sémantiques : théorie, techniques et applications](http://yann.regis-gianas.org/public/proposal.pdf)
    by Yann Régis-Gianas, IRIF -- Univ Paris Diderot -- Inria Paris
18 19 20 21 22 23

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.

24
## Location and duration
REMY Didier's avatar
REMY Didier committed
25

26
The lectures take place at University Paris 7 - Denis Diderot,
POTTIER Francois's avatar
POTTIER Francois committed
27
Bâtiment Sophie Germain, in room **1003**.
28 29 30

They are scheduled on Fridays from 12:45 to 15:30.
There is a 15-minute break in the middle of each lecture.
REMY Didier's avatar
REMY Didier committed
31

32
## Teachers
POTTIER Francois's avatar
POTTIER Francois committed
33

POTTIER Francois's avatar
POTTIER Francois committed
34
   * Functional Programming: Under the Hood (12h30, [François Pottier](http://gallium.inria.fr/~fpottier))
35
   * Metatheory of Typed Programming Languages (12h30, [Didier Rémy](http://gallium.inria.fr/~remy/), *head*)
POTTIER Francois's avatar
POTTIER Francois committed
36 37
   * Advanced Aspects of Type Systems (12h30, [Yann Régis Gianas](http://www.pps.jussieu.fr/~yrg/))
   * Dependently-typed Functional Programming (12h30, [Pierre-Evariste Dagand](https://pages.lip6.fr/Pierre-Evariste.Dagand/))
38 39 40 41 42

## Aims

This course presents the principles and formalisms that underlie many of
today's typed functional programming languages.
43
(Here are some [introductory slides](slides/fpottier-00.pdf).)
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66

The course is made up of four parts and can be split after the first two
parts.

In the first part, we discuss the *operational semantics* of functional
programming languages, and we present several classic *program
transformations*, including closure conversion, defunctionalization, and the
transformation into continuation-passing style (CPS). 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 use operational semantics to *prove* that the meaning
of programs is preserved by these transformations. Finally, we suggest how
these definitions and theorems can be expressed in a form that a machine can
check. That is, although Coq is not a prerequisite of the course, we will at
least try to *read and understand Coq definitions and statements*.

In the second part, 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
67 68
reasoning by induction on the structure of types.  Finally, we introduce
subtyping, row polymorphism, and illustrate the problems induced by
69 70
side effects (references) and the need for the value restriction.

71 72 73 74 75 76 77 78 79
The third part of the course introduces "rich" type systems designed
to guarantee extra properties in addition to safety: principality,
information hiding, modularity, extensionality, purity, control of
effects, algorithmic invariants, complexity, resource usage, or full
functional correctness. The expressivity of these systems sometimes
endangers the tractability, or even the feasibility, of type checking
and type inference: a common thread between these lectures discusses
the tradeoffs made on the design of these systems to balance
expressivity and tractability.
80 81 82 83 84 85

The last part focuses on the use of dependent types for programming:
effectful programming with monads and algebraic effects; tagless
interpreters; programming with total functions; generic programming.
We also show the limits of dependently-typed functional programming.

POTTIER Francois's avatar
POTTIER Francois committed
86 87
## Project

88
The programming project is not yet available.
POTTIER Francois's avatar
POTTIER Francois committed
89

90 91 92 93
## Approximate syllabus

### Functional Programming: Under the Hood

REMY Didier's avatar
REMY Didier committed
94
* (14/09/2018)
POTTIER Francois's avatar
POTTIER Francois committed
95 96
  * Introduction
      ([slides 00](slides/fpottier-00.pdf)).
POTTIER Francois's avatar
POTTIER Francois committed
97
  * Syntax and operational semantics, on paper
POTTIER Francois's avatar
POTTIER Francois committed
98
      ([slides 01a](slides/fpottier-01a.pdf)).
POTTIER Francois's avatar
POTTIER Francois committed
99
  * Syntax, on a machine
POTTIER Francois's avatar
POTTIER Francois committed
100
      ([slides 01b](slides/fpottier-01b.pdf)).
REMY Didier's avatar
REMY Didier committed
101
* (21/09/2018)
POTTIER Francois's avatar
POTTIER Francois committed
102 103 104 105 106
  * Operational semantics, on a machine
      ([Coq demo](coq/DemoSyntaxReduction.v)).
  * From a small-step semantics down to an efficient verified interpreter,
    in several stages
      ([slides 02](slides/fpottier-02.pdf))
107
      ([the lambda-calculus in OCaml](ocaml/pottier/Lambda.ml))
POTTIER Francois's avatar
POTTIER Francois committed
108
      ([Coq repo](coq/)).
REMY Didier's avatar
REMY Didier committed
109
* (28/09/2018) Compiling away first-class functions:
110 111 112
  closure conversion, defunctionalization
  ([slides 03](slides/fpottier-03.pdf))
  ([Coq repo](coq/)).
REMY Didier's avatar
REMY Didier committed
113
* (05/10/2018) Making the stack explicit: the CPS transformation
POTTIER Francois's avatar
POTTIER Francois committed
114 115
  ([slides 04](slides/fpottier-04.pdf))
  ([Coq repo](coq/)).
POTTIER Francois's avatar
POTTIER Francois committed
116
  * Transforming a call-by-value interpreter
117
    ([exercise](ocaml/pottier/EvalCBVExercise.ml), [solution](ocaml/pottier/EvalCBVCPS.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
118
  * Transforming a call-by-name interpreter
119
    ([solution](ocaml/pottier/EvalCBNCPS.ml)).
POTTIER Francois's avatar
POTTIER Francois committed
120
  * Transforming a graph traversal
121
    ([solution](ocaml/pottier/Graph.ml)).
REMY Didier's avatar
REMY Didier committed
122
* (12/10/2018) Equational reasoning and program optimizations
123 124
  ([slides 05](slides/fpottier-05.pdf))
  ([Coq mini-demo](coq/DemoEqReasoning.v)).
125 126 127

### Metatheory of Typed Programming Languages

REMY Didier's avatar
REMY Didier committed
128
* (19/10/2018)
REMY Didier's avatar
REMY Didier committed
129
  [Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
REMY Didier's avatar
REMY Didier committed
130
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout1.pdf)
131 132 133
  (see also [intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf),
  and chap [1,2,3](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
  and [4](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
REMY Didier's avatar
REMY Didier committed
134
  of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
REMY Didier's avatar
REMY Didier committed
135
* (26/10/2018)
136
  [ADTs, existential types, GADTs](http://gallium.inria.fr/~remy/mpri/slides2.pdf)
REMY Didier's avatar
REMY Didier committed
137 138 139
  ([handout](http://gallium.inria.fr/~remy/mpri/handout2.pdf)
   [without](http://gallium.inria.fr/~remy/mpri/handout2a.pdf) or
   [only](http://gallium.inria.fr/~remy/mpri/handout2b.pdf)
140 141
   the extra material)
  (se also [chap 6](http://gallium.inria.fr/~remy/mpri/cours4.pdf)
REMY Didier's avatar
REMY Didier committed
142
   of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
REMY Didier's avatar
REMY Didier committed
143
* (02/11/2018)
REMY Didier's avatar
REMY Didier committed
144 145
  [Overloading](http://gallium.inria.fr/~remy/mpri/slides4.pdf)
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout4.pdf)
146
  (see also [chap 7](http://gallium.inria.fr/~remy/mpri/cours5.pdf)
REMY Didier's avatar
REMY Didier committed
147
  of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
148
* (09/11/2018)
149 150 151 152 153
  [References, Value restriction, Side effects](http://gallium.inria.fr/~remy/mpri/slides5.pdf)
  ([handout](http://gallium.inria.fr/~remy/mpri/handout5.pdf))
  (see also sections [3.6, 3.7](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
   and [4.5](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
   of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
154 155 156 157 158
* (16/11/2018)
  [Logical relations](http://gallium.inria.fr/~remy/mpri/slides3.pdf)
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout3.pdf)
  ([chap 8](http://gallium.inria.fr/~remy/mpri/cours6.pdf)
   of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
159 160
* See exercises in [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)

161

162
### Rich types, tractable typing
163

164
* (07/12/2018) ML and type inference ([Introduction](slides/yrg-00-introduction.pdf)), ([ML](slides/yrg-01-type-inference.pdf)), ([programming exercise](ocaml/yrg/ml/README.md))
165 166 167 168
* (14/12/2018) Subtyping
* (21/12/2018) Dependent types
* (11/01/2019) Functional correctness
* (18/01/2019) Effects and resources
169 170 171

### Dependently-typed Functional Programming

172
* [Guidelines](agda/Index.lagda.rst)
173 174 175 176 177
* (25/01/2019) [Effectful functional programming](slides/pedagand-01.pdf) ([Source](agda/01-effectful/Monad.lagda.rst)).
* (01/02/2019) [Dependent functional programming](slides/pedagand-02.pdf) ([Source](agda/02-dependent/Indexed.lagda.rst), [McCompiler.v](coq/McCompiler.v)).
* (08/02/2019) [Total functional programming](slides/pedagand-03.pdf) ([Source](agda/03-total/Recursion.lagda.rst)).
* (15/02/2019) [Generic functional programming](slides/pedagand-04.pdf) ([Source](agda/04-generic/Desc.lagda.rst)).
* (22/02/2019) [Open problems in dependent functional programming](slides/pedagand-05.pdf) ([Source](agda/05-open/Problems.lagda.rst)).
178

REMY Didier's avatar
REMY Didier committed
179 180
## Evaluation of the course

REMY Didier's avatar
REMY Didier committed
181
Two written exams (a partial exam on Friday Nov 30 and a final exam on
REMY Didier's avatar
REMY Didier committed
182 183 184
March 1 or 8) and one programming project or several programming exercises
are used to evaluate the students that follow the full course. Only the
partial exam will count to grade students who split the course.
185 186

Only course notes and hand written notes are allowed for the exams.
REMY Didier's avatar
REMY Didier committed
187

REMY Didier's avatar
REMY Didier committed
188 189
Although the course has changed, you may still have a look at previous exams
available with solutions:
REMY Didier's avatar
REMY Didier committed
190

REMY Didier's avatar
REMY Didier committed
191
- mid-term exam 2017-2018:
192 193
  [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)).
194
- mid-term exam 2016-2017:
195
  [Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf).
196
- mid-term exam 2015-2016:
197 198 199
  [Type containment](http://gallium.inria.fr/~remy/mpri/exams/partiel-2015-2016.pdf).
- final exam 2014-2015:
  [Copatterns](http://gallium.inria.fr/~remy/mpri/exams/final-2014-2015.pdf).
200
- mid-term exam 2014-2015:
201
  [Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf).
202
- final exam 2013-2014:
203
  [Operations on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf).
204
- mid-term exam 2013-2014:
205
  [Typechecking effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf).
206
- final exam 2012-2013:
207
  [Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf).
208
- mid-term exam 2012-2013:
209
  [Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf).
210
- final exam  2011-2012:
211
  [Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf).
212
- mid-term exam  2011-2012:
213
  [Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf).
REMY Didier's avatar
REMY Didier committed
214
- final exam 2010-2011:
215
  [Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf).
REMY Didier's avatar
REMY Didier committed
216
- mid-term exam 2010-2011:
217
  [Compilation of polymorphic records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2010-2011.pdf).
REMY Didier's avatar
REMY Didier committed
218

219 220
## Recommended software

221
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
222 223 224 225 226 227 228 229
If you have installed it already, skip this step.

Then, install OCaml 4.0x, Coq **8.5.3** and AutoSubst by executing
[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:
230
```bash
231 232
  opam switch mpri24
  eval `opam config env`
233
```
234
and return to your usual version of OCaml (say, 4.07.0) with the following commands:
235
```bash
236 237
  opam switch 4.07.0
  eval `opam config env`
238 239
```

240 241 242
In order to use Coq inside `emacs`,
[ProofGeneral](https://proofgeneral.github.io/)
is highly recommended.
243 244
Here is a suggested
[installation script](coq/proofgeneral.sh).
245

246 247
If desired, ProofGeneral can be further
[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
POTTIER Francois's avatar
POTTIER Francois committed
248

249 250 251
To install and familiarize yourself with Agda, please follow the
[instructions](agda/00-agda/Warmup.lagda.rst).

POTTIER Francois's avatar
POTTIER Francois committed
252 253
## Bibliography

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

[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),
258 259 260 261
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.