1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
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
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
% Lambda Nantes \newline Compréhension, Interprétation et implémentation du $\lambda$-calcul
% **Workshop 1:** 10 Octobre 2024 @ **Palo IT Nantes**
% **Arnaud Bailly** (Cardano Foundation) et **Xavier Van de Woestyne** (Tarides)
# Une nouvelle formule !
> En complément des présentations (habituelles), on voudrait proposer
> un nouveau format, plus interactif, potentiellement plus accessible
> et probablement plus _transportable_ en visio-conférence !
\pause
- Des **workshops interactifs**
- **Indépendants** des langages et technologies (tout est le bienvenu)
- **Pérennes** dans le temps (en permettant notamment plusieurs
sessions sur un même sujet)
- Construction du platforme web pour le **suivi** des workshops (dans
un futur _proche_)
# Pleins d'idées de sujets
- **Compréhension, interprétation et implémentation du
$\lambda$-calcul**
- Implémentation d'applications web, **dans un style fonctionnel**
(pour remplacer, par exemple, les affreuses applications
propriétaires que l'on utilise, comme Meetup, et **parce que c'est
très rigolo de réinventer la roue !**)
- **Vos sujets** (en tant que suggestion, en tant qu'organisateurs, ce
_que vous voulez_), nous somme très ouverts à la contribution et à
l'apprentissage
# Compréhension, Interprétation et implémentation du $\lambda$-calcul
> On dit souvent qu'une compréhension fine du $\lambda$-calcul, la
> base de la programmation fonctionnelle est nécéssaire pour la
> comprendre.
\pause
> **Je prétend que c'est faux** (de la même manière qu'une
> compréhension fine de la théorie des catégories) n'est absolument un
> prérequis (ou une nécéssité) pour faire du Haskell efficacement.
# Alors pourquoi ce premier Workshop ?
- **Ça permet de s'initier à la construction d'un langage**
- C'est tout de même intéressant
- Le $\lambda$-calcul permet de **comprendre** certains points
théoriques liés à la compilation et l'interprétation de langages de
programmation
- Permet de se familiariser avec certains encodages dans des langages
plus riches
- Ça se découpe bien en plusieurs parties
# C'est quoi le $\lambda$-calcul ?
- Un système formel inventé dans les années 30, par **Alonzo Church**
qui décrit/fonde les concepts de **fonctions et d'applications de
fonctions** (qui est, en fait, un langage de programmation théorique)
- Premier formalisme permettant de décrire et caractériser **les
fonctions récursives**, permettant de décrire la notion de
**calculabilité** (que l'on appellera, plus tard, la
_Turing-completude_)\newline\newline
\pause
> Comme pour le modèle de Herbrand-Gödel et les machines de turing, il
> est un des fondaments de la calculabilité, donc de la programmation
> et offre le même niveau d'expressivité.
# Aujourd'hui
- Base conceptuelle des langages de programmations fonctionnels
modernes (laissant à la machine de Turing le rôle de base
conceptuelle des langages impératifs)
- Permet de servir de base pour des modèles de programmations
(certains motifs de conceptions par exemple)
- Sert le travail de l'ingénieur quotidiennement, notamment pour la
construction d'outils (ie: _refactor Engine_ qui est généralement
une conséquence de la $\beta$-reduction ou encore l'indexation
d'occurences via des formes de normalisation)
- Permet d'implémenter des langages en étant étendu, de servir de
cible de compilation et aussi d'outil de comparaison entre des
langages (via des procédés d'analyse sémantique)\pause
- Permet d'organiser des Workshops (dans lesquels on pourra ajouter
des fonctionnalités, un système de type etc) !
# Une grammaire **incroyablement** simple !
Les constituants du $\lambda$-calcul sont appelés des
$\lambda$-termes.
## Variables : `<nom>`
`x` est une variable de nom `x`.
## Abstraction : $\lambda$`<paramètres>.<corps>`
$\lambda x. x$ est la fonction **identité**.
## Application : `<fonction><lambda-terme>`
($\lambda x. x$)`a`, on applique l'identité à `a`.
# En d'autres termes:
```
Term (M, N, O, ...):
M ::= x (variable)
M ::= λx.M (abstraction)
M ::= M N (application)
```
> Comment résoudre des fonctions à plusieurs argument ? La
> **curryfication** !
# Avec quelques conventions de parenthèsages
```
(M) ≡ M
λx.(M N) ≡ λx.M N
λx.(λy.M) ≡ λx.λy.M
(M N) O ≡ M N O
```
---
Avec ces trois éléments, on peut déjà construire beaucoup de choses !
Le fait d'utiliser uniquement des fonctions et des applications pour
encoder des choses s'appelle l'utilisation de
**church-encodings**. (La base de l'OOP en vrai)
## Des booléens
- `TRUE := λx.λy.x`
- `FALSE := λx.λy.y`
\pause
- `AND := λp.λq.p q p`
- `OR := λp.λq.p p q`
- `NOT := λp.p FALSE TRUE`
\pause
- `IFTD := λp.λa.λb.p a b`
---
## De l'arithmétiques
- `0 := λfx.x`
- `1 := λfx.f x`
- `2 := λfx.f (f x)`
- `3 := λfx.f (f (f x))`
- etc.
\pause
- `SUCC := λn.λf.λx.f (n f x)`
- `PLUS := λm.λn.m SUCC n`
- etc.
# Première étape: décrire un AST
Un **AST** (ou, Arbre de Syntaxe Abstrait) est une représentation
manipulable de notre syntaxe.
Avec un AST, on peut, par exemple, considérer que les deux expressions
sont équivalentes :
- `let f x = x + 1`
- `let f x = (+) x 1`
Il est usuel d'utiliser des **sommes** pour décrire les différentes
branches (souvent récursives) de notre arbre !
# Concepts de variables **libres**
> **Une peu naïvement** : Ensembles des variables qui ne sont pas des
> arguments (dans un scope donné). Par exemple:
```
λx.x # Pas de variables libres
λx.x+y # y est libre
```
Quand une variable n'est pas libre, elle est **liée**
# Réductions
Permettant de décrire des équivalence de Lambda Termes.
- $\alpha$-conversion: la **résolution des noms** (`λx.x` = `λy.y`)
(qui entraine des **Substitutions**)
- $\beta$-conversion: l'**application de fonction** (`(λx.x × + 2) 7`
= `7 + 2` = `9`)
- $\eta$-reduction: `(λx.f x)` = `f` si `x` n'est pas **libre**
La base de stratégie d'évaluation et d'optimisation ! (En effet, on
réduira généralement durant l'évaluation d'un programme)
---
On a suffisamment de "bases" pour démarrer !
|
