Résumé
Koka is a strict functional language with full algebraic effect handlers and rich effect typing. The Koka compiler also uses compiler guided reference counting and compiles directly to C code without needing a garbage collector or runtime system. As such, compiling general effect handlers is a challenge as we cannot manipulate the system stack directly to capture continuations.
This seminar talk introduces the design of effect handlers and effect types in Koka with various examples, and then shows how we can use evidence passing in combination with a monadic translation to efficiently compile effect handlers to plain C (or System F). Moreover, we can use the static effect types to lookup evidence in constant time instead of a linear runtime search for the correct effect handler.
