We present handler calculus, a core calculus of effect handlers. Inspired by the Frank programming language, handler calculus does not have primitive functions, just handlers. Functions, products, sums, and inductive types, are all encodable in handler calculus. We extend handler calculus with recursive effects, which we use to encode recursive data types. We extend handler calculus with parametric operations, which we use to encode existential data types. We then briefly outline how one can encode universal data types by composing a CPS translation for parametric handler calculus into System F with Fujita’s CPS translation of System F into minimal existential logic.
Sun 22 AugDisplayed time zone: Seoul change
20:00 - 21:30
|Higher-Order Asynchronous Effects
Danel Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia, Janez Radešček University of LjubljanaPre-print File Attached
Sam Lindley The University of Edinburgh, UKFile Attached
|A Monad for Shared-State Concurrency