Programming Languages and Software Technology

Idris Effekt

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.

Related Publications

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