# Une sémantique mécanisée d'un langage FRP avec effets

Jordan Ischard, Frédéric Dabrowski, Jules Chouquet, Frédéric Loulergue

► To cite this version:

Jordan Ischard, Frédéric Dabrowski, Jules Chouquet, Frédéric Loulergue. Une sémantique mécanisée d'un langage FRP avec effets. Journées Approches Formelles pour l'Assistance au Développement de Logiciels (AFADL), Jun 2025, Pau (France), France. hal-05135592

HAL Id: hal-05135592

https://hal.science/hal-05135592v1

Submitted on 30 Jun 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Une sémantique mécanisée d'un langage FRP avec effets
Résumés longs

Jordan Ischard, Frédéric Dabrowski, Jules Chouquet et Frédéric Louergue

Univ. Orléans, INSA CVL, LIFO EA 4022, Orléans, France

## Introduction

La programmation fonctionnelle réactive (FRP) est un paradigme de programmation fonctionnelle conçu pour simplifier la programmation de systèmes interagissant continuellement avec leur environnement. YAMPA [1], une bibliothèque HASKELL, permet de construire des *fonctions de signal* qui traitent un flux d'entrée de manière synchrone afin de produire un flux de sortie. Bien que cette bibliothèque facilite la production de programmes concis et robuste, la gestion des entrées et sorties reste fastidieuse.

WORMHOLES [5, 6] propose une première solution en 2012, suivie, quelques années plus tard, par d'autres [4, 3] dont MSF. WORMHOLES propose d'interagir avec l'environnement dans le programme via deux nouveaux opérateurs : *rsf* et *wormhole* qui se basent sur un concept de ressource. Une ressource représente une interaction avec l'environnement et le langage limite l'usage à une occurrence lors d'un instant logique. Cette contrainte garantit l'hypothèse d'exécution immédiate du point de vue de l'environnement.

Il existe deux types de ressources : libre et liée. Le premier est directement en contact avec l'environnement extérieur alors que le second est interne au programme. Par conséquent, la contrainte d'utilisation unique pour les ressources liées semble pouvoir être retirée. Ceci est la motivation première des travaux présentés dans l'article [2] que nous résumons ici. En effet, avant de proposer une extension du langage, il convient de s'assurer de la solidité des bases de celui-ci. Nous avons trouvé des problèmes dans la formalisation établit par D. Winograd-Cort et P. Hudak, et par conséquent, nous avons proposé des nouvelles définitions pour la syntaxe et la sémantique du langage et nous les avons formalisées en ROCQ.

## Problèmes et corrections

La formalisation du langage WORMHOLES contient trois problèmes principaux :
1. l'absence du point-fixe dans la définition de la syntaxe ;

2. la possibilité d'échappement d'une ressource liée en dehors de sa portée dans
le système de types ;

3. la non-satisfaction de la propriété de progression par la sémantique dynamique.

Nous proposons d'approfondir légèrement les deux premiers points, le troisième étant déjà assez explicite.

Récursion

La syntaxe de WORMHOLES est définie informellement dans l'article original [5] comme un lambda-calcul étendu, avec une valeur de base, des paires, des projections et une récursion, en plus des fonctions de signal et des deux nouveaux opérateurs. Dans la définition formelle, il n'y a pas de terme représentant le point-fixe. Par conséquent, les lemmes et théorèmes proposés dans l'article original ne le prennent pas en compte.

L'ajout d'un point-fixe n'est pas anodin dans un langage. En effet, il rend invalide la propriété de normalisation du langage, c'est-à-dire que l'on ne peut plus établir que tout programme termine. Cependant, sa présence est bénéfique, car il fait gagner en expressivité. Par conséquent, nous avons ajouté un terme *fix* dans la syntaxe représentant le point fixe.

Échappement

Le système de type de WORMHOLES garantit l'utilisation unique des ressources en conservant, dans le type des fonctions de signal, l'ensemble des ressources utilisées. Les ressources liées sont celles associées à un opérateur *wormhole*, dans ce cas, le système de type est censé garantir qu'elles ne peuvent pas être utilisées en dehors de leur portée.

Cependant, il est possible de faire sortir une ressource liée en utilisant la définit-
ion présentée dans l'article original. Par conséquent, nous avons ajouté les con-
traintes minimales dans la règle qui établit le bon typage d'une expression avec
l'opérateur *wormhole* afin empêcher cet échappement.

Formalisation en ROCQ

Pour nous assurer que nos corrections garantissent les propriétés établies dans
l'article original, nous avons formalisé notre variante de WORMHOLES. Le pro-
jet est disponible dans le répertoire :

https://github.com/JordanIschard/Mechanized-Wormholes

Le travail de formalisation est d'environ 5 kLdC (mille lignes de code) : 2KLdC de spécifications (définitions, lemmes, théorèmes, ...) et 3KLdC de démonstrations.
## Conclusion et travaux futurs

Nous avons suggéré de nouvelles définitions pour la syntaxe et la sémantique du langage WORMHOLES, créant une variante de celui-ci. Nous avons démontré que les théorèmes de l'article original sont satisfaits par notre variante. Finalement, nous avons utilisé l'assistant de preuve ROCQ pour s'assurer de la véracité de nos corrections.

Ce résultat nous permet de revenir à la motivation initiale de ce travail : tenter de relâcher un maximum les restrictions sur les lectures et écritures. En effet, nous pensons que les restrictions sur les ressources liées pourraient être assondules sans invalider les propriétés du langage. Cela permettrait de rendre ce dernier plus permissif et d'attirer plus d'utilisateurs. Une autre piste possible est d'utiliser les concepts introduits par WORMHOLES pour définir une bibliothèque FRP dans OCAML. À notre connaissance, il n'existe pour le moment pas de bibliothèque OCAML qui permette d'intégrer les concepts de Yampa aux traits impératifs inhérents à OCAML.

## References

[1] Paul Hudak, Antony Courtney, Henrik Nilsson, and John Peterson. Arrows, robots, and functional reactive programming. In Johan Jeuring and Simon L. Peyton Jones, editors, *Advanced Functional Programming*, volume 2638 of LNCS, pages 159–187. Springer, 2002.

[2] Jordan Ischard, Frederic Dabrowski, Jules Chouquet, and Frédéric Louergue. A Mechanized Formalization of an FRP Language with Effects. In ACM, editor, *ACM Symposium on Applied Computing (SAC)*, Sicily, Italy, March 2025.

[3] Ivan Perez, Manuel Bärenz, and Henrik Nilsson. Functional reactive programming, refactored. In *International Symposium on Haskell*, Haskell 2016, page 33–44, New York, NY, USA, 2016. ACM.

[4] Atze van der Ploeg and Koen Claessen. Practical principled FRP: forget the past, change the future, frpnow! In Kathleen Fisher and John H. Reppy, editors, *International Conference on Functional Programming (ICFP)*, pages 302–314. ACM, 2015.

[5] Daniel Winograd-Cort and Paul Hudak. Wormholes: Introducing effects to FRP. In *International Symposium on Haskell*, New York, NY, USA, 2012. ACM.

[6] Daniel Winograd-Cort, Hai Liu, and Paul Hudak. Virtualizing real-world objects in FRP. In *Practical Aspects of Declarative Languages (PADL)*, volume 7149 of LNCS, pages 227–241. Springer, 2012.