[Haskell-cafe] Re: Pointfree rank-2 typed function

[Heinrich Apfelmus]

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