Titill: | Algebraic and coalgebraic perspectives on interaction laws |
Höfundur: |
|
Útgáfa: | 2020 |
Tungumál: | Enska |
Umfang: | 186-205 |
Háskóli/Stofnun: | Reykjavik University Háskólinn í Reykjavík |
Svið: | School of Technology (RU) Tæknisvið (HR) |
Deild: | Department of Computer Science (RU) Tölvunarfræðideild (HR) |
ISBN: | 9783030644369 9783030644376 |
Birtist í: | Lecture Notes in Computer Science;12470 |
ISSN: | 0302-9743 1611-3349 |
DOI: | 10.1007/978-3-030-64437-6_10 |
Efnisorð: | Monad algebras; Comonad coalgebras; Interaction laws; Runners; Monad morphisms; Effects; Coeffects; Algebra; Tölvunarfræði |
URI: | https://hdl.handle.net/20.500.11815/4001 |
Tilvitnun:T. Uustalu, N. Voorneveld. Algebraic and coalgebraic perspectives on interaction laws. In B. C. d. S. Oliveira, ed., Programming Languages and Systems: 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 – December 2, 2020, Proceedings, Lecture Notes in Comput. Science, v. 12470, pp. 186-205. Springer, Cham, 2020. doi:10.1007/978-3-030-64437-6_10
|
|
Útdráttur:Monad algebras, turning computations over return values into values, are used to handle algebraic effects invoked by programs, whereas comonad coalgebras, turning initial states into environments (“cocomputations”) over states, describe production of coalgebraic coeffects that can respond to effects. (Monad-comonad) interaction laws by Katsumata et al. describe interaction protocols between a computation and an environment. We show that any triple of those devices can be combined into a single algebra handling computations over state predicates. This method yields an isomorphism between the category of interaction laws, and the category of so-called merge functors which merge algebras and coalgebras to form combined algebras. In a similar vein, we can combine interaction laws with coalgebras only, retrieving Uustalu’s stateful runners. If instead we combine interaction laws with algebras only, we get a novel concept of continuation-based runners that lift an environment of value predicates to a single predicate on computations of values. We use these notions to study different running examples of interactions of computations and environments.
|