Handling Fibred Algebraic Effects in Dependent Type Systems

Watch a 26-minute conference presentation from POPL 2018 exploring the intersection of algebraic computational effects and their handlers in dependently typed programming languages. Discover how Danel Ahman from Inria France extends Plotkin and Pretnar's effect theories to support dependently typed operations, enabling precise computation representations like state with location-dependent store types. Learn about a novel type-based approach to handlers using user-defined algebra types that pairs carrier value types with operation value terms, addressing soundness issues in languages with homomorphisms. Explore how this framework provides mechanisms for reasoning about effectful computations and includes a sound denotational semantics based on families fibrations.