Coalgebraic aspects of bidirectional computation
We have previously (Bx, 2014; MPC, 2015) shown that several statebased bx formalisms can be captured using monadic functional programming, using the state monad together with possibly other monadic effects, giving rise to structures we have called monadic bx (mbx). In this paper, we develop a coalge...
Main Authors: | , , |
---|---|
Format: | Journal article |
Published: |
Association Internationale pour les Technologies Objets
2017
|
_version_ | 1797084895645794304 |
---|---|
author | Abou-Saleh, F McKinna, J Gibbons, J |
author_facet | Abou-Saleh, F McKinna, J Gibbons, J |
author_sort | Abou-Saleh, F |
collection | OXFORD |
description | We have previously (Bx, 2014; MPC, 2015) shown that several statebased bx formalisms can be captured using monadic functional programming, using the state monad together with possibly other monadic effects, giving rise to structures we have called monadic bx (mbx). In this paper, we develop a coalgebraic theory of state-based bx, and relate the resulting coalgebraic structures (cbx) to mbx. We show that cbx support a notion of composition coherent with, but conceptually simpler than, our previous mbx definition. Coalgebraic bisimulation yields a natural notion of behavioural equivalence on cbx, which respects composition, and essentially includes symmetric lens equivalence as a special case. Finally, we speculate on the applications of this coalgebraic perspective to other bx constructions and formalisms. |
first_indexed | 2024-03-07T02:01:34Z |
format | Journal article |
id | oxford-uuid:9d88c774-9512-409d-b58b-e75b0cb63bc0 |
institution | University of Oxford |
last_indexed | 2024-03-07T02:01:34Z |
publishDate | 2017 |
publisher | Association Internationale pour les Technologies Objets |
record_format | dspace |
spelling | oxford-uuid:9d88c774-9512-409d-b58b-e75b0cb63bc02022-03-27T00:43:48ZCoalgebraic aspects of bidirectional computationJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:9d88c774-9512-409d-b58b-e75b0cb63bc0Symplectic Elements at OxfordAssociation Internationale pour les Technologies Objets2017Abou-Saleh, FMcKinna, JGibbons, JWe have previously (Bx, 2014; MPC, 2015) shown that several statebased bx formalisms can be captured using monadic functional programming, using the state monad together with possibly other monadic effects, giving rise to structures we have called monadic bx (mbx). In this paper, we develop a coalgebraic theory of state-based bx, and relate the resulting coalgebraic structures (cbx) to mbx. We show that cbx support a notion of composition coherent with, but conceptually simpler than, our previous mbx definition. Coalgebraic bisimulation yields a natural notion of behavioural equivalence on cbx, which respects composition, and essentially includes symmetric lens equivalence as a special case. Finally, we speculate on the applications of this coalgebraic perspective to other bx constructions and formalisms. |
spellingShingle | Abou-Saleh, F McKinna, J Gibbons, J Coalgebraic aspects of bidirectional computation |
title | Coalgebraic aspects of bidirectional computation |
title_full | Coalgebraic aspects of bidirectional computation |
title_fullStr | Coalgebraic aspects of bidirectional computation |
title_full_unstemmed | Coalgebraic aspects of bidirectional computation |
title_short | Coalgebraic aspects of bidirectional computation |
title_sort | coalgebraic aspects of bidirectional computation |
work_keys_str_mv | AT abousalehf coalgebraicaspectsofbidirectionalcomputation AT mckinnaj coalgebraicaspectsofbidirectionalcomputation AT gibbonsj coalgebraicaspectsofbidirectionalcomputation |