Any system that allows a parametric type variable to be instantiated by a for-all type is called "impredicative", 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:[EMAIL PROTECTED]] | 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) => m (a -> a) | | Wouldn't this be more general: | | (return id) :: forall m. (Monad m) => m (forall a. a -> a) | (return return) :: forall m. (Monad m) => m (forall m1 a. | (Monad m1) | => a -> m1 a) | | ...? | | Is this something GHC could ever do, or are there good reasons why it | would never work in Haskell? | | -- | Ashley Yakeley, Seattle WA | | | _______________________________________________ | Haskell mailing list | [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell | _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
