https://repl.it/repls/DeterminedJointTest
main.hs:43:1: error:
Parse error: module header, import declaration
or top-level declaration expected.
|
43 | something : T
| ^^^^^^^^^^^^^
So, in short it's just coinductive natural number type. I'd say it's very far from useless, I use Conat in Agda pretty often especially if you use other coinductive types.
That's why I find `repl.it` so handy. (No affiliation, and not an ad; it's just one service that I've found useful.) If I want to know something like this from any computer, I can just pop it over to their online REPL. I wasn't sure if it supported GHC pragmas, but it seems by this example that it does.
> So, in short it's just coinductive natural number type. I'd say it's very far from useless, I use Conat in Agda pretty often especially if you use other coinductive types.
Maybe I misunderstand the terminology. If it's true that one can't solve `something = just something`, then doesn't that mean that the type is inductive, not coinductive?
As to what is the practical implications of a Conat class? You can use it pretty much anywhere you use natural numbers, except it gives you less guarantees as it can be infinite.
To be honest, looking at the code again, I cannot be sure if it's coinductive or inductive. i.e. I'm unsure if you can construct:
which would be an infinite stream of `just`s.If that's not possible, it'd be isomorphic to natural numbers we know.