A Fibrational Account of Local States - Archive ouverte HAL Access content directly
Conference Papers Year :

A Fibrational Account of Local States

(1) , (2, 3)
1
2
3

Abstract

One main challenge of the theory of computational effects is to understand how to combine various notions of effects in a meaningful way. Here, we study the particular case of the local state monad, which we would like to express as the result of combining together a family of global state monads parametrized by the number of available registers. To that purpose, we develop a notion of indexed monad inspired by the early work by Street, which refines and generalizes Power's recent notion of indexed Lawvere theory. One main achievement of the paper is to integrate the block structure necessary to encode allocation as part of the resulting notion of indexed state monad. We then explain how to recover the local state monad from the functorial data provided by our notion of indexed state monad. This reconstruction is based on the guiding idea that an algebra of the indexed state monad should be defined as a section of a 2-categorical notion of fibration associated to the indexed state monad by a Grothendieck construction.
Fichier principal
Vignette du fichier
fibrational-view-of-local-states.pdf (311.12 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03066087 , version 1 (15-12-2020)

Identifiers

Cite

Kenji Maillard, Paul-André Melliès. A Fibrational Account of Local States. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, France. pp.402-413, ⟨10.1109/LICS.2015.45⟩. ⟨hal-03066087⟩
36 View
188 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More