4 ms·

Exactly. Parametricity is the killer feature of statically typed functional languages. This why it saddens me when Haskell and OCaml add features that weaken pa

Exactly. Parametricity is the killer feature of statically typed functional languages. This why it saddens me when Haskell and OCaml add features that weaken parametricity, like GADTs and type families.

js8 11y ago
Can you elaborate on your last sentence?
- catnaroek 11y ago
  Sorry, for some reason the “reply” link didn't appear below your post until after I had written my reply to Peaker. My reply to you is exactly the same: https://news.ycombinator.com/item?id=10668568 https://news.ycombinator.com/item?id=10668568
Peaker 11y ago
How do GADTs or type families weaken parametricity?
- catnaroek 11y ago
  Without either GADTs or type families, two types `Foo` and `Bar` with mappings `fw :: Foo -> Bar` and `bw :: Bar -> Foo` that compose in both directions to the identity, are “effectively indistinguishable” from one another in a precise sense. If you have a definition `qux :: T Foo`, for any type function `T` not containing abstract type constructors, you can construct `justAsQuxxy :: T Bar` by applying `fw` and `bw` in the right places. With either GADTs or type families, this nice property is lost.
  - lomnakkus 11y ago
    However, GADTs and TFs are completely opt-in, so it seems a bit of a stretch to construe this as a generally bad thing. IME it's not as if library authors are arbitrarily (i.e. for no good reason) using GADTs or TFs instead of plain old type parameters in their APIs.
    - catnaroek 11y ago
      Reflection, downcasts and assigning `null` to pointers are completely opt-in in Java too. With respect to type families, I'm probably being a little bit unfair. Personally, I don't have much against associated type families. (Although I think Rust handles them much more gracefully than GHC.) But very important libraries in the GHC ecosystem like vector and lens make extensive use of free-floating type families, which I find... ugh... I don't want to get angry.
      - lomnakkus 11y ago
        > Reflection, downcasts and assigning `null` to pointers are completely opt-in in Java too. No, they're not -- not in the same sense, at least. A GADT/TypeFamily is going to be visible in the API. None of the things you mentioned are visible in the API. There's a HUGE difference.
        catnaroek 11y ago
        > A GADT/TypeFamily is going to be visible in the API. Only works if you're never going to make abstract types. Which I guess is technically true in Haskell - the most you can do is hide the constructors of a concrete type. But the ability to make abstract types is very useful. Don't get me wrong, I love Haskell. It's precisely because I love Haskell that I hate it when they add features that make it as hard to reason about as C++. (Yes, there I said it - type families are morally C++ template specialization.)
        lomnakkus 11y ago
        If a type is abstract then the rest is up to the implementation of functions that operate on the data type -- and that could be hiding all kinds of nastiness like unsafePerformIO and the like. Yet, we usually don't care about that because it's an implementation detail. Am I missing some way to "abuse" GADTs/TFs to violate the abstraction boundary or something like that? (I seriously can't see what you think the problem is here. I mean, you can equally well abuse unsafeCoerce/unsafePerformIO to do all kinds of weird things to violate parametricity, so I don't see why GADTs/TFs should be singled out.)
  - Peaker 11y ago
    This nice property is not part of 'parametricity' as I know it, though.
  - tome 11y ago
    Are you saying something like "All type constructors are functorial Hask^n x Hask^op^m -> Hask"?
    - catnaroek 11y ago
      It's something weaker. Consider the groupoid of Haskell types and isomorphisms. Without GADTs and type families, all type constructors of kind `* -> *` are endofunctors on this groupoid. Note 1: And there are higher-kinded analogues, but I hope you get the idea from this. Note 2: There are also exceptions, like `IORef` and friends.

js8 11y ago

Can you elaborate on your last sentence?

catnaroek 11y ago
Sorry, for some reason the “reply” link didn't appear below your post until after I had written my reply to Peaker. My reply to you is exactly the same: https://news.ycombinator.com/item?id=10668568 https://news.ycombinator.com/item?id=10668568

Peaker 11y ago

How do GADTs or type families weaken parametricity?

catnaroek 11y ago
Without either GADTs or type families, two types `Foo` and `Bar` with mappings `fw :: Foo -> Bar` and `bw :: Bar -> Foo` that compose in both directions to the identity, are “effectively indistinguishable” from one another in a precise sense. If you have a definition `qux :: T Foo`, for any type function `T` not containing abstract type constructors, you can construct `justAsQuxxy :: T Bar` by applying `fw` and `bw` in the right places. With either GADTs or type families, this nice property is lost.
- lomnakkus 11y ago
  However, GADTs and TFs are completely opt-in, so it seems a bit of a stretch to construe this as a generally bad thing. IME it's not as if library authors are arbitrarily (i.e. for no good reason) using GADTs or TFs instead of plain old type parameters in their APIs.
  - catnaroek 11y ago
    Reflection, downcasts and assigning `null` to pointers are completely opt-in in Java too. With respect to type families, I'm probably being a little bit unfair. Personally, I don't have much against associated type families. (Although I think Rust handles them much more gracefully than GHC.) But very important libraries in the GHC ecosystem like vector and lens make extensive use of free-floating type families, which I find... ugh... I don't want to get angry.
    - lomnakkus 11y ago
      > Reflection, downcasts and assigning `null` to pointers are completely opt-in in Java too. No, they're not -- not in the same sense, at least. A GADT/TypeFamily is going to be visible in the API. None of the things you mentioned are visible in the API. There's a HUGE difference.
      - catnaroek 11y ago
        > A GADT/TypeFamily is going to be visible in the API. Only works if you're never going to make abstract types. Which I guess is technically true in Haskell - the most you can do is hide the constructors of a concrete type. But the ability to make abstract types is very useful. Don't get me wrong, I love Haskell. It's precisely because I love Haskell that I hate it when they add features that make it as hard to reason about as C++. (Yes, there I said it - type families are morally C++ template specialization.)
        lomnakkus 11y ago
        If a type is abstract then the rest is up to the implementation of functions that operate on the data type -- and that could be hiding all kinds of nastiness like unsafePerformIO and the like. Yet, we usually don't care about that because it's an implementation detail. Am I missing some way to "abuse" GADTs/TFs to violate the abstraction boundary or something like that? (I seriously can't see what you think the problem is here. I mean, you can equally well abuse unsafeCoerce/unsafePerformIO to do all kinds of weird things to violate parametricity, so I don't see why GADTs/TFs should be singled out.)
- Peaker 11y ago
  This nice property is not part of 'parametricity' as I know it, though.
- tome 11y ago
  Are you saying something like "All type constructors are functorial Hask^n x Hask^op^m -> Hask"?
  - catnaroek 11y ago
    It's something weaker. Consider the groupoid of Haskell types and isomorphisms. Without GADTs and type families, all type constructors of kind `* -> *` are endofunctors on this groupoid. Note 1: And there are higher-kinded analogues, but I hope you get the idea from this. Note 2: There are also exceptions, like `IORef` and friends.