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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to