9 ms·

Forbidden Haskell Types

57 points by lelf 6y ago

siraben 6y ago
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 https://en.wikipedia.org/wiki/Occurs_check
netko_netkovic 6y ago
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 ?
- siraben 6y ago
  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/2016/07/typefun.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- fnord123 6y ago
  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.
- twic 6y ago
  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.
  - mightybyte 6y ago
    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.
  - centimeter 6y ago
    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.
- mrkeen 6y ago
  > 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/ https://patrickmn.com/software/the-haskell-pyramid/
- 000000000000010 6y ago
  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?
- gnulinux 6y ago
  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/Conat.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.
  - JadeNB 6y ago
    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.
    - 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?
sonofgod 6y ago
There was a part of me hoping that this would be "forbidden" in the sense of "forbidden knowledge". I was, surprisingly, not disappointed.
- twic 6y ago
  Ah, you wish to learn of the category which is not a category, H̦̻̺̮̝̹̲a̶̶̳͉͚̕ͅs̷͏̷̻͙͚̥͚̟̣ͅk͞͏̼̭ͅͅ.
OscarCunningham 6y ago
Now do 'T = T -> Bool'!
- cvoss 6y ago
  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 https://en.wikipedia.org/wiki/Curry%27s_paradox
batterseapower 6y ago
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/085307.html https://mail.haskell.org/pipermail/haskell-cafe/2010-October... The relevant keyword if you want to learn more here is "equirecursive types".
- carterschonwald 6y ago
  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)
  - batterseapower 6y ago
    Thanks for remembering :P

57 points by lelf 6y ago

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 https://en.wikipedia.org/wiki/Occurs_check

netko_netkovic 6y ago

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 ?

siraben 6y ago
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/2016/07/typefun.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
fnord123 6y ago
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.
twic 6y ago
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.
- mightybyte 6y ago
  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.
- centimeter 6y ago
  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.
mrkeen 6y ago
> 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/ https://patrickmn.com/software/the-haskell-pyramid/
000000000000010 6y ago
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?
gnulinux 6y ago
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/Conat.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.
- JadeNB 6y ago
  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.
  - 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?

sonofgod 6y ago

There was a part of me hoping that this would be "forbidden" in the sense of "forbidden knowledge". I was, surprisingly, not disappointed.

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

OscarCunningham 6y ago

Now do 'T = T -> Bool'!

cvoss 6y ago
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 https://en.wikipedia.org/wiki/Curry%27s_paradox

batterseapower 6y ago

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/085307.html https://mail.haskell.org/pipermail/haskell-cafe/2010-October... The relevant keyword if you want to learn more here is "equirecursive types".

carterschonwald 6y ago
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)
- batterseapower 6y ago
  Thanks for remembering :P