Simon Peyton-Jones wrote:
| Are there workarounds for uses of impredicative types, or do we lose the | ability to express certain programs as a result?
There's usually a workaround. I include the msg I sent below.
I tried to use impredicative polymorphism once to create polymorphic values inside a monad, similar to the following (silly) example foo :: IO (∀a. a -> a) foo = do ref <- newIORef id -- ref :: IO (∀a. a -> a) readIORef ref (Fortunately, it turned out that this was not what I needed anyway.) Generally, it seems to me that all polymorphically typed EDSLs require impredicative polymorphism. After all, they are usually embedded with some kind of functor F (= Expr, IO, Parser, ...) and polymorphically typed means that you want types like F (∀a. a :~> a) and so on. Of course, we don't have (m)any examples of polymorphically typed DSLs yet, but it would be handy to have support for impredicativity in GHC if someone stumbles upon a useful one. Regards, apfelmus -- http://apfelmus.nfshost.com