README.md 11.6 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1
# Functional programming and type systems (2017-2018)
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 9 10 11 12
The lectures take place at University Paris 7 - Denis Diderot,
Bâtiment Sophie Germain, in room 2035.

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

POTTIER Francois's avatar
POTTIER Francois committed
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))
REMY Didier's avatar
REMY Didier committed
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/))
POTTIER Francois's avatar
POTTIER Francois committed
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).)
POTTIER Francois's avatar
POTTIER Francois committed
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
POTTIER Francois's avatar
POTTIER Francois committed
51 52
side effects (references) and the need for the value restriction.

Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
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.
POTTIER Francois's avatar
POTTIER Francois committed
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 70 71 72
## Project

The [programming project](project/) is now available!
The deadline is **Friday, February 16, 2018**.

POTTIER Francois's avatar
POTTIER Francois committed
73 74 75 76
## Approximate syllabus

### Functional Programming: Under the Hood

77 78 79 80
* (22/09/2017)
  Introduction ([slides 00](slides/fpottier-00.pdf)).
  Syntax and operational semantics, on paper and on a machine
  ([slides 01a](slides/fpottier-01a.pdf))
POTTIER Francois's avatar
POTTIER Francois committed
81 82 83
  ([slides 01b](slides/fpottier-01b.pdf)).
  * Newton-Raphson in OCaml ([solution](ocaml/NewtonRaphson.ml)).
  * 1 is not even in Coq ([Even.v](coq/Even.v)).
84
* (29/09/2017)
85
  From a small-step semantics down to an efficient verified interpreter,
POTTIER Francois's avatar
POTTIER Francois committed
86
  in several stages
87 88 89 90
  ([Coq demo](coq/DemoSyntaxReduction.v))
  ([slides 02](slides/fpottier-02.pdf))
  ([OCaml code](ocaml/Lambda.ml))
  ([Coq repo](coq/)).
POTTIER Francois's avatar
POTTIER Francois committed
91 92 93 94
* (06/10/2017) Compiling away first-class functions:
  closure conversion, defunctionalization
  ([slides 03](slides/fpottier-03.pdf))
  ([Coq repo](coq/)).
POTTIER Francois's avatar
README.  
POTTIER Francois committed
95 96 97
* (13/10/2017) Making the stack explicit: the CPS transformation
  ([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)).
POTTIER Francois's avatar
POTTIER Francois committed
104
* (20/10/2017) Equational reasoning and program optimizations
POTTIER Francois's avatar
POTTIER Francois committed
105 106
  ([slides 05](slides/fpottier-05.pdf))
  ([Coq mini-demo](coq/DemoEqReasoning.v)).
POTTIER Francois's avatar
POTTIER Francois committed
107 108 109

### Metatheory of Typed Programming Languages

REMY Didier's avatar
REMY Didier committed
110
* (15/09/2017)
REMY Didier's avatar
REMY Didier committed
111
  [Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
REMY Didier's avatar
handout  
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
* (27/10/2017)
118
  [ADTs, existential types, GADTs](http://gallium.inria.fr/~remy/mpri/slides2.pdf)
REMY Didier's avatar
handout  
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
handout  
REMY Didier committed
125 126 127
* (03/11/2017)
  [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
* (10/11/2017) ~~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)
REMY Didier's avatar
REMY Didier committed
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))
135 136 137 138 139 140 141 142
* (17/11/2017)
  [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)

POTTIER Francois's avatar
POTTIER Francois committed
143

Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
144
### Rich types, tractable typing
POTTIER Francois's avatar
POTTIER Francois committed
145

Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
146 147 148
* (08/12/2017)
  [Introduction](slides/yrg-00-introduction.pdf),
  [ML and Type inference](slides/yrg-01-type-inference.pdf)
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
149 150 151 152
* (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
153 154
  [GADTs](slides/yrg-04-gadt-metatheory.pdf),
  [Exercises](slides/yrg-05-diy-lambda-pi.pdf)
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
155
* Functional correctness
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
156
* Modules
Yann Regis-Gianas's avatar
Yann Regis-Gianas committed
157 158
* Effects and resources

POTTIER Francois's avatar
POTTIER Francois committed
159 160 161

### Dependently-typed Functional Programming

162
* [Guidelines](agda/Index.lagda.rst)
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
163
* [Effectful functional programming](slides/pedagand-01.pdf) ([Source](agda/01-effectful/Monad.lagda.rst)).
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
164
* [Dependent functional programming](slides/pedagand-02.pdf) ([Source](agda/02-dependent/Indexed.lagda.rst), [McCompiler.v](coq/McCompiler.v)).
POTTIER Francois's avatar
POTTIER Francois committed
165 166 167
* Total functional programming.
* Generic functional programming.
* Open problems in dependent functional programming.
POTTIER Francois's avatar
POTTIER Francois committed
168

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

REMY Didier's avatar
12<-1  
REMY Didier committed
171
Two written exams (a partial exam on Friday Dec 1 and a final exam) and one
172
programming project or several programming exercises are used to evaluate
POTTIER Francois's avatar
POTTIER Francois committed
173
the students that follow the full course. Only the partial exam will count
174 175 176
to grade students who split the course.

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

REMY Didier's avatar
REMY Didier committed
178 179
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
180

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

POTTIER Francois's avatar
POTTIER Francois committed
209 210
## Recommended software

211
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
POTTIER Francois's avatar
POTTIER Francois committed
212

213
Then, install OCaml 4.0x and Coq **8.5** via the following commands:
POTTIER Francois's avatar
POTTIER Francois committed
214 215 216 217 218 219
```bash
opam init --comp=4.05 # for instance
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install -j4 -v coq.8.5.3
```
220 221 222 223
(Do *not* install Coq 8.6. The version of AutoSubst that I am using is
not compatible with it. If for some reason you need Coq 8.6, or have
already installed Coq 8.6, note that `opam switch` can be used to let
multiple versions of Coq coexist.)
POTTIER Francois's avatar
POTTIER Francois committed
224

225 226 227 228 229 230 231 232 233
Please also install François Pottier's
[variant](https://github.com/fpottier/autosubst)
of the
[AutoSubst](https://www.ps.uni-saarland.de/autosubst/) library:
```bash
git clone git@github.com:fpottier/autosubst.git
make -C autosubst install
```

234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252
In order to use Coq inside `emacs`,
[ProofGeneral](https://proofgeneral.github.io/)
is highly recommended.
Here is a suggested installation script:
```bash
rm -rf /tmp/PG
cd /tmp
git clone git@github.com:ProofGeneral/PG.git
cd PG
EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs
if [ ! -x $EMACS ]; then
  EMACS=emacs
fi
make EMACS=$EMACS compile
TARGET=/usr/local/share/emacs/site-lisp/ProofGeneral
sudo rm -rf $TARGET
sudo mv /tmp/PG $TARGET
```

253 254 255 256 257 258
Enable ProofGeneral by adding the following line to your `.emacs` file:
```elisp
(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
```
If desired, ProofGeneral can be further
[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
POTTIER Francois's avatar
POTTIER Francois committed
259

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

POTTIER Francois's avatar
POTTIER Francois committed
263 264
## Bibliography

265
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
POTTIER Francois's avatar
POTTIER Francois committed
266
Benjamin C. Pierce, MIT Press, 2002.
REMY Didier's avatar
REMY Didier committed
267 268 269

[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),
Edited by Benjamin C. Pierce, MIT Press, 2005.