In this Tutorial we are going to look at advanced programming with typed effect handlers and FBIP in the Koka language.

• An overview of the current status of Koka: Using recent techniques like Perceus [1] and evidence passing [2] Koka compiles to plain C code without needing garbage collection or a runtime system. Demonstrate the interactive environment and give a primer on Koka syntax including “with” syntax and trailing lambdas.

• Effect handlers: we show various patterns of effect handlers and effect typing using row-polymorphism. We also discuss masking and local state, and the theory behind evidence passing.

• FBIP – functional but in-place: this is a novel technique that relies on Perceus style reference counting. Just like we can express loops in a functional style using tail-recursion, we can express various imperative (mutating) algorithms in a purely functianal way using FBIP. We discuss tree rebalancing, and generic zipper visitor patterns that can rebalance in-place.

• Advanced Effect Handlers: if we have time, discuss initially/finally, linear effects, named handlers, first-class heaps [3], async/await, etc.

Planned programme (with 5min breaks between each part): in EST/NewYork

12:30: A primer on Koka, syntax and effect types.
13:00: Algebraic Effect Handlers.
13:30: Operational Semantics and Evidence Passing.
break.
14:30: FBIP: functional but in-place algorithms.
15:00: Linear Resource Calculus.
15:20: Advanced Effect Handlers: mask behind, linear effects, initially/finally, etc.
16:00: end

References:

[1] Perceus: Garbage Free Reference Counting with Reuse. Alex Reinking*, Ningning Xie*, Leonardo de Moura, Daan Leijen. PLDI’21. pdf.
[2] Generalized Evidence Passing for Effect Handlers (or, Efficient Compilation of Effect Handlers to C). Ningning Xie, Daan Leijen. ICFP’21. pdf.
[3] First-class Named Effect Handlers. Ningning Xie, Youyou Cong, Daan Leijen. HOPE’21. pdf