Blogs (27) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 14:00 - 14:30 at L3 - Effects and Dependent Types

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar’s effect theories, whose dependently typed operations allow us to capture precise notions of computation, e.g., state with location-dependent store types and dependently typed update monads. Our treatment of handlers is based on an observation that their conventional term-level definition leads to unsound program equivalences being derivable in languages that include a notion of homomorphism. We solve this problem by giving handlers a novel type-based treatment via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations), based on Plotkin and Pretnar’s insight that handlers denote algebras for a given algebraic theory. The conventional presentation of handlers can then be routinely derived from our type-based treatment. We also demonstrate that our treatment of handlers provides a useful mechanism for reasoning about effectful computations.

Sun 3 Sep

hope-2017-talks
14:00 - 15:00: HOPE 2017 - Effects and Dependent Types at L3
hope-2017-talks150444000000014:00 - 14:30
Talk
hope-2017-talks150444180000014:30 - 15:00
Talk