Opin vísindi

Algebraic and coalgebraic perspectives on interaction laws

Algebraic and coalgebraic perspectives on interaction laws

Title: Algebraic and coalgebraic perspectives on interaction laws
Author: Uustalu, Tarmo   orcid.org/0000-0002-1297-0579
Voorneveld, Niels   orcid.org/0000-0001-6650-3493
Date: 2020
Language: English
Scope: 186-205
University/Institute: Reykjavik University
Háskólinn í Reykjavík
School: School of Technology (RU)
Tæknisvið (HR)
Department: Department of Computer Science (RU)
Tölvunarfræðideild (HR)
ISBN: 9783030644369
Series: Lecture Notes in Computer Science;12470
ISSN: 0302-9743
DOI: 10.1007/978-3-030-64437-6_10
Subject: Monad algebras; Comonad coalgebras; Interaction laws; Runners; Monad morphisms; Effects; Coeffects; Algebra; Tölvunarfræði
URI: https://hdl.handle.net/20.500.11815/4001

Show full item record


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


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.

Files in this item

This item appears in the following Collection(s)