Quantified computational effects and interaction - verkefni lokið
Fréttatilkynning verkefnisstjóra
In functional programming, one distinguishes between purely functional computation (computation of return values from arguments) and computation with effects (manipulation of memory, interactive input-output, nondeterminism etc.). Effectful computations run in an interaction with the world outside them; they issue requests to the world (for example, a computation may issue a fetch request to memory) and expect adequate responses.
We set out to study two relevant mathematical structures: graded monads as a model of effectful
computations where the effect is quantified (one can reason about degrees of effectfulness) and
monad-comonad interaction laws as a model of communication protocols between effectful
computations and coeffectful environments. We achieved our original goals (confirmed our original research hypotheses) and surpassed them. We found out that a considerably finer tool for
quantitative analysis of effects than graded monads is provided by what we christened flexibly
graded monads and established the precise relationship of the two concepts. Going considerably
beyond working out the basic theory of monad-comonad interaction laws along the lines we had
envisaged, we were able to develop a (co)algebraic perspective and an abstraction from monads to
monoids.
∙ Information on how the results will be applied
The results will in due time impact functional programming practice through new programming
methodology, new program analysis and verification tools and new programming languages. We are directly contributing with prototype implementations of our constructions and demonstrations
thereof to developers.
∙ A list of the project’s outputs
-16 research articles, including some in the most prestigious conferences in our field (LICS 2020, FoSSaCS 2022, ICFP 2022),
- presentations at the respective conferences and workshops,
- presentations at many further meetings and seminars,
- two summer schools courses(MGS 2021, OPLSS 2021), a tutorial at a conference (ICFP 2021),
- Haskell and Agda code implementing/formalizing the results.
See the project webpage http://www.ru.is/faculty/tarmo/qei/ for detailed lists.
Heiti verkefnis: Quantified computational effects and interaction
Verkefnisstjóri: Tarmo Uustalu,
Háskólanum í Reykjavík
Tegund styrks: Verkefnisstyrkur
Styrktímabil: 2017-2019
Fjárhæð styrks kr. 46.314.000
Tilvísunarnúmer Rannís: 196323
