README.md 9.39 KB
Newer Older
1
# Functional programming and type systems (2017-2018)
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 committed
5

6
## Location and duration
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 committed
13

14
## Teachers
POTTIER Francois committed
15

POTTIER Francois committed
16
   * Functional Programming: Under the Hood (12h30, [François Pottier](http://gallium.inria.fr/~fpottier))
REMY Didier committed
17
   * [Metatheory of Typed Programming Languages](http://gallium.inria.fr/~remy/mpri/) (12h30, [Didier Rémy](http://gallium.inria.fr/~remy/), *head*)
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 53 54 55 56 57 58 59 60 61 62 63 64 65 66
side effects (references) and the need for the value restriction.

The third part of the course describes more advanced features of type
systems: exceptions and effect handlers, including their typechecking and
static analyses: type inference, data flow and control flow analyses.
Finally, it introduces dependent types and refinement types.

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.

## Approximate syllabus

### Functional Programming: Under the Hood

67 68 69 70
* (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 committed
71 72 73
  ([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)).
74
* (29/09/2017)
75
  From a small-step semantics down to an efficient verified interpreter,
POTTIER Francois committed
76
  in several stages
77 78 79 80
  ([Coq demo](coq/DemoSyntaxReduction.v))
  ([slides 02](slides/fpottier-02.pdf))
  ([OCaml code](ocaml/Lambda.ml))
  ([Coq repo](coq/)).
81 82 83 84
* (06/10/2017) Compiling away first-class functions:
  closure conversion, defunctionalization
  ([slides 03](slides/fpottier-03.pdf))
  ([Coq repo](coq/)).
POTTIER Francois committed
85 86 87
* (13/10/2017) Making the stack explicit: the CPS transformation
  ([slides 04](slides/fpottier-04.pdf))
  ([Coq repo](coq/)).
POTTIER Francois committed
88 89 90 91 92 93
  * 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)).
94
* (20/10/2017) Equational reasoning and program optimizations
95 96
  ([slides 05](slides/fpottier-05.pdf))
  ([Coq mini-demo](coq/DemoEqReasoning.v)).
97 98 99

### Metatheory of Typed Programming Languages

REMY Didier committed
100
* (15/09/2017)
REMY Didier committed
101
  [Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
102 103 104 105
  (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)
  of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)).
REMY Didier committed
106
* (27/10/2017)
107 108 109 110 111 112
  [ADTs, existential types, GADTs](http://gallium.inria.fr/~remy/mpri/slides2.pdf)
  ([without](http://gallium.inria.fr/~remy/mpri/slides2a.pdf) or
   [only](http://gallium.inria.fr/~remy/mpri/slides2b.pdf)
   the extra material; 
  and [chap 6](http://gallium.inria.fr/~remy/mpri/cours4.pdf)).
  of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
POTTIER Francois committed
113
* (03/11/2017) Logical relations.
114
* (10/11/2017) Subtyping. Rows.
REMY Didier committed
115
* (17/11/2017) References, Value restriction, Side effects.
116 117 118

### Advanced Aspects of Type Systems

POTTIER Francois committed
119 120 121 122 123
* Exceptions and effect handlers. (Compiled away via CPS.)
* Typechecking exceptions and handlers.
* Type inference. (ML. Bidirectional. Elaboration.)
* Data/control flow analysis.
* Functional correctness. Intro to dependent/refinement types.
124 125 126

### Dependently-typed Functional Programming

POTTIER Francois committed
127 128 129 130 131
* Effectful functional programming.
* Dependent functional programming.
* Total functional programming.
* Generic functional programming.
* Open problems in dependent functional programming.
132

REMY Didier committed
133 134 135 136 137 138 139
## Evaluation of the course

Two written exams (a partial and a final exam) 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.

REMY Didier committed
140 141
Although the course has changed, you may still have a look at previous exams
available with solutions:
REMY Didier committed
142

143
- mid-term exam 2016-2017:
REMY Didier committed
144
 [Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf)
145
- mid-term exam 2015-2016:
REMY Didier committed
146 147
 [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)
148
- mid-term exam 2014-2015:
REMY Didier committed
149
 [Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf)
150
- final exam 2013-2014:
REMY Didier committed
151
 [Operation on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf)
152
- mid-term exam 2013-2014:
REMY Didier committed
153
 [Typechecking Effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf)
154
- final exam 2012-2013:
REMY Didier committed
155
 [Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf)
156
- mid-term exam 2012-2013:
REMY Didier committed
157
 [Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf)
158
- final exam  2011-2012:
REMY Didier committed
159
 [Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf)
160
- mid-term exam  2011-2012:
REMY Didier committed
161
 [Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf)
REMY Didier committed
162
- final exam 2010-2011:
REMY Didier committed
163
  [Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf)
REMY Didier committed
164
- mid-term exam 2010-2011:
REMY Didier committed
165
 [Compilation
REMY Didier committed
166
 of polymorphic records](http://gallium.inria.fr/~remy/mpri/exams/2010/partiel-2010-2011.pdf)
REMY Didier committed
167

168 169
## Recommended software

170
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
171

172
Then, install OCaml 4.0x and Coq **8.5** via the following commands:
173 174 175 176 177 178
```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
```
179 180 181 182
(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 committed
183

184 185 186 187 188 189 190 191 192
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
```

193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
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
```

212 213 214 215 216 217
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 committed
218 219 220

## Bibliography

221
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
POTTIER Francois committed
222
Benjamin C. Pierce, MIT Press, 2002.
REMY Didier committed
223 224 225

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