<div dir="ltr"><div>Thank you very much, this kind of real world examples are very useful to us.</div><div>Right now we are still researching what are the possibilities, but we'll try to cover this use case.</div><div><br></div><div>Regards,</div><div>Alejandro<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">El lun., 15 jul. 2019 a las 16:21, Oliver Charles (<<a href="mailto:ollie@ocharles.org.uk">ollie@ocharles.org.uk</a>>) escribió:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Alejandro and other GHC devs,<br>
<br>
I've just been pointed to this mailing list, and in particular the<br>
discussion on guarded impredicativity from the Haskell IRC channel. I<br>
wasn't following the list before, so sorry if this post comes out of<br>
threads!<br>
<br>
I have a use case for impredicative polymorphism at the moment that<br>
comes out of some work on effect systems. Essentially, what I'm trying<br>
to do is to use reflection to thread around the interpretation of an<br>
effect. One encoding of effects is:<br>
<br>
newtype Program signature carrier a =<br>
  Program { ( forall x. signature x -> carrier x ) -> carrier a }<br>
<br>
But for various reasons, this sucks for writing really high performant code.<br>
<br>
My formulation is instead to change that -> to =>, and to carry around<br>
the signature interpretation with reflection. Thus we have something<br>
roughly along the lines of:<br>
<br>
newtype Program s signature carrier a =<br>
 Program ( forall m. Monad m => m a )<br>
<br>
with<br>
<br>
runProgram<br>
  :: ( forall s. Reifies s ( signature :~> carrier ) => Program s<br>
signature carrier a )<br>
  -> carrier a<br>
<br>
All is well and good, but from the user's perspective, it sucks to<br>
actually compose these things together, due to the `forall s` bit. For<br>
example, I can write:<br>
<br>
foo =<br>
  runError (runState s myProgram)<br>
<br>
but I can't write<br>
<br>
foo =<br>
  runError . runState s $<br>
  myProgram<br>
<br>
or<br>
<br>
foo =<br>
  myProgram<br>
    & runState s<br>
    & runError<br>
<br>
I was excited to hear there is a branch with some progress on GI, but<br>
unfortunately it doesn't seem sufficient for my application. I've<br>
uploaded everything (it's just two files) here:<br>
<br>
<a href="https://gist.github.com/ocharles/8008bf31c70d0190ff3440f9a5b0684d" rel="noreferrer" target="_blank">https://gist.github.com/ocharles/8008bf31c70d0190ff3440f9a5b0684d</a><br>
<br>
Currently this doesn't compile, but I'd like it to (I'm using the `nix<br>
run` command mpickering shared earlier). The problem is Example.hs:55<br>
- if you change the first . to a $, it type checks.<br>
<br>
Let me know if this is unclear and I'm happy to refine it. I just<br>
wanted to show you:<br>
<br>
* Roughly what I want to do<br>
* A concrete program that still fails to type check, even though I<br>
believe it should (in some ideal type checker...)<br>
<br>
Regards,<br>
Ollie<br>
</blockquote></div>