5 ms·

How do GADTs or type families weaken parametricity?

by Peaker 11y ago

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.

How do GADTs or type families weaken parametricity?

by Peaker 11y ago

How do GADTs or type families weaken parametricity?

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.