Qualified Effect Types — Taming Control-Flow through Linear Effect Handlers
- Jonathan Immanuel Brachthäuser ,
- Daan Leijen
MSR-TR-2023-42 |
Published by Microsoft
This technical report is the result of an internship of Jonathan Brachthäuser at Microsoft Research, Redmond in 2018. While the report is published in 2023, the paper reflects the work at the time of writing.
Combining control effects with global side-effects and ex- ternal resources can lead to code which is hard to reason about. We introduce the concept of control-flow linearity (in contrast to data-flow linearity) as a tool for the programmer to reason about control-flow in the presence of control effects. Through a novel combination of an effect system with qualified types we track the control-flow linearity of each effect as part of the effect type of a function. We formalize control-flow linearity and prove soundness of our linearity analysis.