'Forall' Polymorphism Question

[Andrew Kennedy]

Not quite.=20

"A definition is impredicative if it refers to a collection which
contains the object to be defined."
(see http://www.xrefer.com/entry/552390)

If you stratify a type system so that quantifiers only quantify over
things at a lower "stratum" then (I think) it is predicative (=3D not
impredicative). But you might have forall quantifiers at more than one
level in your system, as is the case in some formalizations of ML's
module system (Shao et al) where a predicative subset of the
impredicative F_\omega is used.

I'm also willing to be corrected!

- Andrew.

> -----Original Message-----
> From: Simon Peyton-Jones [mailto:simonpj@microsoft.com]=20
> Sent: Wednesday, October 31, 2001 12:20 PM
> To: Ashley Yakeley; Haskell List
> Subject: RE: 'Forall' Polymorphism Question
>=20
>=20
> Any system that allows a parametric type variable to
> be instantiated by a for-all type is called "impredicative",=20
> I think.  Example:  Maybe (forall a. a->a), or as you have=20
> below (m (forall a. a->a)).
>=20
> I don't understand all (well, any) of the details, but I=20
> understand that impredicative systems make type inference=20
> nigh impossible. I don't know any programming language that=20
> has impredicative types. Haskell certainly does not, nor any=20
> extension I know of.
>=20
> I'm willing to be corrected!
>=20
> Simon
>=20
> | -----Original Message-----
> | From: Ashley Yakeley [mailto:ashley@semantic.org]
> | Sent: 31 October 2001 10:14
> | To: Haskell List
> | Subject: 'Forall' Polymorphism Question
> |=20
> |=20
> | I note that GHC by default gives this type for "return id":
> |=20
> |     (return id) :: forall m a. (Monad m) =3D> m (a -> a)
> |=20
> | Wouldn't this be more general:
> |=20
> |     (return id) :: forall m. (Monad m) =3D> m (forall a. a -> a)
> |     (return return) :: forall m. (Monad m) =3D> m (forall m1 a.
> | (Monad m1)=20
> | =3D> a -> m1 a)
> |=20
> | ...?
> |=20
> | Is this something GHC could ever do, or are there good=20
> reasons why it
> | would never work in Haskell?
> |=20
> | --
> | Ashley Yakeley, Seattle WA
> |=20
> |=20
> | _______________________________________________
> | Haskell mailing list
> | Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
> |=20
>=20
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
>=20