Using existential types

[Derek Elkins]

On Thu, 9 Oct 2003 19:13:48 -0700 (PDT)
oleg at 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.