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.
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