Handling Fibred Algebraic Effects - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2018

Handling Fibred Algebraic Effects

Résumé

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar’s effect theories, whose dependently typed operations allow us to capture precise notions of computation, e.g., state with location-dependent store types and dependently typed update monads. Our treatment of handlers is based on an observation that their conventional term-level definition leads to unsound program equivalences being derivable in languages that include a notion of homomorphism. We solve this problem by giving handlers a novel type-based treatment via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a set of value terms (the operations), capturing Plotkin and Pretnar’s insight that effect handlers denote algebras. We then show that the conventional presentation of handlers can be routinely derived, and demonstrate that this type-based treatment of handlers provides a useful mechanism for reasoning about effectful computations. We also equip the resulting language with a sound denotational semantics based on families fibrations.
Fichier principal
Vignette du fichier
popl18.pdf (427.83 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01672734 , version 1 (12-10-2019)

Licence

Paternité

Identifiants

Citer

Danel Ahman. Handling Fibred Algebraic Effects. Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), pp.1-29. ⟨10.1145/3158095⟩. ⟨hal-01672734⟩

Collections

INRIA INRIA2
120 Consultations
92 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More