[Haskell-cafe] Restricted type classes

[Dan Doel]

On Wednesday 08 September 2010 11:17:43 pm wren ng thornton wrote:
>      -- | Proof that impure is not pure at E
>      fmap f (impure a)
>      == fmap f (E a a)
>      == E (f a) a
>      /= E (f a) (f a)
>      == impure (f a)

I don't believe your proof. The type of E is as follows:

  E :: a -> b -> E a

The free theorem given by that type is:

  forall f g x y. map f (E x y) = E (f x) (g y)

Setting y = x and g = f, we get:

  forall f x. map f (E x x) = E (f x) (f x)

So your above proof simply assumes that parametricity can be refuted. seq may 
cause that, but without seq, one would expect parametricity to hold, or at 
least not be refutable (unless there are other notorious examples I'm failing 
to remember; existential types aren't one).

I think the core of this is your ensuing discussion about equality versus 
equivalence. You seem to be advancing the notion that "equality" can only be 
used to refer to intensional equality. But intensional equality doesn't work 
very well for existential types, and up to extensional equality, the above 
should hold. Further, even with intensional equality, one wouldn't expect to 
be able to prove that E (f a) a /= E (f a) (f a). We should merely not be able 
to prove that  E (f a) a = E (f a) (f a).

Going back to free theorems, the theorem for:

  pure :: a -> T a

is

  map f . pure = pure . f

so any proposed counter example to that must be a refutation of parametricity 
for the language in question. I can believe that seq will produce refutations. 
Any proposal in which existential types do the same parametricity seems to me 
like it should be rethought.

-- Dan