Guarded Impredicativity

[Oliver Charles]

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