> Am I right in thinking that the following holds ?
> 
> polymorphic  = has type 'a  = for all
> monomorphic  = has type '_a = exists
> 
> Here '=' stands for 'equal in spirit'.
> 
> 
> Toby Moth

Yes you are 'right in spirit': more precisely '_a means an unknown
type, that should be precised by further constraints or computations
(as are unknowns in math). There is no quantifier in a type with '_a,
as opposed to existential types (type scheme with existential
quantifier in fact).

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/