News for hackers. Stuff that matters.

A comment on Forbidden Haskell Types. Parent comment

Re:Forbidden Haskell Types by JadeNB on Friday July 17, 2020 @05:29PM (#23875886)
No need to wonder! I just grabbed the example code from the post and stuck the extra `something` in it:

    https://repl.it/repls/DeterminedJointTest
(I think that's the right sharing link, although repl.it seems to be down right now.) It doesn't compile:

     main.hs:43:1: error:
        Parse error: module header, import declaration
        or top-level declaration expected.
       |
    43 | something : T
       | ^^^^^^^^^^^^^
Maybe I had the syntax wrong.
[ Parent | on HN ]
Re:Forbidden Haskell Types by gnulinux on Friday July 17, 2020 @05:37PM (#23876087)
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.

[ Parent | on HN ]
Re:Forbidden Haskell Types by JadeNB on Friday July 17, 2020 @06:30PM (#23876737)
> 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?

[ Parent | on HN ]
Re:Forbidden Haskell Types by gnulinux on Friday July 17, 2020 @06:52PM (#23876957)
Yes you're right it is inductive, I misread your comment as "it compiles" and once again got lazy and didn't check the link. :(
[ Parent | on HN ]
Re:Forbidden Haskell Types by JadeNB on Friday July 17, 2020 @08:05PM (#23877557)
No, 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). When I tried again, it didn't compile, and I thought I could sneak edit since you hadn't responded. Sorry!
[ Parent | on HN ]
Re:Forbidden Haskell Types by gnulinux on Monday July 20, 2020 @09:57AM (#23897861)
Haha no problem, thanks for your input!
[ Parent | on HN ]