I recently wrote a paper Iteration and labelled iteration with Paul. Summary: When you naively add iteration to lambda calculus, nested loops with control are very inconvenient in the resulting language. The inconvenience is rather like trying to program with De Bruijn indices. We give an alternative syntax using second-order labels.
» paper html / pdf
My research is about improving functional programming, specifically tweaking algebraic operations and handlers. Intuitively, we know that we can “implement” all kinds of effects using handlers. But is this really true? Can we make it true?
If we handle
set operations with
runState, then we want to optimise e.g.
get() + get() to
2 × get(). Unfortunately, this optimisation is invalid under lambdas, at least in most incarnations of effect&handler systems. This is because you can always install a new handler for
get and then run your lambda under the new handler. It is very difficult to know what handler will be active at the time a lambda is activated.
So I play with a different effect&handler system. In my system, handlers bind operation names. So if you make
(λx. get() + get()) directly under
runState, then even if you install a new handler, the
get will still always point to the
runState. And so we know that
(λx. get() + get()) = (λx. 2 × get()).
My recent iteration paper helps set up the syntax for such a language with handlers of lexical operations. » more about my research