README.md 11.6 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
## Location and duration
REMY Didier's avatar
REMY Didier committed
7

8
The lectures take place at University Paris 7 - Denis Diderot,
POTTIER Francois's avatar
POTTIER Francois committed
9
Bâtiment Sophie Germain, in room **1003**.
10 11 12

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
13

14
## Teachers
POTTIER Francois's avatar
POTTIER Francois committed
15

POTTIER Francois's avatar
POTTIER Francois committed
16
   * Functional Programming: Under the Hood (12h30, [François Pottier](http://gallium.inria.fr/~fpottier))
17
   * Metatheory of Typed Programming Languages (12h30, [Didier Rémy](http://gallium.inria.fr/~remy/), *head*)
POTTIER Francois's avatar
POTTIER Francois committed
18 19
   * 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/))
20 21 22 23 24

## Aims

This course presents the principles and formalisms that underlie many of
today's typed functional programming languages.
25
(Here are some [introductory slides](slides/fpottier-00.pdf).)
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48

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
49 50
reasoning by induction on the structure of types.  Finally, we introduce
subtyping, row polymorphism, and illustrate the problems induced by
51 52
side effects (references) and the need for the value restriction.

53 54 55 56 57 58 59 60 61
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.
62 63 64 65 66 67

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
68 69
## Project

70
The programming project is not yet available.
POTTIER Francois's avatar
POTTIER Francois committed
71

72 73 74 75
## Approximate syllabus

### Functional Programming: Under the Hood

REMY Didier's avatar
REMY Didier committed
76
* (14/09/2018)
POTTIER Francois's avatar
POTTIER Francois committed
77 78
  * Introduction
      ([slides 00](slides/fpottier-00.pdf)).
POTTIER Francois's avatar
POTTIER Francois committed
79
  * Syntax and operational semantics, on paper
POTTIER Francois's avatar
POTTIER Francois committed
80
      ([slides 01a](slides/fpottier-01a.pdf)).
POTTIER Francois's avatar
POTTIER Francois committed
81
  * Syntax, on a machine
POTTIER Francois's avatar
POTTIER Francois committed
82
      ([slides 01b](slides/fpottier-01b.pdf)).
REMY Didier's avatar
REMY Didier committed
83
* (21/09/2018)
POTTIER Francois's avatar
POTTIER Francois committed
84 85 86 87 88 89 90
  * 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))
      ([the lambda-calculus in OCaml](ocaml/Lambda.ml))
      ([Coq repo](coq/)).
REMY Didier's avatar
REMY Didier committed
91
* (28/09/2018) Compiling away first-class functions:
92 93 94
  closure conversion, defunctionalization
  ([slides 03](slides/fpottier-03.pdf))
  ([Coq repo](coq/)).
REMY Didier's avatar
REMY Didier committed
95
* (05/10/2018) Making the stack explicit: the CPS transformation
POTTIER Francois's avatar
POTTIER Francois committed
96 97
  ([slides 04](slides/fpottier-04.pdf))
  ([Coq repo](coq/)).
POTTIER Francois's avatar
POTTIER Francois committed
98 99 100 101 102 103
  * Transforming a call-by-value interpreter
    ([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)).
  * Transforming a call-by-name interpreter
    ([solution](ocaml/EvalCBNCPS.ml)).
  * Transforming a graph traversal
    ([solution](ocaml/Graph.ml)).
REMY Didier's avatar
REMY Didier committed
104
* (12/10/2018) Equational reasoning and program optimizations
105 106
  ([slides 05](slides/fpottier-05.pdf))
  ([Coq mini-demo](coq/DemoEqReasoning.v)).
107 108 109

### Metatheory of Typed Programming Languages

REMY Didier's avatar
REMY Didier committed
110
* (19/10/2018)
REMY Didier's avatar
REMY Didier committed
111
  [Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
REMY Didier's avatar
REMY Didier committed
112
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout1.pdf)
113 114 115
  (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
116
  of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
REMY Didier's avatar
REMY Didier committed
117
* (26/10/2018)
118
  [ADTs, existential types, GADTs](http://gallium.inria.fr/~remy/mpri/slides2.pdf)
REMY Didier's avatar
REMY Didier committed
119 120 121
  ([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)
122 123
   the extra material)
  (se also [chap 6](http://gallium.inria.fr/~remy/mpri/cours4.pdf)
REMY Didier's avatar
REMY Didier committed
124
   of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
REMY Didier's avatar
REMY Didier committed
125
* (02/11/2018)
REMY Didier's avatar
REMY Didier committed
126 127
  [Logical relations](http://gallium.inria.fr/~remy/mpri/slides3.pdf)
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout3.pdf)
REMY Didier's avatar
REMY Didier committed
128
  ([chap 8](http://gallium.inria.fr/~remy/mpri/cours6.pdf)
REMY Didier's avatar
REMY Didier committed
129
   of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
REMY Didier's avatar
REMY Didier committed
130
* (09/11/2018) ~~Subtyping. Rows.~~
REMY Didier's avatar
REMY Didier committed
131 132
  [Overloading](http://gallium.inria.fr/~remy/mpri/slides4.pdf)
  [(handout)](http://gallium.inria.fr/~remy/mpri/handout4.pdf)
133
  (see also [chap 7](http://gallium.inria.fr/~remy/mpri/cours5.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
* (16/11/2018)
136 137 138 139 140 141 142
  [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))
* See exercises in [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)

143

144
### Rich types, tractable typing
145

REMY Didier's avatar
REMY Didier committed
146 147 148
(07/12/2018) (14/12/2018) (21/12/2018) (11/01/2019) (18/01/2019)

* [Introduction](slides/yrg-00-introduction.pdf),
Yann REGIS-GIANAS's avatar
Yann REGIS-GIANAS committed
149
  [ML and Type inference](slides/yrg-01-type-inference.pdf)
Yann REGIS-GIANAS's avatar
Yann REGIS-GIANAS committed
150 151 152 153
* (15/12/2017) Subtyping
  [Exercises](slides/yrg-02-diy-lambda-calculus-with-subtyping.pdf)
  [Answers](slides/yrg-03-diy-lambda-calculus-with-subtyping-answers.pdf)
* (22/12/2017 - 12/01/2018) Dependent types
Yann REGIS-GIANAS's avatar
Yann REGIS-GIANAS committed
154 155
  [GADTs](slides/yrg-04-gadt-metatheory.pdf),
  [Exercises](slides/yrg-05-diy-lambda-pi.pdf)
Yann REGIS-GIANAS's avatar
Yann REGIS-GIANAS committed
156
* (19/01/2018) [Functional correctness](slides/yrg-06-functional-correctness.pdf)
157
* Effects and resources
158 159 160

### Dependently-typed Functional Programming

REMY Didier's avatar
REMY Didier committed
161 162
(25/01/2019) (/01/02/2019) (08/02/2019) (15/02/2019) (22/02/2019)

163
* [Guidelines](agda/Index.lagda.rst)
164
* [Effectful functional programming](slides/pedagand-01.pdf) ([Source](agda/01-effectful/Monad.lagda.rst)).
165
* [Dependent functional programming](slides/pedagand-02.pdf) ([Source](agda/02-dependent/Indexed.lagda.rst), [McCompiler.v](coq/McCompiler.v)).
166
* [Total functional programming](slides/pedagand-03.pdf) ([Source](agda/03-total/Recursion.lagda.rst)).
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
167
* [Generic functional programming](slides/pedagand-04.pdf) ([Source](agda/04-generic/Desc.lagda.rst)).
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
168
* [Open problems in dependent functional programming](slides/pedagand-05.pdf) ([Source](agda/05-open/Problems.lagda.rst)).
169

REMY Didier's avatar
REMY Didier committed
170 171
## Evaluation of the course

REMY Didier's avatar
REMY Didier committed
172 173 174 175
Two written exams (a partial exam on Friday Nov 23 or 30 and a final exam on
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.
176 177

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

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

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

210 211
## Recommended software

212
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
213 214 215 216 217 218 219 220
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:
221
```bash
222 223
  opam switch mpri24
  eval `opam config env`
224
```
225
and return to your usual version of OCaml (say, 4.07.0) with the following commands:
226
```bash
227 228
  opam switch 4.07.0
  eval `opam config env`
229 230
```

231 232 233
In order to use Coq inside `emacs`,
[ProofGeneral](https://proofgeneral.github.io/)
is highly recommended.
234 235
Here is a suggested
[installation script](coq/proofgeneral.sh).
236

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

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

POTTIER Francois's avatar
POTTIER Francois committed
243 244
## Bibliography

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

[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),
249 250 251 252
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.