RAIRO - Theoretical Informatics and Applications (RAIRO: ITA)

Theoret. Informatics Appl. 36, 155-180 (2002)
DOI: 10.1051/ita:2002008

Semantics of value recursion for Monadic Input/Output

Levent Erkök¹, John Launchbury^{2, 1} and Andrew Moran²

¹ OGI School of Science and Engineering, OHSU; erkok@cse.ogi.edu.
² Galois Connections, Inc.

Abstract
Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell's IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this paper, we describe a semantics for a lazy language based on Haskell, supporting monadic I/O, mutable variables, usual recursive definitions, and value recursion. Our semantics is composed of two layers: a natural semantics for the functional layer, and a labeled transition semantics for the IO layer.

What is OpenURL?