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

[Peter Hercek]

apfelmus wrote:
> -+- Since ∀ and ∃ are clearly different, why does Haskell have only one 
> of them and even uses ∀ to declare existential types? The answer is the 
> following relation:
> 
>   ∃a.(a -> a) = ∀b. (∀a.(a -> a) -> b) -> b
> 
> So, how to compute a value  b  from an existential type ∃a.(a -> a)? 
> Well, we have to use a function  ∀a.(a -> a) -> b  that works for any 
> input type (a -> a) since we don't know which one it will be.
> 
> More generally, we have
> 
>   ∃a.(f a)    = ∀b. (∀a.(f a) -> b) -> b
> 
Is that by definition or (if it a consequence of the previous formula,
  is that one by definition)? Because it kind of makes sense but that
  does not mean much. If the formulas are not by defininition,
  any pointers to explanation why they are valid?
Why it is not only like this?
∃a.(f a)    = ∀b. (∀a.(f a) -> b)

> - Exercise 2: ∀ can be lifted along function arrows, whereas ∃ can't. 
> Explain why
> 
>   String -> ∀a.a   =   ∀a.String -> a
>   String -> ∃a.a  =/=  ∃a.String -> a
> 
> Since ∀ can always be lifted to the top, we usually don't write it 
> explicitly in Haskell.
> 
I do not see why forall can be lifted to the top of function arrows.
  I probably do not understand the notation at all. They all seem to be
  different to me.

  String -> ∀a.a
a function which takes strings a returns a value of all types together
  for any input string (so only bottom could be the return value?)

  ∀a.(String -> a)
a function which takes strings and returns a values of a type we want
  to be returned (whichever one it is; in given  contexts the return
  value type is the same for all input strings)

  String -> ∃a.a
a function taking strings and returning values of some type but we do
  not know anything about the type (in the same contexts and for each
  different input string the output type can be different)

  ∃a.(String -> a)
a function taking strings and returning values of some type; for each
  different input string there is the same output type

  Any pointers to explanations?

Thanks for one of the more informative posts on this subject.


Peter.