diff options
Diffstat (limited to 'support')
| -rw-r--r-- | support/2024-10-10.md | 216 | ||||
| -rw-r--r-- | support/2024-10-10.pdf | bin | 60690 -> 0 bytes | |||
| -rw-r--r-- | support/Makefile | 11 |
3 files changed, 0 insertions, 227 deletions
diff --git a/support/2024-10-10.md b/support/2024-10-10.md deleted file mode 100644 index 390ff10..0000000 --- a/support/2024-10-10.md +++ /dev/null @@ -1,216 +0,0 @@ -% 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 ! diff --git a/support/2024-10-10.pdf b/support/2024-10-10.pdf Binary files differdeleted file mode 100644 index 68a3c7b..0000000 --- a/support/2024-10-10.pdf +++ /dev/null diff --git a/support/Makefile b/support/Makefile deleted file mode 100644 index 2a45ef1..0000000 --- a/support/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -all: 2024-10-10.pdf - -%.pdf: %.md - pandoc -t beamer -f markdown+implicit_figures \ - -V theme:default -V aspectratio:169 \ - --pdf-engine=xelatex \ - -V monofont='DejaVu Sans Mono' \ - $(<) -o $(@) - -clean: - rm -rf *.pdf |