Guarded Impredicativity

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

Guarded Impredicativity

Alejandro Serrano Mena
Dear all,

We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].

For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.

The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.

Just for reference, the best to get a working clone is to follow these steps:
> git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> cd impredicative-ghc
> git remote add trupill [hidden email]:trupill/ghc.git
> git fetch trupill
> git checkout trupill master

Thanks very much in advance,
Alejandro


_______________________________________________
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

GHC - devs mailing list

Just to amplify: we are very interested to

 

  • Get some idea of whether anyone  cares about impredicativity.  If we added it to GHC, would you use it?  Have you ever bumped up Haskell’s inability to instantiate a polymorphic function at a polytype.

 

  • Get some idea of whether the particular form of impredicativity described in the paper would be expressive enough for your application.

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 28 June 2019 13:12
To: [hidden email]
Subject: Guarded Impredicativity

 

Dear all,

 

We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].

 

For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.

 

The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).

For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.

 

Just for reference, the best to get a working clone is to follow these steps:

> git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc

> cd impredicative-ghc

> git remote add trupill [hidden email]

> git fetch trupill

> git checkout trupill master

 

Thanks very much in advance,

Alejandro

 


_______________________________________________
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

Matthew Pickering
In reply to this post by Alejandro Serrano Mena
Have you modified how typed quotations are type checked? For example,
with your patch I would hope that

[| id |] :: Code (forall a . a -> a)

would be accepted?

I'll try it out. This patch will have big ramifications for the typed
template haskell community.

Matt

On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
<[hidden email]> wrote:

>
> Dear all,
>
> We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>
> For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>
> The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
> For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>
> Just for reference, the best to get a working clone is to follow these steps:
> > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> > cd impredicative-ghc
> > git remote add trupill [hidden email]:trupill/ghc.git
> > git fetch trupill
> > git checkout trupill master
>
> Thanks very much in advance,
> Alejandro
>
> _______________________________________________
> 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
No, up to now the only changes are in the type checking of applications and variables.
However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).

El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
Have you modified how typed quotations are type checked? For example,
with your patch I would hope that

[| id |] :: Code (forall a . a -> a)

would be accepted?

I'll try it out. This patch will have big ramifications for the typed
template haskell community.

Matt

On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
<[hidden email]> wrote:
>
> Dear all,
>
> We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>
> For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>
> The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
> For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>
> Just for reference, the best to get a working clone is to follow these steps:
> > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> > cd impredicative-ghc
> > git remote add trupill [hidden email]:trupill/ghc.git
> > git fetch trupill
> > git checkout trupill master
>
> Thanks very much in advance,
> Alejandro
>
> _______________________________________________
> 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

Elliot Cameron-2
Sorry meant to reply all:

I ran into the error recently here: https://github.com/monadfix/named/issues/24

trying to use a fun named arguments library. I can't immediately tell if these changes to GHC are sufficient to help. This library is using a newtype with phantom arguments.

On Fri, Jun 28, 2019, 8:20 AM Alejandro Serrano Mena <[hidden email]> wrote:
No, up to now the only changes are in the type checking of applications and variables.
However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).

El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
Have you modified how typed quotations are type checked? For example,
with your patch I would hope that

[| id |] :: Code (forall a . a -> a)

would be accepted?

I'll try it out. This patch will have big ramifications for the typed
template haskell community.

Matt

On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
<[hidden email]> wrote:
>
> Dear all,
>
> We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>
> For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>
> The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
> For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>
> Just for reference, the best to get a working clone is to follow these steps:
> > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> > cd impredicative-ghc
> > git remote add trupill [hidden email]:trupill/ghc.git
> > git fetch trupill
> > git checkout trupill master
>
> Thanks very much in advance,
> Alejandro
>
> _______________________________________________
> 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
Reply | Threaded
Open this post in threaded view
|

Re: Guarded Impredicativity

Matthew Pickering
In reply to this post by Alejandro Serrano Mena
I just tried it and it doesn't currently work.

[1 of 1] Compiling Id               ( Id.hs, interpreted )

Id.hs:14:7: error:
    • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
      Expected type: TExpQ (forall a. a -> a)
        Actual type: Q (TExp (a0 -> a0))
    • In the Template Haskell quotation [|| id ||]
      In the expression: [|| id ||]
      In an equation for ‘foo’: foo = [|| id ||]
   |
14 | foo = [|| id ||]
   |

Do you think you could perhaps take a look into fixing it?

PS: If you disable the testsuite on CI (so that the build passes) then
people can download and use the artefacts from your branch rather than
have to build the compiler from source.

Cheers,

Matt

On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
<[hidden email]> wrote:

>
> No, up to now the only changes are in the type checking of applications and variables.
> However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).
>
> El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
>>
>> Have you modified how typed quotations are type checked? For example,
>> with your patch I would hope that
>>
>> [| id |] :: Code (forall a . a -> a)
>>
>> would be accepted?
>>
>> I'll try it out. This patch will have big ramifications for the typed
>> template haskell community.
>>
>> Matt
>>
>> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
>> <[hidden email]> wrote:
>> >
>> > Dear all,
>> >
>> > We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>> >
>> > For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>> >
>> > The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
>> > For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>> >
>> > Just for reference, the best to get a working clone is to follow these steps:
>> > > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
>> > > cd impredicative-ghc
>> > > git remote add trupill [hidden email]:trupill/ghc.git
>> > > git fetch trupill
>> > > git checkout trupill master
>> >
>> > Thanks very much in advance,
>> > Alejandro
>> >
>> > _______________________________________________
>> > 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
In reply to this post by Alejandro Serrano Mena
Would this permit explicit impredicativity as described in [1]? Simon mentions in [1] that explicit impredicativity is easier to implement than guarded impredicativity, although it's not clear to me if the latter would imply the former.

Ryan S.
-----

_______________________________________________
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
In reply to this post by Matthew Pickering
Hi,

El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<[hidden email]>) escribió:
I just tried it and it doesn't currently work.

[1 of 1] Compiling Id               ( Id.hs, interpreted )

Id.hs:14:7: error:
    • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
      Expected type: TExpQ (forall a. a -> a)
        Actual type: Q (TExp (a0 -> a0))
    • In the Template Haskell quotation [|| id ||]
      In the expression: [|| id ||]
      In an equation for ‘foo’: foo = [|| id ||]
   |
14 | foo = [|| id ||]
   |

Do you think you could perhaps take a look into fixing it?

I will give it a try.

PS: If you disable the testsuite on CI (so that the build passes) then
people can download and use the artefacts from your branch rather than
have to build the compiler from source.

Is there an easy way to do this (or a tutorial), better in a way which doesn't break the actual CI pipeline if this is finally merged?

Regards,
Alejandro


On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
<[hidden email]> wrote:
>
> No, up to now the only changes are in the type checking of applications and variables.
> However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).
>
> El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
>>
>> Have you modified how typed quotations are type checked? For example,
>> with your patch I would hope that
>>
>> [| id |] :: Code (forall a . a -> a)
>>
>> would be accepted?
>>
>> I'll try it out. This patch will have big ramifications for the typed
>> template haskell community.
>>
>> Matt
>>
>> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
>> <[hidden email]> wrote:
>> >
>> > Dear all,
>> >
>> > We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>> >
>> > For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>> >
>> > The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
>> > For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>> >
>> > Just for reference, the best to get a working clone is to follow these steps:
>> > > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
>> > > cd impredicative-ghc
>> > > git remote add trupill [hidden email]:trupill/ghc.git
>> > > git fetch trupill
>> > > git checkout trupill master
>> >
>> > Thanks very much in advance,
>> > Alejandro
>> >
>> > _______________________________________________
>> > 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
In reply to this post by Ryan Scott
Yes, this is one of the features we would like to have. If you write down the explicit instantiation of a function, we just take it, no questions asked (well, the terms should still be type correct).
But writing out *every* single impredicative instantiation is really tiresome, hence we are looking for "simple" ways to flow this information around and alleavite a bit the burden.

El vie., 28 jun. 2019 a las 15:43, Ryan Scott (<[hidden email]>) escribió:
Would this permit explicit impredicativity as described in [1]? Simon mentions in [1] that explicit impredicativity is easier to implement than guarded impredicativity, although it's not clear to me if the latter would imply the former.

Ryan S.
-----
_______________________________________________
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
In reply to this post by Matthew Pickering
After having a quick look, I think it could be done easily in terms of type checking. Alas, there's some code in TcSplice.hs which insists anyway on having a quantifier-free type:

tcTExpTy :: TcType -> TcM TcType
tcTExpTy exp_ty
= do { unless (isTauTy exp_ty) $ addErr (err_msg exp_ty)
; ... }
where
err_msg ty
= vcat [ text "Illegal polytype:" <+> ppr ty
, text "The type of a Typed Template Haskell expression must" <+>
text "not have any quantification." ]

Does anybody have any pointers about why this restriction is in place?

Regards,
Alejandro

El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<[hidden email]>) escribió:
I just tried it and it doesn't currently work.

[1 of 1] Compiling Id               ( Id.hs, interpreted )

Id.hs:14:7: error:
    • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
      Expected type: TExpQ (forall a. a -> a)
        Actual type: Q (TExp (a0 -> a0))
    • In the Template Haskell quotation [|| id ||]
      In the expression: [|| id ||]
      In an equation for ‘foo’: foo = [|| id ||]
   |
14 | foo = [|| id ||]
   |

Do you think you could perhaps take a look into fixing it?

PS: If you disable the testsuite on CI (so that the build passes) then
people can download and use the artefacts from your branch rather than
have to build the compiler from source.

Cheers,

Matt

On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
<[hidden email]> wrote:
>
> No, up to now the only changes are in the type checking of applications and variables.
> However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).
>
> El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
>>
>> Have you modified how typed quotations are type checked? For example,
>> with your patch I would hope that
>>
>> [| id |] :: Code (forall a . a -> a)
>>
>> would be accepted?
>>
>> I'll try it out. This patch will have big ramifications for the typed
>> template haskell community.
>>
>> Matt
>>
>> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
>> <[hidden email]> wrote:
>> >
>> > Dear all,
>> >
>> > We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>> >
>> > For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>> >
>> > The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
>> > For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>> >
>> > Just for reference, the best to get a working clone is to follow these steps:
>> > > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
>> > > cd impredicative-ghc
>> > > git remote add trupill [hidden email]:trupill/ghc.git
>> > > git fetch trupill
>> > > git checkout trupill master
>> >
>> > Thanks very much in advance,
>> > Alejandro
>> >
>> > _______________________________________________
>> > 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

Matthew Pickering
I believe the restriction is because of impredicativity..

My idea was to temporarily break the CI config whilst the tests don't
pass. I can make a MR for you if this would be acceptable.

Matt

On Fri, Jun 28, 2019 at 3:27 PM Alejandro Serrano Mena
<[hidden email]> wrote:

>
> After having a quick look, I think it could be done easily in terms of type checking. Alas, there's some code in TcSplice.hs which insists anyway on having a quantifier-free type:
>
> tcTExpTy :: TcType -> TcM TcType
> tcTExpTy exp_ty
> = do { unless (isTauTy exp_ty) $ addErr (err_msg exp_ty)
> ; ... }
> where
> err_msg ty
> = vcat [ text "Illegal polytype:" <+> ppr ty
> , text "The type of a Typed Template Haskell expression must" <+>
> text "not have any quantification." ]
>
> Does anybody have any pointers about why this restriction is in place?
>
> Regards,
> Alejandro
>
> El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<[hidden email]>) escribió:
>>
>> I just tried it and it doesn't currently work.
>>
>> [1 of 1] Compiling Id               ( Id.hs, interpreted )
>>
>> Id.hs:14:7: error:
>>     • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
>>       Expected type: TExpQ (forall a. a -> a)
>>         Actual type: Q (TExp (a0 -> a0))
>>     • In the Template Haskell quotation [|| id ||]
>>       In the expression: [|| id ||]
>>       In an equation for ‘foo’: foo = [|| id ||]
>>    |
>> 14 | foo = [|| id ||]
>>    |
>>
>> Do you think you could perhaps take a look into fixing it?
>>
>> PS: If you disable the testsuite on CI (so that the build passes) then
>> people can download and use the artefacts from your branch rather than
>> have to build the compiler from source.
>>
>> Cheers,
>>
>> Matt
>>
>> On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
>> <[hidden email]> wrote:
>> >
>> > No, up to now the only changes are in the type checking of applications and variables.
>> > However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).
>> >
>> > El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<[hidden email]>) escribió:
>> >>
>> >> Have you modified how typed quotations are type checked? For example,
>> >> with your patch I would hope that
>> >>
>> >> [| id |] :: Code (forall a . a -> a)
>> >>
>> >> would be accepted?
>> >>
>> >> I'll try it out. This patch will have big ramifications for the typed
>> >> template haskell community.
>> >>
>> >> Matt
>> >>
>> >> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
>> >> <[hidden email]> wrote:
>> >> >
>> >> > Dear all,
>> >> >
>> >> > We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>> >> >
>> >> > For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>> >> >
>> >> > The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
>> >> > For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>> >> >
>> >> > Just for reference, the best to get a working clone is to follow these steps:
>> >> > > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
>> >> > > cd impredicative-ghc
>> >> > > git remote add trupill [hidden email]:trupill/ghc.git
>> >> > > git fetch trupill
>> >> > > git checkout trupill master
>> >> >
>> >> > Thanks very much in advance,
>> >> > Alejandro
>> >> >
>> >> > _______________________________________________
>> >> > 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

Matthew Pickering
In reply to this post by Alejandro Serrano Mena
Here is a nix one liner to test the current state of the branch.

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

On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
<[hidden email]> wrote:

>
> Dear all,
>
> We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].
>
> For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.
>
> The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
> For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.
>
> Just for reference, the best to get a working clone is to follow these steps:
> > git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> > cd impredicative-ghc
> > git remote add trupill [hidden email]:trupill/ghc.git
> > git fetch trupill
> > git checkout trupill master
>
> Thanks very much in advance,
> Alejandro
>
> _______________________________________________
> 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

Spiwack, Arnaud
In reply to this post by GHC - devs mailing list
Dear Alejandro and Simon,

Taking into account that I'm a bit of an impredicativity nut, so I may be over enthusiastic.

- I frequently want more impredicativity in GHC
- Last time I did, guarded impredicativity, as in the paper, would have, I believed, done the trick.

That being said, it is somewhat hard to give an answer on the spot, but I'll try to take note of why and whether guarded impredicativity would suffice.

Best,
Arnaud


On Fri, Jun 28, 2019 at 2:15 PM Simon Peyton Jones via ghc-devs <[hidden email]> wrote:

Just to amplify: we are very interested to

 

  • Get some idea of whether anyone  cares about impredicativity.  If we added it to GHC, would you use it?  Have you ever bumped up Haskell’s inability to instantiate a polymorphic function at a polytype.

 

  • Get some idea of whether the particular form of impredicativity described in the paper would be expressive enough for your application.

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 28 June 2019 13:12
To: [hidden email]
Subject: Guarded Impredicativity

 

Dear all,

 

We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].

 

For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.

 

The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).

For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.

 

Just for reference, the best to get a working clone is to follow these steps:

> git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc

> cd impredicative-ghc

> git remote add trupill [hidden email]

> git fetch trupill

> git checkout trupill master

 

Thanks very much in advance,

Alejandro

 

_______________________________________________
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
Thanks very much,
If you had some snippets of code or some libraries you could share with us, that would be extremely helpful.

Regards,
Alejandro

El jue., 4 jul. 2019 a las 9:10, Spiwack, Arnaud (<[hidden email]>) escribió:
Dear Alejandro and Simon,

Taking into account that I'm a bit of an impredicativity nut, so I may be over enthusiastic.

- I frequently want more impredicativity in GHC
- Last time I did, guarded impredicativity, as in the paper, would have, I believed, done the trick.

That being said, it is somewhat hard to give an answer on the spot, but I'll try to take note of why and whether guarded impredicativity would suffice.

Best,
Arnaud


On Fri, Jun 28, 2019 at 2:15 PM Simon Peyton Jones via ghc-devs <[hidden email]> wrote:

Just to amplify: we are very interested to

 

  • Get some idea of whether anyone  cares about impredicativity.  If we added it to GHC, would you use it?  Have you ever bumped up Haskell’s inability to instantiate a polymorphic function at a polytype.

 

  • Get some idea of whether the particular form of impredicativity described in the paper would be expressive enough for your application.

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 28 June 2019 13:12
To: [hidden email]
Subject: Guarded Impredicativity

 

Dear all,

 

We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/].

 

For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.

 

The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).

For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.

 

Just for reference, the best to get a working clone is to follow these steps:

> git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc

> cd impredicative-ghc

> git remote add trupill [hidden email]

> git fetch trupill

> git checkout trupill master

 

Thanks very much in advance,

Alejandro

 

_______________________________________________
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