Guarded Impredicativity

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Guarded Impredicativity

Oliver Charles-3
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
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Alejandro Serrano Mena
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 (<[hidden email]>) 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

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Ryan Scott
In reply to this post by Oliver Charles-3
I have another interesting application of guarded impredicativity that
I want to bring up. Currently, GHC #16140 [1] makes it rather
inconvenient to use quantified constraints in type synonyms. For
instance, GHC rejects the following example by default:

    type F f = (Functor f, forall a. Eq (f a))

This is because F is a synonym for a constraint tuple, so mentioning a
quantified constraint in one of its arguments gets flagged as
impredicative. In the discussion for #16140, we have pondered doing a
major rewrite of the code in TcValidity to permit F. But perhaps we
don't need to! After all, the quantified constraint in the example
above appears directly underneath a type constructor (namely, the type
constructor for the constraint 2-tuple), which should be a textbook
case of guarded impredicativity.

I don't have the guarded impredicativity branch built locally, so I am
unable to test if this hypothesis is true. In any case, I wanted to
mention it as another motivating use case.

Ryan S.
-----
[1] https://gitlab.haskell.org/ghc/ghc/issues/16140
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Artem Pelenitsyn
Hello Ryan,

Your example seems to work out of the box with the GI branch.

With the oneliner Matthew posted before:
It is really easy to check. Also, I didn't see anywhere mentioned that one need to provide -XImpredicativeTypes. The whole example, therefore, is:

{-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}                                                                                                                                                                                                                        
module M where
type F f = (Functor f, forall a. Eq (f a))

--
Best, Artem

On Fri, 19 Jul 2019 at 09:18, Ryan Scott <[hidden email]> wrote:
I have another interesting application of guarded impredicativity that
I want to bring up. Currently, GHC #16140 [1] makes it rather
inconvenient to use quantified constraints in type synonyms. For
instance, GHC rejects the following example by default:

    type F f = (Functor f, forall a. Eq (f a))

This is because F is a synonym for a constraint tuple, so mentioning a
quantified constraint in one of its arguments gets flagged as
impredicative. In the discussion for #16140, we have pondered doing a
major rewrite of the code in TcValidity to permit F. But perhaps we
don't need to! After all, the quantified constraint in the example
above appears directly underneath a type constructor (namely, the type
constructor for the constraint 2-tuple), which should be a textbook
case of guarded impredicativity.

I don't have the guarded impredicativity branch built locally, so I am
unable to test if this hypothesis is true. In any case, I wanted to
mention it as another motivating use case.

Ryan S.
-----
[1] https://gitlab.haskell.org/ghc/ghc/issues/16140
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Ryan Scott
Good to know. Thanks for checking!

Ryan S.

On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn
<[hidden email]> wrote:

>
> Hello Ryan,
>
> Your example seems to work out of the box with the GI branch.
>
> With the oneliner Matthew posted before:
> nix run -f https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz \
> ghc-head-from -c ghc-head-from \
> https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz
> It is really easy to check. Also, I didn't see anywhere mentioned that one need to provide -XImpredicativeTypes. The whole example, therefore, is:
>
> {-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}
> module M where
> type F f = (Functor f, forall a. Eq (f a))
>
> --
> Best, Artem
>
> On Fri, 19 Jul 2019 at 09:18, Ryan Scott <[hidden email]> wrote:
>>
>> I have another interesting application of guarded impredicativity that
>> I want to bring up. Currently, GHC #16140 [1] makes it rather
>> inconvenient to use quantified constraints in type synonyms. For
>> instance, GHC rejects the following example by default:
>>
>>     type F f = (Functor f, forall a. Eq (f a))
>>
>> This is because F is a synonym for a constraint tuple, so mentioning a
>> quantified constraint in one of its arguments gets flagged as
>> impredicative. In the discussion for #16140, we have pondered doing a
>> major rewrite of the code in TcValidity to permit F. But perhaps we
>> don't need to! After all, the quantified constraint in the example
>> above appears directly underneath a type constructor (namely, the type
>> constructor for the constraint 2-tuple), which should be a textbook
>> case of guarded impredicativity.
>>
>> I don't have the guarded impredicativity branch built locally, so I am
>> unable to test if this hypothesis is true. In any case, I wanted to
>> mention it as another motivating use case.
>>
>> Ryan S.
>> -----
>> [1] https://gitlab.haskell.org/ghc/ghc/issues/16140
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Alejandro Serrano Mena
Just to keep you posted about the current development, we are working on a new approach to impredicativity which is inspired by guarded impredicativity but requires much fewer changes to the codebase. In particular, our goal is to isolate the inference of impredicativity, instead of contaminating the whole compiler with it.

The repo where we are developing it lives in https://gitlab.haskell.org/trupill/ghc (branch "quick-look").

Regards,
Alejandro

El vie., 19 jul. 2019 a las 23:40, Ryan Scott (<[hidden email]>) escribió:
Good to know. Thanks for checking!

Ryan S.

On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn
<[hidden email]> wrote:
>
> Hello Ryan,
>
> Your example seems to work out of the box with the GI branch.
>
> With the oneliner Matthew posted before:
> nix run -f https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz \
> ghc-head-from -c ghc-head-from \
> https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz
> It is really easy to check. Also, I didn't see anywhere mentioned that one need to provide -XImpredicativeTypes. The whole example, therefore, is:
>
> {-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}
> module M where
> type F f = (Functor f, forall a. Eq (f a))
>
> --
> Best, Artem
>
> On Fri, 19 Jul 2019 at 09:18, Ryan Scott <[hidden email]> wrote:
>>
>> I have another interesting application of guarded impredicativity that
>> I want to bring up. Currently, GHC #16140 [1] makes it rather
>> inconvenient to use quantified constraints in type synonyms. For
>> instance, GHC rejects the following example by default:
>>
>>     type F f = (Functor f, forall a. Eq (f a))
>>
>> This is because F is a synonym for a constraint tuple, so mentioning a
>> quantified constraint in one of its arguments gets flagged as
>> impredicative. In the discussion for #16140, we have pondered doing a
>> major rewrite of the code in TcValidity to permit F. But perhaps we
>> don't need to! After all, the quantified constraint in the example
>> above appears directly underneath a type constructor (namely, the type
>> constructor for the constraint 2-tuple), which should be a textbook
>> case of guarded impredicativity.
>>
>> I don't have the guarded impredicativity branch built locally, so I am
>> unable to test if this hypothesis is true. In any case, I wanted to
>> mention it as another motivating use case.
>>
>> Ryan S.
>> -----
>> [1] https://gitlab.haskell.org/ghc/ghc/issues/16140
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs