'Forall' Polymorphism Question

[Simon Peyton-Jones]

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
below (m (forall a. a->a)).

I don't understand all (well, any) of the details, but I understand
that impredicative systems make type inference nigh impossible.
I don't know any programming language that has impredicative types.
Haskell certainly does not, nor any extension I know of.

I'm willing to be corrected!

Simon

| -----Original Message-----
| From: Ashley Yakeley [mailto:ashley@semantic.org]=20
| 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.=20
| (Monad m1)=20
| =3D> a -> m1 a)
|=20
| ...?
|=20
| Is this something GHC could ever do, or are there good reasons why it=20
| would never work in Haskell?
|=20
| --=20
| Ashley Yakeley, Seattle WA
|=20
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
|=20