Wed 10 Jan 2018 11:20 - 11:45 at Watercourt - Types and Effects Chair(s): Neel Krishnaswami

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), capturing Plotkin and Pretnar’s insight that handlers denote algebras. We show that the conventional presentation of handlers can then be routinely derived. We also demonstrate that this type-based treatment of handlers provides a useful mechanism for reasoning about effectful computations.

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Types and EffectsResearch Papers at Watercourt
Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge
10:30
25m
Talk
Linear Haskell: practical linearity in a higher-order polymorphic language
Research Papers
Jean-Philippe Bernardy University of Gothenburg, Mathieu Boespflug Tweag I/O, Ryan R. Newton Indiana University, Simon Peyton Jones Microsoft Research, Arnaud Spiwack Tweag I/O
Pre-print File Attached
10:55
25m
Talk
Polyadic Approximations, Fibrations and Intersection Types
Research Papers
11:20
25m
Talk
Handling fibred algebraic effects
Research Papers
Danel Ahman Inria Paris
11:45
25m
Talk
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław