The semantic marriage of monads and effects
Extended abstract
Dominic Orchard

Tomas Petricek

Alan Mycroft

arXiv:1401.5391v1 [cs.PL] 21 Jan 2014

Computer Laboratory, University of Cambridge
{firstname.lastname}@cl.cam.ac.uk

Abstract
Wadler and Thiemann unified type-and-effect systems with monadic
semantics via a syntactic correspondence and soundness results
with respect to an operational semantics. They conjecture that a
general, “coherent” denotational semantics can be given to unify
effect systems with a monadic-style semantics. We provide such a
semantics based on the novel structure of an indexed monad, which
we introduce. We redefine the semantics of Moggi’s computational
λ-calculus in terms of (strong) indexed monads which gives a oneto-one correspondence between indices of the denotations and the
effect annotations of traditional effect systems. Dually, this approach yields indexed comonads which gives a unified semantics
and effect system to contextual notions of effect (called coeffects),
which we have previously described [9].
Previously, Wadler and Thiemann established a syntactic correspondence between type-and-effect systems and the monadic semantics approach by annotating monadic type constructors with
the effect sets of the type-and-effect system [10]. They established
soundness results between the effect system and an operational
semantics, and conjectured a “coherent semantics” of effects and
monads in a denotational style. One suggestion was to associate to
each effect set σ a different monad T σ .
We take a different approach to a coherent semantics, unifying
effect systems with a monadic-style semantics in terms of the novel
notion of indexed monads, which generalises monads.1
Indexed monads

Indexed monads comprise a functor
T : I → [C, C]

(i.e., an indexed family of endofunctors) where I is a strict
monoidal category (I, ⊗, 1) and T is a lax monoidal functor, mapping the strict monoidal structure on I to the strict monoid of
endofunctor composition ([C, C], ◦, IC ).
The operations of the lax monoidal structure are thus:
.

η1 : IC −
→ T1

.

µF,G : TF ◦ TG −
→ T(F ⊗ G)

1 Note this differs to Johnstone’s notion of indexed monad in the context
of topos theory, the indexed monads seen in the work of McBride [4], and
parameterised monads by Atkey [1].

These lax monoidal operations of T match the shape of the regular
monad operations. Furthermore, the standard associativity and unitality conditions of the lax monoidal functor give coherence conditions to η1 and µF,G which are analogous to the regular monad
laws, but with added indices, e.g., µ1,G ◦ (η1 )TG = idTG .
Example (Indexed exponent/reader monad) Given the monoid
(P(X), ∪, ∅) (for some set X), the indexed family of Set endofunctors where TXA = X ⇒ A (with ⇒ denoting exponents)
and TXf = λk.f ◦ k, is an indexed monad with:
η∅ a = λx.a
µF,G k = λx.(k (x − (G − F ))) (x − (F − G))
where x : F ∪ G and k : F ⇒ (G ⇒ A) thus k takes two
arguments, the F -only subset of x (written x−(G−F )) and the Gonly subset of x (written x − (F − G)) where (−) is set difference.
The indexed reader monad models the composition of computations with implicit parameters, where the required implicit parameters of subcomputations are combined in their composition.
This provides a more refined model to the notion of implicitly parameterised computations than the traditional reader monad, where
implicit parameters are uniform throughout a computation and its
subcomputations.
Relating indexed monads and monads Indexed monads collapse
to regular monads when I is a single-object monoidal category.
Thus, indexed monads generalise monads.
Note that indexed monads are not indexed families of monads.
That is, for all indices F ∈ obj(I) then TF may not be a monad.
An indexed monadic semantics for λc We extend indexed monads to strong indexed monads, with an indexed strength operation
(and analogous laws to usual monadic strength):
(τF )A,B : (A × TF B) → TF (A × B)
We replay Moggi’s categorical semantics for the computational λcalculus (λc ) [5], replacing the regular strong monad operations
with the analogous operations of an indexed strong monad. This
provides an indexed semantics. For example, the semantics of λabstraction becomes the following (where we write the parameter
to T as a subscript for notational clarity below):
JΓ, x : σ ⊢ e : τ K = g : JΓK × JσK → TF τ
JΓ ⊢ λx : σ.e : σ → τ K = η1 ◦ (Λg) : JΓK → T1 (σ ⇒ TF τ )
(where for g : A × B → C, Λg : A → (B ⇒ C)).
Coherent semantics In this indexed monadic semantics, the indices of denotations have exactly the same structure as the effect annotations of a traditional effect system (with judgments
Γ ⊢ e : τ, F for an expression e with effects F ).
We unify effect systems with indexed monadic semantics, so
that JΓ ⊢ e : τ, F K : JΓK → TF Jτ K, taking obj(I) as the effect

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2014/1/22

sets of a traditional effect system, with the strict monoidal structure
on I provided by the effect lattice, with 1 = ⊥ and ⊗ = ⊔, and
morphisms f : X → Y in I iff X ⊑ Y in the effect lattice.
Pleasingly, the usual equational theory for λc (such as β-equality
for values) follows directly from the strong indexed monad axioms.
The morphism mapping of T defines natural transformations
.
ιX,Y : TX −
→ TY when X ⊑ Y which provides a semantics
to sub-effecting:
(sub)

JΓ ⊢ e : τ, F ′ K = g : JΓK → TF ′ Jτ K F ′ ⊑ F
JΓ ⊢ e : τ, F K = ιF ′ ,F ◦ g : JΓK → TF Jτ K

For a particular notion of effect, the indexed strong monad can be
defined such that the propagation of effect annotations in an effect
system maps directly to the semantic propagation of effects. For
example, for memory effects the functor can be made more precise
with respect to the effect, e.g., T{read ρ : τ } A = τ → A and
T{write ρ : τ } A = A × τ (note: the latter is not itself a monad).
Therefore strong indexed monads neatly unify a (categorical)
semantics of effects with traditional effect systems. The indexed
monad structure arises simply from the standard category theory
construction of lax monoidal functors, where T preserves the strict
monoidal structure of I in [C, C]. Crucially, indexed monads are
not an indexed family of monads (contrasting with Wadler and
Thiemann’s original conjecture).
In context We argue our approach provides an intermediate solution between the traditional monadic approach (which does not
couple annotations of an effect system to semantics) and algebraic
effect theories (see, e.g., Kammar and Plotkin [3]).
Our approach differs somewhat to Atkey’s parameterised monads, defined for T : S×S op → [C, C]. Our indexed monad structure
has a more systematic derivation, arising from the strict monoidal
preservation of the lax monoidal functor. This technique can be applied to derive coherent semantic structures/effect system pairs for
other notions of computation.
Effect systems traditionally define effect annotations in terms
of sets with composition via set union [2]. This has the additional
property that combining effect annotations is symmetric (due to
commutativity of union). The more general structure of a monoid
here, also used by Nielson and Nielson [6], provides an opportunity
for generating effect information that records the order of effects.
Extending the approach to other notions We apply the same
technique used to derive indexed monads to give richer effect systems/semantics in two ways.
1. A strict colax monoidal functor D : I → [C, C] gives rise to
the dual notion of indexed comonads, which we have previously
shown to provide the notion of a coeffect system (analysing contextual requirements) and a semantics for contextual program
effects [7, 9].
For a monoid (I, ⊗, 1), indexed comonads have the colax operations:
.

ε1 : D1 −
→ IC

.

δF,G : D(F ⊗ G) −
→ DF ◦ DG

Interestingly, indexed comonads seem much more useful than
comonads since they relax the usual shape preservation property of comonads.
Example (Indexed partiality comonad) For the boolean conjunction monoid ({f , t}, ∧, t), the following indexed family of
endofunctors is an indexed comonad:
D fA = 1
D tA = A
D f f = !A
D tf = f

a dependently-typed partiality construction DA = 1 + A.
Note however, that DA = 1 + A is not a comonad since
ε : DA → A is not well defined. The indexed partiality
comonad encodes the notion of a partial context/input to a
computation, and has been previously shown to give a simple
liveness analysis coupled with a semantics that embeds the
notion of dead-code elimination [9].
Coeffect systems differ to effect systems in their treatment of
λ-abstraction where, for coeffect judgments Γ?F ⊢ e : τ
(meaning expression e has contextual requirements F ):
(abs)

Γ, x : σ?F ∨ F ′ ⊢ e : τ
F′

Γ?F ⊢ λx.e : σ −→ τ
Reading this rule top-down, the coeffects of the function body
are split between immediate contextual requirements and latent
F′

requirements (written −→). Thus, with respect to contextual
requirements, λ-abstraction is not “pure” as it is for effects.
In an indexed semantics unifying a coeffect system with an
indexed comonad, the semantics of λ-abstraction requires the
additional structure of an indexed (semi-)monoidal comonad
with the operation:
(mF,G )A,B : DF A × DG B → DF ∨G (A × B)
where ∨ is an associative binary operation over I.
2. Nielson and Nielson defined a more general effect system with
a richer algebraic effect structure, separating the traditional approach of an effect lattice into operations for sequential composition, alternation, and fixed-points [6]. Relatedly on the semantic side, the structure of a joinad has been proposed to give
the semantics of sequencing, alternation and parallelism in an
effectful language [8], adding additional monoidal structures to
a monad. Similarly to indexed monads, joinads can be generalised to indexed joinads, giving a correspondence between the
richer effect systems of Nielson and Nielson and a joinad-based
semantics. This is future work.

References
[1] ATKEY, R. Parameterised notions of computation. In Proceedings of
the Workshop on Mathematically Structured Functional Programming
(2006), Cambridge Univ Press.
[2] G IFFORD , D. K., AND L UCASSEN , J. M. Integrating functional and
imperative programming. In Proceedings of Conference on LISP and
func. prog. (1986), LFP ’86.
[3] K AMMAR , O., AND P LOTKIN , G. D. Algebraic foundations for
effect-dependent optimisations. In ACM SIGPLAN Notices (2012),
vol. 47, ACM, pp. 349–360.
[4] M C BRIDE, C. Functional pearl: Kleisli arrows of outrageous fortune. Journal of Functional Programming (to appear).
[5] M OGGI , E. Computational lambda-calculus and monads. In Logic
in Computer Science, 1989. LICS’89, Proceedings., Fourth Annual
Symposium on (1989), IEEE, pp. 14–23.
[6] N IELSON , F., AND N IELSON , H. Type and effect systems. Correct
System Design (1999), 114–136.
[7] O RCHARD , D. Programming contextual computations. PhD thesis,
University of Cambridge, 2013. (To appear).
[8] P ETRICEK , T., M YCROFT, A., AND S YME , D. Extending Monads
with Pattern Matching. In Proceedings of Haskell Symposium (2011),
Haskell 2011.
[9] P ETRICEK , T., O RCHARD , D. A., AND M YCROFT, A. Coeffects:
Unified static analysis of context-dependence. In ICALP (2) (2013),
pp. 385–397.

with εt a = a, δt,t a = a, and δX,Y a = 1 when X = f
and/or Y = f . The indexed partiality comonad is essentially

[10] WADLER , P., AND T HIEMANN , P. The marriage of effects and
monads. ACM Trans. Comput. Logic 4 (January 2003), 1–32.

2

2014/1/22

