Hacker News new | past | comments | ask | show | jobs | submit login
Forbidden Haskell Types (semantic.org)
57 points by lelf 23 days ago | hide | past | favorite | 23 comments



If anyone is confused by how the author uses "proof" in this article, they are referring to the Curry-Howard isomorphism that types represent propositions in a constructive logic and well-typed terms inhabiting those types can be considered as proofs. a :~: b is the type that a and b are "equal", i.e. they are the same type. the functions convert1 and convert2 witness the isomorphism between a and b.

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.

[0] https://en.wikipedia.org/wiki/Occurs_check


For another approach to making this work in Haskell, see this thread of mine from 2010: https://mail.haskell.org/pipermail/haskell-cafe/2010-October...

The relevant keyword if you want to learn more here is "equirecursive types".


Zomg it’s max!

(For those who don’t know, the parent poster wrote and maintained a lot of nice Haskell Libs at one point)


Thanks for remembering :P


Thank you for the article, it is great read. I'm trying to follow haskell-oriented blogs, some of them are cool to read, while more deeper ones are harder to follow (probably it is about me, not about author!).

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 ?


As Simon Peyton-Jones put it[0], Haskell is a language where people work as well as play. Sometimes there's an obvious practical use, sometimes it's not so obvious or may not exist at all. In this case, I as a Haskeller don't see a good use of "forbidden types", however, type families have many practical uses, see [1].

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/...


Jon Harrop, who is a troll, but on occasion quite funny, once wrote:

Haskell is best at solving problems that Haskell invented and other languages do not have.


This is very true, but I think there’s a good reason for it - using Haskell forces you to first address many fundamental issues that most languages just let you paper over. The issues still exist in other languages, but you can ignore them, and then years later wonder why so much software is ad-hoc and full of complicated, but preventable, bugs.

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.


LOL, I've been programming Haskell full-time professionally for 10 years and think that Haskell is very effective for practical tasks. But in this case I completely agree with you. That quote fits this thread perfectly.


In this case it looks like `T = Maybe T` is isomorphic to a coinductive natural number type, where `suc = just` and `zero = nothing`. You can see an example implementation of it in Agda: https://github.com/agda/agda-stdlib/blob/master/src/Codata/C...

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
which would be an infinite stream of `just`s.

If that's not possible, it'd be isomorphic to natural numbers we know.


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.


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.


> 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?


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. :(


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!


Haha no problem, thanks for your input!


I have the same question... if a type is used by the type-checker to verify the consistency of the data it’s annotating, then I don’t see how a recursive definition could provide anything new, other than potentially making type checking run forever...

Although maybe there’s something conceptually satisfying about defining bottom as the only type that refers to itself?


> 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 ?

Not just you.

https://patrickmn.com/software/the-haskell-pyramid/


It's not you. There's a lot of navel gazing and making people feel like they can't produce working software unless they have higher kind types preventing side effectual reordering for their hylomorphisms. And yet, life finds a way.


Now do 'T = T -> Bool'!


Curry's Paradox [0], for anyone wondering why this suggestion is entertaining and deserves its exclamation point.

[0] https://en.wikipedia.org/wiki/Curry%27s_paradox


There was a part of me hoping that this would be "forbidden" in the sense of "forbidden knowledge".

I was, surprisingly, not disappointed.


Ah, you wish to learn of the category which is not a category, H̦̻̺̮̝̹̲a̶̶̳͉͚̕ͅs̷͏̷̻͙͚̥͚̟̣ͅk͞͏̼̭ͅͅ.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: