From Monads to Effects and Back

The combination of monads and effects leads to a clean and easy to reason about programming paradigm. Monadic programming is easy to reason about, but can be cumbersome, as it requires explicit lifting and binding. In this paper, we combine monads and effects within a single programming paradigm: we use monads to define the semantics of effect types, and then, use the effects to program with those monads. We implemented an extension to the effect type system of Koka [15] with user defined effects. We use a type-directed translation to automatically lift effectful into monadic programs, by inserting bind- and unit operations.

• Type: Journal
• Year: 2016
• Where: PADL
• Authors: Niki Vazou, Daan Leijen
• Keywords: PADL 2016, Programming Languages