Thank you very much, this kind of real world examples are very useful to us. Right now we are still researching what are the possibilities, but we'll try to cover this use case. Regards, Alejandro El lun., 15 jul. 2019 a las 16:21, Oliver Charles () escribió:

Hi Alejandro and other GHC devs,

I've just been pointed to this mailing list, and in particular the discussion on guarded impredicativity from the Haskell IRC channel. I wasn't following the list before, so sorry if this post comes out of threads!

I have a use case for impredicative polymorphism at the moment that comes out of some work on effect systems. Essentially, what I'm trying to do is to use reflection to thread around the interpretation of an effect. One encoding of effects is:

newtype Program signature carrier a = Program { ( forall x. signature x -> carrier x ) -> carrier a }

But for various reasons, this sucks for writing really high performant code.

My formulation is instead to change that -> to =>, and to carry around the signature interpretation with reflection. Thus we have something roughly along the lines of:

newtype Program s signature carrier a = Program ( forall m. Monad m => m a )

with

runProgram :: ( forall s. Reifies s ( signature :~> carrier ) => Program s signature carrier a ) -> carrier a

All is well and good, but from the user's perspective, it sucks to actually compose these things together, due to the `forall s` bit. For example, I can write:

foo = runError (runState s myProgram)

but I can't write

foo = runError . runState s $ myProgram

or

foo = myProgram & runState s & runError

I was excited to hear there is a branch with some progress on GI, but unfortunately it doesn't seem sufficient for my application. I've uploaded everything (it's just two files) here:

https://gist.github.com/ocharles/8008bf31c70d0190ff3440f9a5b0684d

Currently this doesn't compile, but I'd like it to (I'm using the `nix run` command mpickering shared earlier). The problem is Example.hs:55 - if you change the first . to a $, it type checks.

Let me know if this is unclear and I'm happy to refine it. I just wanted to show you:

* Roughly what I want to do * A concrete program that still fails to type check, even though I believe it should (in some ideal type checker...)

Regards, Ollie