Explicit effect subtyping. (8th June 2020)

• Record Type: Journal Article
• Authors: KARACHALIAS, GEORGIOS; PRETNAR, MATIJA; SALEH, AMR HANY; VANDERHALLEN, STIEN; SCHRIJVERS, TOM
• Is Part Of: Journal of functional programming. Volume 30(2020)
• Publication Date: 2020-06-08
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796820000131
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortunately, in our experience, implementing optimisations for Eff is overly error-prone because its core language is implicitly typed, making code transformations very fragile. To remedy this, we present an explicitly typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.