Repository logo
 

The semantic marriage of monads and effects

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

Orchard, Dominic 
Petricek, Tomas 

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 lambda-calculus in terms of (strong) indexed monads which gives a one-to-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.

Description

Keywords

cs.PL, cs.PL

Journal Title

CoRR

Conference Name

Journal ISSN

Volume Title

Publisher

Publisher DOI

Publisher URL

Rights

All rights reserved