Hacker News new | ask | show | jobs
by sclv 3617 days 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.
1 comments
catnaroek 3617 days 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

link
sclv 3617 days 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.

link
wyager 3617 days ago
Sounds like the problem there is that the Haskell typechecker assumes injectivity, not that it supports case-analysis.
link
catnaroek 3617 days ago
The injectivity assumption isn't unjustified - type constructors are injective.
link
wyager 3616 days 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.

link
catnaroek 3616 days ago
The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.
link