Jeff Polakow wrote:
However, I don't see
how they are not equivalent (in the presence of impredicative
polymorphism) since I can write
derivations for both
forall b. (b -> String /\ Int) |- (forall b. b -> String) /\ Int
and
(forall b. b -> String) /\ Int |- forall b. (b -> String /\ Int)
in intuitionistic logic.
(Side-stepping your main point, rather, which I think Chris K answered
correctly)
This is a non-sequitur.
The fact that A |- B and B |- A does not make them the same type. It
makes them isomorphic types.
I can prove
(A \/ B) /\ C -| |- (A /\ C) \/ (B /\ C)
but that doesn't mean "(Either a b,c)" and "Either (a,c) (b,c)" are the
same haskell type.
It does mean they are isomorphic types, neglecting bottoms.
But isomorphic types are not the same type, for the type checker!
Jules
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
