2 ms·

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