[Haskell-cafe] Re: Existential types (Was: Type vs TypeClass
apfelmus at quantentunnel.de
Thu Oct 25 04:06:51 EDT 2007
Dan Weston wrote:
> Thanks for the concise explanation. I do have one minor question though.
> > -+- A more useful example is
> > ∃a. Show a => a i.e. ∃a.(a -> String, a)
> > So, given a value (f,x) :: ∃a.(a -> String, a), we can do
> > f x :: String
> > but that's pretty much all we can do. The type is isomorphic to a simple
> > String.
> Don't you mean *epimorphic* instead of isomorphic (not that it matters)?
> For any existential type a of cardinality less than that of String, it
> is isomorphic, but if a = String, then by Cantor's theorem String ->
> String has a cardinality greater than String and cannot be isomorphic to
I do mean isomorphic. The point is that because we can't know what a
is, the only thing we will ever be able to do with it is plug it into
the function given. So, there is no difference in using the function
result in the first place.
To show that formally, one has to use _parametricity_ which is basically
the fact that the intuition about ∀ (and ∃) is true. For instance, the
intuition says that every function of type
∀a. a -> a
has to be the identity function (or _|_ but let's ignore that) because
it "may not look into a ". These quotes can be translated into
math-speak and are then called "parametricity".
More information about the Haskell-Cafe