[Haskell-cafe] Why this existential type could not work?
Albert Y. C. Lai
trebla at vex.net
Fri Aug 22 17:08:15 UTC 2014
On 14-08-21 03:08 AM, Magicloud Magiclouds wrote:
> Thank you. I think I need to understand the different means of forall
> when it at different positions.
Each value has a giver (aka creator, implementer) and a receiver (aka
It always and only comes down to: who chooses what to plug into the type
variable, the giver or the receiver. Exactly one of the two can choose.
data Head = HC (forall b. Maybe b)
head_example :: Head
head_example = HC (...)
The receiver of head_example can choose what b is. The giver of
head_example cannot choose.
How do I know? Because this is analogous to:
like_head_example :: forall b. Maybe b
like_head_example = ...
The giver of like_head_example cannot choose.
data Tail = forall b. TC (Maybe b)
tail_example :: Tail
tail_example = TC (...)
The giver of tail_example can choose what b is. The receiver cannot choose.
How do I know? Because the type of TC is
TC :: forall b. Maybe b -> Tail
The user of TC can choose. The user of TC is the giver of tail_example.
Now I talk about parametricity. Parametricity implies: the person who
cannot choose cannot ask either.
The giver of head_example cannot choose b. He/She cannot ask what is
The receiver of tail_example cannot choose b. He/She cannot ask what is
Non-generic Java lacks parametricity. Therefore, the person who cannot
choose can still ask what is chosen by instanceOf.
Generic Java has parametricity. Like Haskell, the person who cannot
choose cannot ask by instanceOf.
More information about the Haskell-Cafe