[Haskell-cafe] How to understand the 'forall' ?

[Daniil Elovkov]

Eugene Kirpichov wrote:
> 
> P.S. I tried to write up the difference between datatype and function
> declarations in this respect, but my explanations turned into a mess,
> so I erased them in the hope that someone will explain it better than
> me.
> 

Hello Eugene, I'll give it a try.

In a non-constructive way: there seems to be nothing in common between those.

In a constructive way:

Datatype forall is called existential quantification, forall in function signature is called first-class polymorphism, if I'm not mistaken.

Existential is a perfect word, because it really is
data S = exists a. Show a => S [a].
The meaning is that within a given instance of S there lies some value of some particular type (a type exists). It's not any, it's some particular type. It can be either [Int], or forall a. Show a => [a], for example [], or some other type, but it exists.

With first-class polymorphism there's nothing that lies somewhere. Nothing of some particular type. The function whose type is forall ... is applicable to any type within the given bounds. And even this function itself doesn't lie anywhere, since it's a parameter. I think it can be considered just a way to impact the scope of type parameters within the signature, roughly speaking.

Not sure it this is useful, but

data S = ∃x. S x
f :: ∀x. x -> (∀y. y -> t) -> t

and just in case, the data constructor S doesn't use first-class polymorphism since its type is just
S :: ∀x. x -> S

I know that you perfectly understand it, I just tried to word it :)

--
Daniil Elovkov