3 ms·

> Parametricity is too good to give up. With the minor exception of reference cells (`IORef`, `STRef`, etc.), if two types are isomorphic, applying the same typ

by sclv 10y ago

> Parametricity is too good to give up. With the minor exception of reference cells (`IORef`, `STRef`, etc.), if two types are isomorphic, applying the same type constructor to them should yield isomorphic types. You know that's not what parametricity means, right? Like, at all? Here's a challenge. `foo :: forall a. a -> a` Now, by parametricity that should have only one inhabitant (upto iso). Use your claimed break in parametricity from type families and provide me two distinct inhabitants.

catnaroek 10y ago
> Now, by parametricity that should have only one inhabitant (upto iso). I can count at least three: `undefined`, `const undefined` and `id`. > Use your claimed break in parametricity from type families and provide me two distinct inhabitants. Does this count? Here Oleg constructs an inhabitant of False using just some means to case-analyze types (GADTs or type families): http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html
- wyager 10y ago
  Sounds like the problem there is that the Haskell typechecker assumes injectivity, not that it supports case-analysis.
  - catnaroek 10y ago
    The injectivity assumption isn't unjustified - type constructors are injective.
    - wyager 10y ago
      > The injectivity assumption isn't unjustified Strongly disagree. (+2) 3 == (+1) 4 implies neither (+2) == (+1) nor 3 == 4. So Fst goes out the window. (even 5) == (even 7) does not imply 5 == 7. >type constructors are injective. But type functions aren't, and that's what we want. I agree that it's misleading to have type functions look like type constructors syntactically.
      - catnaroek 10y ago
        The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.
- sclv 10y ago
  i should have specified "modulo bottom" because i somehow didn't cotton i was talking to someone more interested in pedantry than actual discussion. that said, constructing an inhabitant of false a _different_ way (when we can already write "someFalse = someFalse") is not particularly interesting, and again doesn't speak to parametricity in any direct way.

by sclv 10y ago

catnaroek 10y ago

> Now, by parametricity that should have only one inhabitant (upto iso). I can count at least three: `undefined`, `const undefined` and `id`. > Use your claimed break in parametricity from type families and provide me two distinct inhabitants. Does this count? Here Oleg constructs an inhabitant of False using just some means to case-analyze types (GADTs or type families): http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html

wyager 10y ago
Sounds like the problem there is that the Haskell typechecker assumes injectivity, not that it supports case-analysis.
- catnaroek 10y ago
  The injectivity assumption isn't unjustified - type constructors are injective.
  - wyager 10y ago
    > The injectivity assumption isn't unjustified Strongly disagree. (+2) 3 == (+1) 4 implies neither (+2) == (+1) nor 3 == 4. So Fst goes out the window. (even 5) == (even 7) does not imply 5 == 7. >type constructors are injective. But type functions aren't, and that's what we want. I agree that it's misleading to have type functions look like type constructors syntactically.
    - catnaroek 10y ago
      The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.
sclv 10y ago
i should have specified "modulo bottom" because i somehow didn't cotton i was talking to someone more interested in pedantry than actual discussion. that said, constructing an inhabitant of false a _different_ way (when we can already write "someFalse = someFalse") is not particularly interesting, and again doesn't speak to parametricity in any direct way.