'Forall' Polymorphism Question

Simon Peyton-Jones simonpj@microsoft.com
Wed, 31 Oct 2001 04:19:33 -0800

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!


| -----Original Message-----
| From: Ashley Yakeley [mailto:ashley@semantic.org]=20
| Sent: 31 October 2001 10:14
| To: Haskell List
| Subject: 'Forall' Polymorphism Question
| I note that GHC by default gives this type for "return id":
|     (return id) :: forall m a. (Monad m) =3D> m (a -> a)
| Wouldn't this be more general:
|     (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)
| ...?
| Is this something GHC could ever do, or are there good reasons why it=20
| would never work in Haskell?
| --=20
| Ashley Yakeley, Seattle WA
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell