Definition
The delay monad on a type is the coinductive type given as the greatest fixed point of the endofunctor . It forms a monad
Equivalently, it is specified by the observation map
One often writes the two observable cases as
meaning respectively that the computation returns immediately or delays for one step and continues as .
An element of is a computation that either returns a value immediately or takes one more step before continuing.
Monad structure
The unit is given by immediate return:
The bind operation is defined corecursively by the equations
\mathrm{now}(x) \mathbin{\gg=} f &= f(x) \\ \mathrm{later}(d) \mathbin{\gg=} f &= \mathrm{later}(d \mathbin{\gg=} f). \end{aligned}$$ Thus delayed steps are preserved while the eventual returned value is passed to the next computation. ## Equality The delay monad carries an intensional notion of equality: the number of `later` steps matters. In particular, $$\mathrm{later}(\mathrm{now}(x)) \neq \mathrm{now}(x)$$ in general. For this reason, the delay monad records not only whether a computation terminates, but also how many delays occur before termination. ## Relation to partiality The delay monad is often used to encode [[Partial Function|partial functions]] in a total language. For extensional reasoning one compares it with the [[Partiality Monad]], which forgets finite delay information. In set-theoretic or extensional settings this is often described as quotienting the delay monad by a weaker equivalence, but in intensional type theory that description is only an intuition and requires additional work to recover the monad structure. ## Related Concepts - [[Partiality Monad]] - [[Monad]] - [[Partial Function]] - [[Bisimulation]] - [[capretta2005-partiality]]