Idris Effekt is a small functional language embedded into Idris. It does not (yet) feature effect handlers, but only delimited control. Using dependent types, effectful statements are indexed by the “shape” of the stack. The language serves as case study and shows how to efficiently compile languages with control effects when the shape of the stack is known at compile time.
Since this information might not always be available at compile time, in ongoing work, we are using just-in-time compilation to optimize programs with respect to the order of effect handlers.
Zero-cost Effect Handlers by Staging (Technical Report)
by Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
In Under consideration for publication in Proc. Conf. Programming Language Design and Implementation (PLDI). ACM Press, 2019.Learn More
Typing, Representing, and Abstracting Control: Functional Pearl
by Philipp Schuster and Jonathan Brachthäuser
In Proceedings of the International Workshop on Type-Driven Development. ACM Press, 2018.Learn More