On Thu, 9 Oct 2003 19:13:48 -0700 (PDT) [EMAIL PROTECTED] 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. _______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
