[Haskell-cafe] Re: Existential types (Was: Type vs TypeClass
duality)
Peter Hercek
peter at syncad.com
Wed Oct 24 14:26:24 EDT 2007
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.
More information about the Haskell-Cafe
mailing list