31 ms·

> 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.

• mkehrt 10y ago
  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.
  • wyager 10y ago
    >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 10y ago
      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.