Forbidden Haskell Types
semantic.org
semantic.org
The core reason why GHC didn't allow the naïve recursive definition in the first place is because the definition failed the occurs check[0], so using type families and explicitly labeling the types circumvents the problem.
The relevant keyword if you want to learn more here is "equirecursive types".
(For those who don’t know, the parent poster wrote and maintained a lot of nice Haskell Libs at one point)
Anyway, I often struggle to understand "what problem is author solving exactly", in terms "what is the benefit if we create such recursive type (or whatever else is the theme)" ? Somehow, there are lot of articles making some magic and showing "how can this be done in haskell", but at the end it is hard to understand "what is the benefit here, which real-life problem can I solve by using this technique, how to relate this with real world".
Please do not get me wrong, this not only about this post, but somehow very often in haskell - related posts. Or is it only me ?
In the same lecture, SPJ elaborates on how the usefulness of typeclasses weren't apparent in the beginning only to be discovered more later, in part through people playing.
[0] A History of Haskell
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/...
Haskell is best at solving problems that Haskell invented and other languages do not have.
E.g. haskell’s laziness forced early haskellers to think about denotational ways of managing effects, and ended up forcing them to invent modern monadic effect systems. Now, there are a lot of people who actually prefer explicit effect management over freely mixing effects and logic, and not just because they have stockholm syndrome.
Not just you.
Although maybe there’s something conceptually satisfying about defining bottom as the only type that refers to itself?
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:
something : T
something = just something
If that's not possible, it'd be isomorphic to natural numbers we know.
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?
I was, surprisingly, not disappointed.