Blogs (28) >>
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

Displayed time zone: Belfast change

14:00 - 15:00
Effects and Dependent TypesHOPE at L3
14:00
30m
Talk
Handling fibred algebraic effects
HOPE
Danel Ahman University of Edinburgh
14:30
30m
Talk
Only Control Effects and Dependent Types
HOPE
Youyou Cong Ochanomizu University, William J. Bowman Northeastern University