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
it.
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".
Regards,
apfelmus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
