Research summary

It’s been long since I let you know what I’m doing, so let me try to explain what I’m at!

Purely functional programming works well for some applications, but others are more naturally expressed using some side effects. Monads have been great in programming semi-functionally with strong guarantees. I investigate an alternative approach, which promises to improve on existing work in

• dealing well with combinations of effects,
• having a clean denotational and operational semantics, as well as
• having a useful equational theory.

I will now outline my research program in more detail. In particular, I indicate where the existing approaches have shortcomings.

It is common in languages such as Haskell to encode the monad in question as a Haskell data type with its operations, return, and >>=. However, there are composability drawbacks to encoding the appropriate effect monad as a data type in a programming language. [1]

Plotkin and Power [4] found that for many effects, the monad arises from a set of operations subject to equations, and treated them as primitive instead of the monad. Plotkin and Pretnar [5] introduced a concept of handler: a language construct that interprets operations and maps them to different code, subject to the equations. However, the equational theory on terms is only defined in terms of their denotations.

Bauer and Pretnar [6], in turn, treated handlers as primitive, and obtained denotational and operational semantics. Rather than a priori equations, the handlers give “meaning” to the operations. For instance, they show that directly under a pair of state handlers, the state equations hold.

Bauer and Pretnar’s paper validates Kammar and Plotkin’s work on effectful terms on a more fine-grained way [2]: each term has an “effect type” that lists the effects that may result from its execution. If a handler handles certain operations without re-throwing those operations, those operations can be subtracted from the outer effect type. In other words: to write an effectless program, you can instead write a handler which interprets effects, and put inside it an effectful program.

The state handler is a good example: it “creates” a temporary memory cell that is functional inside the handler, but operations corresponding to the state are not visible on the outside. There is an analogy with monad transformers in Haskell, which “list” the effects of a subprogram; “handling” a state effect with evalStateT removes StateT from the stack of monad transformers.

But the notion of handler in “Core Eff”, as described by Bauer, Plotkin, and Pretnar, allows only a weak equational theory: the state equations cannot in general hold under thunks (“lambdas”), because thunks might escape from those state handlers, or they might be applied under nested handlers with different behaviour.

These two problems are ruled out syntactically in our variant notion of handler, which binds the operations, up to alpha equivalence. Like Bauer and Pretnar’s model, our computation judgements list the operations that might be observed on the outside. Thunks with bound operations cannot escape from the corresponding handler, in the same way that free $$x$$ is unrelated to bound $$x$$ in $$\langle x, \lambda x. x\rangle$$. Thunks with operations can float into nested handlers, but alpha renaming ensures that those handlers handle different operations. We suspect that the language has a clean equational theory, and clean denotational and operational semantics. Specifically, all operations in this model are algebraic [3], that is, they commute with evaluation contexts.

In particular, we hope that many optimisations in [2] follow from the equational theory for our system, from the definitions of the handlers.

Notes and references

 [1] I will detail these in the future.
 [2] (1, 2) Ohad Kammar and Gordon D. Plotkin. Algebraic foundations for effect-dependent optimisations. ACM SIGPLAN Notices, 47(1):349, 2012. doi:10.1145/2103621.2103698.
 [3] Gordon Plotkin and John Power. Algebraic operations and general effects. Applied Categorical Structures, 11(1):69, 2003. doi:10.1023/A:1023064908962.
 [4] Gordon Plotkin and John Power. Computational effects and operations: an overview. Electronic Notes in Theoretical Computer Science, 73:149, 2004. doi:10.1016/j.entcs.2004.08.008.
 [5] Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science, December 2013. doi:10.2168/LMCS-9(4:23)2013.
 [6] (1, 2) Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 2014. doi:10.2168/LMCS-10(4:9)2014.