Kleene Monads: Handling Iteration in a Framework of Generic Effects

Abstract. Monads are a well-established tool for modelling various computational effects. They form the semantic basis of Moggi’s computational metalanguage, the metalanguage of effects for short, which made its way into modern functional programming in the shape of Haskell’s do-notation. Standard computational idioms call for specific classes of monads that support additional control operations. Here, we introduce Kleene monads, which additionally feature nondeterministic choice and Kleene star, i.e. nondeterministic iteration, and we provide a metalanguage and a sound calculus for Kleene monads, the metalanguage of control and effects, which is the natural joint extension of Kleene algebra and the metalanguage of effects. This provides a framework for studying abstract program equality focussing on iteration and effects. These aspects are known to have decidable equational theories when studied in isolation. However, it is well known that decidability breaks easily; e.g. the Hor...

• Type: Conference
• Year: 2009
• Where: CALCO
• Authors: Sergey Goncharov, Lutz Schröder, Till Mossakowski
• Keywords: CALCO 2009, Kleene, Kleene Monads, Mathematics, Metalanguage