3 ms·

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