Prism : un langage fonctionnel non pur avec effets typés

• Prism est un compilateur expérimental qui ne cache pas les effets comme les variables mutables, les exceptions ou les flux, mais les expose dans les types, tout en conservant un type pur comme Int -> Int pour les mutations locales non observables de l’extérieur
• Son idée centrale repose sur les handlers d’effets algébriques et le polymorphisme de rangée (row polymorphism), où les effets sont réunis dans la rangée du type de fonction, et les handlers ne traitent que les labels nécessaires avant de transmettre le reste
• Le même système d’effets permet d’exprimer les exceptions, les générateurs/flux, les lenses, l’état var, et les flux fail/guard, certains chemins étant abaissés sans listes intermédiaires ni composition à l’exécution
• Côté performances, Prism combine le evidence passing avec le comptage de références Perceus pour éviter les allocations à chaque appel d’effet, et optimise les mises à jour fonctionnelles de valeurs possédées de manière unique en mutations en place
• Prism fournit aussi LLVM IR, MLIR, un runtime C, un interpréteur Rust, un modèle Lean 4 et un playground WASM, ce qui permet d’inspecter directement l’inférence de types et les résultats du lowering

---

Mutations invisibles de l’extérieur et effets typés

• Le point de départ de Prism est qu’une fonction fib qui utilise var et l’affectation en interne peut malgré tout apparaître comme une fonction pure pour un observateur externe
  • L’exemple fib met à jour deux variables en place, sans exposer d’état hors de la fonction
  • Son type est Int -> Int, et l’effet n’apparaît pas dans le type
• Prism est un compilateur fonctionnel de preuve de concept développé depuis trois ans, qui modélise les effets à partir d’idées modernes de typage issues des familles OCaml 5, Haskell et Koka
• L’objectif central n’est pas d’éviter les effets, mais de les intégrer dans le système de types et de laisser le compilateur en éliminer le coût par optimisation

Les effets se comportent comme des interfaces

• Dans Prism, les effets déclarent des opérations, et les handlers leur donnent une sémantique selon le modèle des handlers d’effets algébriques
  • effect Gen { ctl yield(Int) : Unit } déclare l’opération yield
  • Le !{Gen} de fn produce(n) : !{Gen} Unit indique dans le type que la fonction effectue un yield
• Un même producteur peut être interprété différemment selon la manière dont on traite la continuation k
  • total additionne les valeurs de yield
  • count compte le nombre d’appels à yield
  • Si l’on abandonne k, on obtient une exception ; si on l’appelle une fois, un état ou un générateur ; si on l’appelle plusieurs fois, un comportement d’exploration
• L’exemple de l’effet Amb exprime la recherche de triplets pythagoriciens avec choose et reject
  • choose(n) fournit des valeurs dans l’intervalle 0..n-1
  • Le handler relance la même continuation pour chaque candidat afin de construire un arbre d’exploration
• Contrairement à OCaml 5, Prism inclut les effets dans les types et n’impose pas de remonter manuellement des couches comme avec une pile de monad transformers en Haskell
  • Les rangées d’effets se fusionnent structurellement au fil des appels
  • Elles se comportent comme un ensemble de labels, pas comme une pile

Des fonctionnalités exprimées par un seul mécanisme

• Exceptions

  • Dans Prism, une exception est un handler qui abandonne la continuation
  • Une clause final ctl détruit k et utilise la valeur de son corps comme résultat du handler
  • Il ne s’agit ni de propager un Result, ni de parsemer la pile d’appels de ?
  • Les exceptions étant des labels dans la rangée d’effets, elles se composent comme des exceptions extensibles
  • Chaque échec est une opération distincte, et la rangée du type de fonction indique quelles exceptions peuvent s’échapper
  • Dans l’exemple Abort et Timeout, fetch a le type !{Abort, Timeout}
  • with_default ne traite que Timeout, renvoie la valeur de repli "cached", et le type ne conserve ensuite que !{Abort}
  • Contrairement aux checked exceptions de Java, cela fonctionne comme un ensemble structurel ouvert et non lié à une hiérarchie de classes

• Générateurs et flux

  • Les flux sont composés de producteurs qui effectuent emit, de transformateurs qui les interceptent puis réémettent, et de consommateurs qui les réduisent avec un fold
  • Le pipeline consiste à imbriquer des handlers autour d’un seul producteur, ce qui évite structurellement la création de listes intermédiaires
  • Exemple : srange(1, n).smap(square).skeep(even).stake(5).ssum()
  • Un arrêt anticipé comme stake(5) est un handler qui abandonne la continuation après avoir obtenu les valeurs nécessaires
  • La bibliothèque de flux est inspirée de pipes et conduit en Haskell

• Lenses

  • Dans Prism, les lenses ne relèvent pas d’une bibliothèque séparée, mais d’une combinaison entre chemins de mise à jour d’enregistrements et modèle mémoire
  • Dans des enregistrements imbriqués, une seule expression de chemin permet de mettre à jour plusieurs champs profonds
  • Exemple : { g | player.pos.x = 30, player.hp = 95, score = 110 }
  • La structure reconstruit la spine des enregistrements imbriqués, mais réutilise les cellules démontées quand la valeur est possédée de manière unique
  • Grâce à cela, une mise à jour fonctionnelle peut être compilée en écriture de pointeurs
  • Aucun type optic n’est alloué ni composé à l’exécution
  • deriving (Lens) génère des accesseurs ordinaires comme score_of et with_score

• État mutable

  • var est désucré en opérations get/set d’un effet privé
  • Un handler installé à la fin du bloc traite cet effet
  • L’analyse d’échappement des closures rejette les cas où l’état pourrait sortir du bloc
  • La fonction englobante peut ainsi conserver une rangée d’effets vide

• Échec

  • L’échec est exprimé comme un effet anonyme Fail, et le système de types gère le fait qu’« une expression peut ne pas produire de valeur »
  • fail() déclenche un échec, et guard(cond) échoue si la condition est fausse
  • ?? utilise une valeur de repli quand l’expression de gauche échoue
  • ?. parcourt une chaîne d’options avec arrêt anticipé
  • Les guards de compréhension élaguent les éléments en échec au lieu de provoquer un crash
  • Comme var est lui aussi un sucre pour des handlers, un bloc transact peut prendre un instantané des variables vivantes et revenir en arrière en cas d’échec

Fonctionnalités de typage modernes

• Prism utilise une inférence bidirectionnelle de types higher-rank de la famille Dunfield-Krishnaswami, afin que la majorité du code n’ait pas besoin d’annotations de type
• Aux frontières qui exigent du polymorphisme d’ordre supérieur, les binders sont explicités avec forall
  • pick(g : forall a. (a) -> a) permet d’appliquer g à la fois à Bool et à Int
  • Dans un cœur Damas-Milner, le premier appel unifierait a avec Bool, ce qui ferait rejeter le second appel
• Le polymorphisme ad hoc est exprimé avec des type classes à la Lean
  • Les instances sont des valeurs nommées
  • given Ord(a) demande un dictionnaire
  • Quand plusieurs instances existent, l’une peut être marquée canonical et les autres passées explicitement via using
• deriving génère les instances répétitives et les accesseurs de champs pour Eq, Ord, Show, Lens, etc.
• Le pattern matching est lui aussi relié aux classes
  • pattern First(n) for Peek = view peek est un pattern qui utilise une méthode de classe comme view
  • head_or peut réutiliser le même pattern sur plusieurs types disposant d’une instance Peek
• show fonctionne de façon orientée type sans classe dédiée
  • Le compilateur synthétise un printer structurel à partir du type statique
  • Il ne lit pas de tags de type à l’exécution pour décider de la représentation à afficher
• Les rangées d’effets sont elles aussi polymorphes
  • fn twice(f : (Unit) -> Int ! {| e}) additionne le résultat d’une fonction passée en argument, quelle que soit sa rangée d’effets e
  • Pour un thunk pur, e s’unifie avec la rangée vide {}
  • Pour un thunk qui effectue des effets comme Tick ou Say, cette rangée est transmise telle quelle

Une compilation qui réduit le coût des effets

• Une implémentation académique classique des effets algébriques reconstruit le calcul sous forme d’arbre de free monad, ce qui peut allouer une petite cellule à chaque opération
• Le chemin rapide de Prism repose sur le evidence passing de la famille Koka
  • Au lieu de reconstruire le calcul pour retrouver un handler, les clauses de handlers actives sont transmises à chaque site d’opération comme des paramètres ordinaires
  • do op est abaissé en appel direct
  • Une seule closure est allouée à l’installation du handler, donc le coût est en O(handlers) et non proportionnel au nombre d’opérations
• L’encodage free monad reste disponible en solution de repli
  • Pour les calculs qui s’échappent vers des structures de données
  • Pour les resumptions multishot véritables
  • Pour des motifs comme les masked handlers
• Les pipelines de flux calculent les evidence d’effets nécessaires au-delà des frontières de fonctions grâce à une analyse de flux interprocédurale
  • Les evidence sont propagées dans les producteurs et transformateurs
  • La chaîne complète est abaissée en une seule boucle
  • Il n’y a ni liste intermédiaire ni allocation d’une cellule par opération
• Cette approche permet à un compilateur d’effets d’obtenir un résultat proche de la stream fusion de Haskell ou de la monomorphisation des adaptateurs d’itérateurs Rust

Modèle mémoire et runtime

• Prism utilise le comptage de références Perceus
  • Les cellules du tas sont libérées de manière déterministe à des points connus statiquement
  • Il n’y a ni pause ni tracing
• La réutilisation limitée au frame consiste à renvoyer vers le constructeur les cellules tout juste démontées par pattern matching
  • Un map sur une liste possédée de manière unique semble rester une fonction pure qui renvoie une nouvelle liste, mais peut en réalité être transformé en mutation en place
  • Les mises à jour par lens compilées en écritures de pointeurs reposent sur le même mécanisme
• La discipline mémoire du runtime ressemble à celle de Lean 4, mais Prism émet du LLVM IR
  • Le LLVM IR est généré via inkwell
  • Un module MLIR textuel est aussi produit pour le même programme
  • Le résultat est lié avec clang au runtime C écrit à la main prism_rt.c
• prism_rt.c est un petit runtime d’environ 2 000 lignes
  • Les cellules du tas utilisent une structure d’au moins 4 words, de la forme { refcount, tag, arity, fields... }
  • Il inclut un allocateur, rc_inc/rc_dec, un allocateur de réutilisation en place, ainsi que des primitives pour les grands entiers et les chaînes
  • Il n’y a ni thread collecteur, ni card table, ni safepoint
• L’allocateur par défaut est le malloc de libc, avec une option mimalloc activable pour les benchmarks
• Le live-cell oracle vérifie par assert à la fin de l’exécution que l’équilibre du tas est à 0, afin que la suite de tests confirme l’absence de garbage

Modèle Lean et validation des backends

• L’interpréteur Prism relève de la famille des machines CEK, et cette machine est reflétée dans le modèle Lean 4 models/Prism.lean
• Le modèle Lean 4 comprend un théorème vérifié mécaniquement établissant que la relation small-step est déterministe
  • Le programme progresse toujours vers exactement un état suivant
• L’interpréteur de l’implémentation Rust sert aussi d’oracle différentiel
  • Tous les programmes du corpus doivent passer par l’interpréteur ainsi que par les backends LLVM, MLIR et binaire C lié
  • Le build ne passe que si les sorties des quatre chemins sont identiques au byte près
• Cette déterminisme sert de base à une exécution durable rejouable
  • En figeant les entrées et en enregistrant l’exécution, l’idée est d’obtenir une relecture bit pour bit
  • Les versions futures visent un Prism capable de vérifier comme propriété de type la sûreté du replay après crash

Playground WASM et code source

• Le même interpréteur est compilé en WASM et permet d’exécuter du code Prism sans installation dans le playground
• Le playground exécute les programmes dans un worker
• Des boutons permettent d’afficher les signatures de type inférées, les rangées d’effets et le core IR abaissé
  • On peut voir la forme concrète prise par une boucle var ou un pipeline de flux après lowering
• Les exemples de l’article sont inclus dans la liste déroulante
• Le code source complet, le modèle Lean et le runtime C sont disponibles dans le dépôt Prism sur GitHub

Filiations d’implémentation et nature du projet

• Le core IR de Prism appartient à la famille call-by-push-value et s’appuie sur Call-by-Push-Value: A Functional/Imperative Synthesis de Levy
• Le chemin rapide pour les effets est proche de Generalized Evidence Passing for Effect Handlers et Effect Handlers, Evidently de Xie et Leijen
• Le modèle mémoire s’appuie sur Perceus: Garbage Free Reference Counting with Reuse, Reference Counting with Frame-Limited Reuse et FP^2: Fully in-Place Functional Programming
• Les rangées d’effets relèvent de la famille du row polymorphism et des scoped labels, et les handlers prolongent Handlers of Algebraic Effects de Plotkin et Pretnar, en passant par Eff et Koka
• Le pattern matching repose sur des decision trees et une usefulness matrix, et la forme pattern combine les view patterns et Pattern Synonyms de GHC
• La couche d’échec reprend The Verse Calculus via des handlers final ctl
• L’orientation de Prism se rapproche moins du « purement fonctionnel » que de l’idée de rendre les effets visibles, typés et composables
• Le projet lui-même se présente moins comme un outil pratique que comme un jouet ou une œuvre quasi artistique, un compilateur conçu pour l’élégance intellectuelle des idées de programmation fonctionnelle

[GN⁺]

Commentaires sur Lobste.rs

• Je ne vois pas bien quel rapport les lentilles ont avec les effets. Chaque fois que l’article mentionne les lentilles, elles semblent sans lien entre elles, à part le fait d’être rangées sous « une astuce déclinée de cinq façons »
  Et je ne comprends pas non plus ce que tick_use() est censé faire. Est-ce qu’on attend vraiment du lecteur qu’il comprenne un exemple aussi tordu sans explication ? Des annotations de type auraient aidé

  • Les lentilles sont expliquées plus en détail ici : https://sdiehl.github.io/prism/spec.html#86-optic-paths
    Malgré tout, au-delà du niveau métaphorique, je ne vois toujours pas très bien le rapport entre les lentilles et les effets. L’auteur écrit :

    This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
    Autrement dit, je pense que la métaphore est la suivante : les monades sont des valeurs, alors que les effets ne sont pas des valeurs mais une forme de structure de contrôle. De même, les lentilles sont des valeurs, tandis que les optic paths de Prism ne sont pas des valeurs, mais plutôt des structures de contrôle dotées d’une syntaxe codée en dur

• Il faudra que je prenne davantage de temps pour comprendre, mais ça a vraiment l’air magnifique

• Vraiment impressionnant. C’est même pour cela que je me demande pourquoi Diehl qualifie le compilateur de jouet à la fin de l’article. Cela ressemble à une preuve de concept réussie, qui montre un nouveau niveau d’élégance

• J’aimerais voir plus en détail à quoi ressemble concrètement la représentation intermédiaire call-by-push-value. Je suis particulièrement curieux de savoir comment elle gère les points de jonction (join points)
  Il existe des articles qui traitent de la théorie consistant à ajouter des effets à CBPV. Dire que les calculs ont des types d’effets et que les valeurs n’en ont pas est assez naturel, mais je n’ai rien vu d’assez concrétisé pour s’appliquer directement au passage de preuves de Koka, donc c’est intéressant
  Globalement, j’aimerais savoir comment il se positionne par rapport à Koka. Avec FBIP, Perceus et le passage de preuves, il est clair que c’est fortement inspiré des travaux sur Koka, tout en étant aussi nettement différent puisqu’il utilise CBPV comme représentation intermédiaire. Je ne vois simplement pas très bien à quel point c’est différent

• Ça ressemble beaucoup à ce que j’essaie de trouver le temps de construire depuis un moment. J’aime bien !

• Un peu hors sujet, mais j’ai toujours trouvé dommage que le projet « write you a haskell » de Stephen se soit arrêté il y a quelques années. Pour Prism, j’aimerais voir une explication d’implémentation de niveau tutoriel

• Je me demande ce qui est « impur » dans ce langage. Le mot n’apparaît que dans le titre et ne revient pas dans le corps du texte
  Comme tous les effets semblent être suivis, les fonctions sans effet restent des fonctions mathématiques. Est-ce que je rate quelque chose ?

  • Cela semble lié à l’utilisation de variables locales mutables à l’intérieur des définitions de fonctions, comme dans la définition donnée de fib. var x est une variable mutable impure, tandis que let x est une variable immuable pure

• C’est vraiment chouette d’avoir implémenté comme une interface supplémentaire des choses qui étaient habituellement traitées comme des fonctionnalités du langage, par exemple yield dans le langage X ou throw dans le langage Y
  Le fait de pouvoir construire plusieurs flux de contrôle — effets de bord, exceptions, continuations — au-dessus d’une même abstraction est une façon intéressante de repenser toute la question de la conception, et j’espère que cela aidera ou stimulera davantage d’exploration et d’innovation. Je pense que j’y reviendrai pendant des années pour y puiser de l’inspiration