One nice use of the "general recursion monad" idea is "mtac" ( http://plv.mpi-sws.org/mtac/ ), a "tactic language" for Coq. This allows meta-programming, to calculate what a value/function/etc. should be, which is really useful for proof objects (i.e. values which are required for compilation, but have no effect on runtime computation).

A tactic language doesn't need to be total, since it's only run at compile-time, so no errors can leak into the resulting proof/program. The worst that can happen is the compiler hangs.

Coq comes with "ltac", which is a horrible imperative language that leads to very fragile proofs. On the other hand, mtac is just Coq's normal, total FP language ("gallina"). A monad is used to wrap up general recursion, so that gallina can be used un-changed.

During compilation, these monadic values are forced, which either leads to a value or causes the compiler to hang. This is a really nice compromise, since you can write Haskell-style FP code which "obviously terminates", without having to prove that it terminates, you still have access to all of the nice dependent type machinery, and the end result (the program, not the meta-program) is guaranteed to be total (unlike, say, an Idris function which turns off the totality checker).

> You would of course need to factor out the outer-loop to do this

What are you referring to? Data/codata checking works with local type inference.

Essentially, to get a nonterminating, program, your top level function needs to take a piece of codata to corecurse over to run indefinitely. Since you can't actually write a program that takes no arguments that produces an infinite piece of data, all programs must terminate.

>Since you can't actually write a program that takes no arguments that produces an infinite piece of data

Huh?

    inf = Cons 1 inf

Hm, you may be right. I though that was going to violate:

> Each recursive function call must be on a syntactic subcomponent of its formal parameter.

But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it:

> Ordinary recursion is not legal over codata, because it might not terminate.