On Thu, 9 Oct 2003 19:13:48 -0700 (PDT) oleg@pobox.com wrote:
It was derived with a simple transformation: composing (rowv -> a) with (a->String) to eliminate the existential type a.
It seems there is a pattern here. When we write data Foo a b = forall ex. Foo <something1> <something2> <something3>
with ex unconstrained, then one of <something> must be a function F(a,b) -> ex and another something is a function ex -> G(a,b). Here F(a,b) is some expression that includes ground types, a, b -- but not ex. Indeed, otherwise we have no way to convert something into ex and to get anything out. The third something is perhaps a transformer ex -> H(a,b) -> ex. It seems therefore we are guaranteed that there is always a composition of <something>s that does not include ex. Therefore, instead of carrying original <something>, we can carry the compositions, and get rid of the existential quantification.
It seems that (g.f) :: i -> o is equivalent to stating exists c. f:: (i->c) ^ g::(c->o) or, in the Haskell type language data P i o = forall c. P (i->c) (c->o) P f g
As always, the wiki has some remarks about this, http://www.haskell.org/hawiki/ExistentialTypes.