On the expressive power of user-defined effects:
effect handlers, monadic reflection, and delimited
controlWork in Progress
Ohad Kammar<ohad.kammar@cs.ox.ac.uk>
joint work withYannick Forster, Sam Lindley, and Matija Pretnar
The 4th Southern REPLS
Imperial College
27 September 2016
NIVERS

GO FH

YTH

IT

EUR

E

D I

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

N B

U

Effect oriented programming

Native effects
I I/O.
I Mutable state.
I Randomness and non-determinism.

User-defined effectsI Parsing.
I Constraint solving.
I Proof-search tactics.
I Redefine existing effects?

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

A brief history of functional programming and effects

A love-hate story
Effects are harmful. . .
I Disallow useful compiler optimisations.
I Break referential transparency.
I Depart from the λ-calculus (βη-equality, confluence).

But are useful!

A rift and a bridge
ML and Scheme vs. Haskell.
Monads [Moggi’89, Wadler’91], now in Haskell, ML, Scheme, F∗,C++. . .

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Algebraic effects
Monad issues
I No interface for effects.
I Compositionality and modularity issues.
I Steep learning curve.

Plotkin-Power-Pretnar-Bauer
I Add effect operations to Moggi’s theory[Plotkin-Power’02,’03].
I Add exception handlers, and more generally, effect handlers[Plotkin-Pretnar’09].
I Programming with algebraic effects and handlers[Bauer-Pretnar’15].

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Delimited control

Goto on steroids
Effect handlers are a new kind of delimited control effect.
But(!):
I Clean denotational semantics. [Plotkin-Pretnar’09]
I Clean program logic. [Pretnar’s thesis]
I Clean meta-theory: strong normalisation and type-and-effectsystems [K-Lindley-Oury’13], unrestricted polymorphism[K-Pretnar’16], . . .

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Basic research question

Monads, handlers, and delimited control
I How do these abstractions compare?
I How to compare these abstractions?

Macro expressibility [Fellisen’90]
I Expressive power of Turing-complete languages.
I Computability and complexity reductions are too crude.
I Macro translations:II

Keep shared fragment identical.
Compositional a.k.a. local a.k.a. homomorphic.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Contribution: bird’s eye

MAM

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Contribution: bird’s eye

EFFMAM

DEL

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

MON

On the expressive power of user-defined effects

Contribution: bird’s eye

EFF

==
MAM

=
DEL

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

MON

On the expressive power of user-defined effects

Contribution: bird’s eye

EFF
DEL

MAM
MON

EFF`
DEL `

MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Contribution: bird’s eye

EFF
DEL

MAM
MON

===
6∃
DEL `

MAM `

6∃

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

EFF`

6∃MON `On the expressive power of user-defined effects

Contribution: bird’s eye

EFF
DEL

MAM
MON

===6∃

DEL `

MAM `6∃

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

EFF`

6∃MON `On the expressive power of user-defined effects

Contribution: bird’s eye

EFF
DEL

MAM
MON

==EFF`DEL `MAM `6∃MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Contribution: bird’s eye

EFF
DEL

MAM
MON+

EFF`
++

DEL `

MAM `+MON `
EFF`
DEL `

MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Contribution: bird’s eye

EFFDEL

MAMMON++DEL `=+MAM `EFF`==+MON `EFF`
DEL `MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Talk structure

I Short tutorial on algebraic effects, monadic reflection, anddelimited control

Rationale: Most fiddly task was simplifying and unifying calculi.
I Time pertmitting: discuss the negative result.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

The lambda calculus with effects (mam)SyntaxV , W ::=||

split(V , x1 .x2 .M)
case0 (V )case(V , inj1 x1 .M1values
variableunit value
pairingvariant constructor
thunkcomputations
pattern matching: productvoidvariants

|||
|
|
|
|

, inj2 x2 .M2 )V!
return V
let x ← M in N
λx.M
M V
hM1 , M2 iprji Mforce
returnersequencing (monadic bind)function abstraction
function application
computation pairprojection||||
M, N ::=x()(V1 , V2 )inji V{M}

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

The lambda calculus with effects (mam)Syntax (CBPV)
V , W ::=||

split(V , x1 .x2 .M)
case0 (V )case(V , inj1 x1 .M1valuesvariableunit value
pairingvariant constructor
thunkcomputations
pattern matching: productvoidvariants

|
|
|
|||
|

, inj2 x2 .M2 )V!
return V
let x ← M in N
λx.M
M V
hM1 , M2 iprji Mforce
returnersequencing (monadic bind)function abstraction
function application
computation pairprojection||||
M, N ::=x()(V1 , V2 )inji V{M}

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

The lambda calculus with effects (mam)Operational semantics
Reduction frames and contexts
B ::= let x ← [ ] in N | [ ] V | prji [ ] basic frames
F ::= B
computation frames
C ::=evaluation context[ ]holeC[F [ ]]
layered frame
Beta reduction

Mβ M

0(β.×)
split((V1 , V2 ), x1 .x2 .M)(β.+) case(inji V , inj1 x1 .M1 , inj2 x2 .M2 )
(β.U)
{M}!
let x ← return V in M
(λx.M) V
prji hM1 , M2 i

(β.F )(β.→)(β.&)
Reduction

M

M0M
C[M]

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

β M

β M[V1 /x1 , V2 /x2 ]β Mi [V /xi ]β M
β M[V /x]β M[V /x]β Mi

0C[M 0 ]On the expressive power of user-defined effects

The lambda calculus with effects (mam)TypesE::=∅K::=| EffVal| CompE| Ctxt
A, B ::=
α| 1| A1 × A2| 0| A1 + A2
| UE CC , D ::=
FA| A→C| C1 & C2
Θ::= α1 , . . . , αnΓ, ∆ ::= x1 : A1 , . . . , xn : An

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

effects
pure effectkinds
effectsvaluesE -computations
environments
value types
type variable
unit
value products
empty
variant
thunkscomputation types
returners
functionscomputation products
type environments
environments
On the expressive power of user-defined effects

The lambda calculus with effects (mam)Denotational semantics
Standard, using sets and functions. Using Hermida’s [’93] lifting:

Theorem (adequacy)
Denotational equivalence implies contextural equivalence: for all
Θ; Γ `E P, Q : X , if ⟦P⟧ = ⟦Q⟧ then P ' Q.

Corollary (soundness and strong normalisation)
All well-typed closed ground returners reduce to a normal form: forall ; `∅ M : FG there exists some ; ` V : G such that
⟦return V ⟧ = ⟦M⟧ andM?

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

return VOn the expressive power of user-defined effects

Effect handlers

Syntax [K-Lindley-Oury’13]
M, N ::= . . .
computations| op V
operation call
| handle M with H
handling construct
H::=handlers{return x 7→ M}
return clause| H ] {op p k 7→ N}
operation clause(where op does not occur in H)

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Effect handlers

Operational semantics
Reduction frames and contexts···

F ::= . . .
computation frame| handle [ ] with H
H ::= [ ] | H[B[ ]]hoisting context

Beta reduction···(handle.F )handle (return V ) with H
where H return = λx.M(handle.op)handle H[op V ] with H

β M[V /x]βN[V /p, {λx.handle H[return x] with H}/k]
where H op = λp k.N and x ∈/ FV (H, H)

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Effect handlers
Types
E ::= . . .
effects| {op : A → B} ] E
arity assignment
K ::= . . .
kinds| Hndlrhandlers
0R ::= A E ⇒E Chandler types · · ·Computation typing

Θ; Γ `E M : C(op : A → B) ∈ E

Θ; Γ ` V : A···Θ; Γ `E op V : FBHandler typing

Θ; Γ ` H : R(Θ `k Γ : Ctxt, E : Eff, C : CompE )Θ; Γ `E M : FA

Θ; Γ `E 0 handle M with H : C(Θ `k Γ : Ctxt, R : Hndlr)

E = {opi : Ai → Bi }i
H = {return x 7→ M} ] {opi p k 7→ Ni }i[Θ; Γ, p : Ai , k : UE 0 (Bi → C ) `E 0 Ni : C ]iΘ; Γ, x : A `E 0 M : C0Θ; Γ ` H : A E ⇒E C

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

0Θ; Γ ` H : A E ⇒E C

On the expressive power of user-defined effects

Effect handlers

Denotational semantics
Using free monads for a signature. Using a folklore lifting [cf.
K’14] we have adequacy, soundness and strong normalisation.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Monadic reflection

Syntax [Filinski’94-10]
T::= mon(M, N) monads
M, N ::= . . .
computations| µ̂(N)
reflect| [N]Treify

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Monadic reflection

Operational semantics
Reduction frames and contexts
F ::= B | [[ ]]T
computation frames
H ::= [ ] | H[B[ ]] hoisting contexts · · ·Beta reduction···(reify)[return V ]T(reflect) [H[µ̂(N)]]T

β Nu VTβ Nb {N} {(λx.[H[return x]] )}for every T = mon(Nu , Nb ).

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Monadic reflection
Types
E ::= . . .
effects
E ≺ hα.C , N, Mi
layered monadMonad typingΘ `m T : E

Θ, α; `E Nu : α → C(Θ `k E : Eff)

Θ, α, β; `E Nb : UE C → UE (α → C [β/α]) → C [β/α]Θ `m mon(Nu , Nb ) : E ≺ hα.C , Nu , Nb i
Computation typing···Θ; Γ `E M : C(Θ `k Γ : Ctxt, E : Eff, C : CompE )Θ `m T : E ≺ hα.C , Nu , Nb iΘ; Γ `E ≺hα.C ,Nu ,Nb i N : AT

Θ; Γ `E [N]: C [A/α]Θ; Γ `E N : C [A/α]Caveats

Θ; Γ `E ≺hα.C ,Nu ,Nb i µ̂(N) : FA

Essentially top level monad declarations to avoid dependent types.
Requires type variables.
Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Monadic reflection

Denotational semantics
Partial semantics due to the invalidity of the monad laws.
Using TT -lifting, we have adequacy, soundness and strong
normalisation for terms whose semantics is defined.

Lemma (Finite denotation property)
For any tuple θ = hXα iα∈Θ of finite sets, if the types A and C
have well-defined denotations for θ, they denote finite sets.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Delimited control

SyntaxM, N ::= . . .
computations| S0 k.M
shift-0| hM|x.Ni
reset

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Delimited control

Operational semantics
Reduction frames and contexts···

F ::= . . .
computation frame| h[ ]|x.Ni
H ::= [ ] | H[B[ ]] hoisting context

Beta reduction···(reset) h(return V )|x.Mi

β M[V /x]

(shift0 )β M[λy .hH[return y ]|x.Ni/k]hH[S0 k.M]|x.Ni

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Delimited control

Types [Danvy and Filinski, sketched]E ::= . . . effects| E, A
Computation typing···Θ; Γ `E M : C

Θ; Γ, k : UE (B → FA) `E M : FA(Θ `k Γ : Ctxt, E : Eff, C : CompE )Θ; Γ `E ,A M : FAΘ; Γ, x : A `E N : C

Θ; Γ `E ,A S0 k.M : FB

Θ; Γ `E hM|x.Ni : C

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Delimited control

Denotational semantics
An adequate denotational semantics is an open problem.
Perhaps [Atkey’06]’s parameterised monads?

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Untyped translations

EFF==
MAM=DEL

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

MON

On the expressive power of user-defined effects

Typed translations

EFF
DEL

MAM
MON

EFF`
DEL `

MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Typed translations

EFF
DEL

MAM
MON

===EFF`

6∃
DEL `MAM `6∃

6∃
MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Typed translations

EFF
DEL

MAMMON===EFF`

6∃
DEL `

MAM `

6∃6∃
MON `

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Typed translations

EFF
DEL

MAM
MON==
EFF`
DEL `

MAM `

6∃MON `

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Richer types

EFF
DEL

MAM
MON+

EFF`
++

DEL `

MAM `+

MON `
EFF`
DEL `

MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Richer types

EFF
DEL

MAM
MON++

DEL `=+MAM `EFF`==+MON `EFF`
DEL `MAM `MON `Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Richer types

Conjectures
I Handlers + polymorphic arities express delimited control andmonadic reflection
I Delimited control + effect polymorphism express effecthandlers and monadic reflection.
I Parameterised monadic reflection and polymorphism express

effect handlers and delimited control.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects

Summary and conclusions

I Rigorous set-up for comparing user-defined effect abstractions.
I New and folklore macro translations.
I Inexpressivity result via a denotational invariant.
I Type system extensions accepting the translations.

Ohad Kammar <ohad.kammar@cs.ox.ac.uk>

On the expressive power of user-defined effects