The constructive lift monad

The constructive lift monad is the coinductive type $T(A) \equiv \nu\alpha.\; A + \alpha.$

The intuition is that an element of this type either tells you a value of type $A$, or tells you to compute some more and try again. Nontermination is modeled by the element which never returns a value, and always keeps telling you to compute some more.

Our goal is to construct a general fixed-point combinator $\mu(f : TA \to TA) : 1 \to TA$, which takes an $f$ and then produces a computation corresponding to the fixed point of $f$. To fix notation, we'll take the constructors to be:
$$
\begin{array}{lcl}
\mathsf{roll} & : & A + TA \to TA \\
\mathsf{unroll} & : & TA \to A + TA
\end{array}
$$
Since this is a coinductive type, we also have an unfold satisfying the following equation:
$$
\mathsf{unfold}(f : X \to A + X) : X \to TA \equiv \mathsf{roll} \circ (\mathit{id} + (\mathsf{unfold}\; f)) \circ f
$$
First, we will explicitly construct the bottom element, corresponding to the computation that runs forever, with the following definition:
$$
\bot : 1 \to TA \equiv \mathsf{unfold}(\mathsf{inr})
$$
This definition just keeps telling us to wait, over and over again. Now, we can define the fixed point operator:
$$
\begin{array}{l}
\mu(f : TA \to TA) : 1 \to TA \\
\mu(f) \equiv (\mathsf{unfold} (\mathsf{unroll} \circ f)) \circ \bot
\end{array}
$$
What this does is to pass bottom to $f$. If $f$ returns a value, then we're done. Otherwise, $f$ returns us another thunk, which we can pass back to $f$ again, and repeat.

Of course, this is exactly the intuition behind fixed points in domain theory. Lifting in domains is usually defined directly, and I don't know who invented the idea of defining it as a coinductive type. I do recall a 1999 paper by Martin Escardo which uses (a slight variant of) it, and he refers to it as a well-known construction in metric spaces, so probably the papers from the Dutch school of semantics are a good place to start the search. This construction has seen a renewed burst of interest in the last few years, since it offers a relatively convenient way to represent nonterminating functions in dependent type theory. It's also closely related to step-indexed models in operational semantics, since, given a terminating element of the lift monad, you can compute how many steps it takes to return a value.

It's stuff like this that makes me say I can't tell the difference between operational and denotational semantics any more.