Takahiro Sanada - Category-Graded Algebraic Theories and Effect Handlers

entics:10491 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10491
Category-Graded Algebraic Theories and Effect HandlersArticle

Authors: Takahiro Sanada

    We provide an effect system CatEff based on a category-graded extension of algebraic theories that correspond to category-graded monads. CatEff has category-graded operations and handlers. Effects in CatEff are graded by morphisms of the grading category. Grading morphisms represent fine structures of effects such as dependencies or sorts of states. Handlers in CatEff are regarded as an implementation of category-graded effects. We define the notion of category-graded algebraic theory to give semantics of CatEff and prove soundness and adequacy. We also give an example using category-graded effects to express protocols for sending receiving typed data.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: December 16, 2022
    Submitted on: December 16, 2022
    Keywords: Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 180 times.
    This article's PDF has been downloaded 137 times.