Programming Languages

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

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