Lifting of operations in modular monadic semantics
Monads have become a fundamental tool for structuring denotational semantics and programs by abstracting a wide variety of computational features such as side-effects, input/output, exceptions, continuations and non-determinism. In this setting, the notion of a monad is equipped with operations that...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2009
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/11226/ |
| _version_ | 1848791224350146560 |
|---|---|
| author | Jaskelioff, Mauro Javier |
| author_facet | Jaskelioff, Mauro Javier |
| author_sort | Jaskelioff, Mauro Javier |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Monads have become a fundamental tool for structuring denotational semantics and programs by abstracting a wide variety of computational features such as side-effects, input/output, exceptions, continuations and non-determinism. In this setting, the notion of a monad is equipped with operations that allow programmers to manipulate these computational effects. For example, a monad for side-effects is equipped with operations for setting and reading the state, and a monad for exceptions is equipped with operations for throwing and handling exceptions.
When several effects are involved, one can employ the incremental approach to mod- ular monadic semantics, which uses monad transformers to build up the desired monad one effect at a time. However, a limitation of this approach is that the effect-manipulating operations need to be manually lifted to the resulting monad, and consequently, the lifted operations are non-uniform. Moreover, the number of liftings needed in a system grows as the product of the number of monad transformers and operations involved.
This dissertation proposes a theory of uniform lifting of operations that extends the incremental approach to modular monadic semantics with a principled technique for lifting operations. Moreover the theory is generalized from monads to monoids in a monoidal category, making it possible to apply it to structures other than monads.
The extended theory is taken to practice with the implementation of a new extensible monad transformer library in Haskell, and with the use of modular monadic semantics to obtain modular operational semantics. |
| first_indexed | 2025-11-14T18:25:06Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-11226 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:25:06Z |
| publishDate | 2009 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-112262025-02-28T11:12:05Z https://eprints.nottingham.ac.uk/11226/ Lifting of operations in modular monadic semantics Jaskelioff, Mauro Javier Monads have become a fundamental tool for structuring denotational semantics and programs by abstracting a wide variety of computational features such as side-effects, input/output, exceptions, continuations and non-determinism. In this setting, the notion of a monad is equipped with operations that allow programmers to manipulate these computational effects. For example, a monad for side-effects is equipped with operations for setting and reading the state, and a monad for exceptions is equipped with operations for throwing and handling exceptions. When several effects are involved, one can employ the incremental approach to mod- ular monadic semantics, which uses monad transformers to build up the desired monad one effect at a time. However, a limitation of this approach is that the effect-manipulating operations need to be manually lifted to the resulting monad, and consequently, the lifted operations are non-uniform. Moreover, the number of liftings needed in a system grows as the product of the number of monad transformers and operations involved. This dissertation proposes a theory of uniform lifting of operations that extends the incremental approach to modular monadic semantics with a principled technique for lifting operations. Moreover the theory is generalized from monads to monoids in a monoidal category, making it possible to apply it to structures other than monads. The extended theory is taken to practice with the implementation of a new extensible monad transformer library in Haskell, and with the use of modular monadic semantics to obtain modular operational semantics. 2009-12-10 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/11226/1/Thesis.pdf Jaskelioff, Mauro Javier (2009) Lifting of operations in modular monadic semantics. PhD thesis, University of Nottingham. monadic semantics monads programming computers computer science |
| spellingShingle | monadic semantics monads programming computers computer science Jaskelioff, Mauro Javier Lifting of operations in modular monadic semantics |
| title | Lifting of operations in modular monadic semantics |
| title_full | Lifting of operations in modular monadic semantics |
| title_fullStr | Lifting of operations in modular monadic semantics |
| title_full_unstemmed | Lifting of operations in modular monadic semantics |
| title_short | Lifting of operations in modular monadic semantics |
| title_sort | lifting of operations in modular monadic semantics |
| topic | monadic semantics monads programming computers computer science |
| url | https://eprints.nottingham.ac.uk/11226/ |