Guarded Impredicativity

Alejandro Serrano Mena trupill at gmail.com
Tue Jul 16 08:24:56 UTC 2019


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 (<ollie at ocharles.org.uk>)
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190716/93fc9425/attachment.html>


More information about the ghc-devs mailing list