التفاصيل البيبلوغرافية
| العنوان: |
Explicit effect subtyping. |
| المؤلفون: |
KARACHALIAS, GEORGIOS, PRETNAR, MATIJA, SALEH, AMR HANY, VANDERHALLEN, STIEN, SCHRIJVERS, TOM |
| المصدر: |
Journal of Functional Programming; 2020, Vol. 30, p1-57, 57p |
| مصطلحات موضوعية: |
ALGEBRAIC equations, PROGRAMMING languages, MATHEMATICAL analysis, NUMERICAL calculations, ALGORITHMS |
| مستخلص: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Journal of Functional Programming is the property of Cambridge University Press and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| قاعدة البيانات: |
Complementary Index |
