4 ms·
Cool! Yeah I've been lazy as I don't have Haskell setup on my work computer. So, in short it's just coinductive natural number type. I'd say it's very far from
by gnulinux 6y ago
Cool! Yeah I've been lazy as I don't have Haskell setup on my work computer.
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.
- JadeNB 6y ago> Cool! Yeah I've been lazy as I don't have Haskell setup on my work computer. 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?
- gnulinux 6y agoYes you're right it is inductive, I misread your comment as "it compiles" and once again got lazy and didn't check the link. :(
- JadeNB 6y agoNo, that's my fault, not yours. It originally did say it compiled, but that turned out to be some kind of error with repl.it, which appeared to be down as part of this outage (https://news.ycombinator.com/item?id=23875692 https://news.ycombinator.com/item?id=23875692). When I tried again, it didn't compile, and I thought I could sneak edit since you hadn't responded. Sorry!
- gnulinux 6y agoHaha no problem, thanks for your input!