On Wednesday 08 September 2010 11:17:43 pm wren ng thornton wrote:
-- | Proof that impure is not pure@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