[Haskell-cafe] Re: Existential types (Was: Type vs TypeClass duality)

[apfelmus]

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