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.