Essentially, to get a nonterminating, program, your top level function needs to ...

wyager · on Oct 6, 2016

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

Huh?

    inf = Cons 1 inf

mkehrt · on Oct 6, 2016

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.