By analogy: a Haskell (Agda) program is pure (total), but that doesn't mean that it can't do IO (general recursion) -- it just means you have to annotate that fact at the type level
-
-
Technically there is no `main :: GR String` in Agda, but it would not hurt any of Agda's goals to have that.
2 replies 0 retweets 0 likes -
IO is coinductive in Agda so you do in fact have the ability to run a GR program.
3 replies 2 retweets 11 likes -
Replying to @anormalform @edwinbrady and
General recursion is bigger than coinduction + induction. Trivially, `while (true);` exists, and also an infinite set of more complex programs that are isomorphic to it. Though, I will accept the argument that all *useful* GR is either inductive or coinductive. :-)
1 reply 0 retweets 2 likes -
Replying to @djspiewak @edwinbrady and
I don't see the issue? `main` having a coinductive IO type is the escape hatch that allows you to run a program (e.g. `while (true);`) until you either get an answer or a user interrupt.
1 reply 0 retweets 2 likes -
Replying to @anormalform @edwinbrady and
But how do you encode `while (true);` as a coterminating process? I suppose you can unfold into Unit. I wonder if that works universally?
1 reply 0 retweets 0 likes -
Replying to @djspiewak @anormalform and
Presumably the constructor emitted by each step of the coinductive loop would have a "Skip" option that does nothing, corresponding to one iteration of the no-op while loop
1 reply 0 retweets 0 likes -
Replying to @GabrielG439 @anormalform and
Encodings like that make me honestly wonder if there is a difference, formal or practical, between general recursion and evaluated coinduction.
1 reply 0 retweets 0 likes -
Replying to @djspiewak @anormalform and
There is a difference when you want to mechanically prove whether two coinductive programs are equivalent. With coinduction you can prove equivalence safely via bisimulation if they have the same pattern of Skip constructors, whereas with general recursion you can't
1 reply 0 retweets 1 like -
Replying to @GabrielG439 @djspiewak and
It's probably worth noting that you can obviously run rule 110 indefinitely from a productive program. If nothing else, it's productive because you print out the state of the world plus a newline on each iteration. From this perspective, skip as an IO action makes sense.
1 reply 0 retweets 2 likes
A big difference for me is that coinduction allows you to be precise about what promises you're making, and where. I could have a type that represents GR programs, and that'd might be fine, or I might want something more specific (as I probably would for a server).
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.