% 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 : `` `x` est une variable de nom `x`. ## Abstraction : $\lambda$`.` $\lambda x. x$ est la fonction **identité**. ## Application : `` ($\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 !