[Haskell-cafe] Why this existential type could not work?

[Albert Y. C. Lai]

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 
user, client).

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 
chosen either.

The receiver of tail_example cannot choose b. He/She cannot ask what is 
chosen either.

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.