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 < ghc-devs@haskell.org> 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 *On Behalf Of *Alejandro Serrano Mena *Sent:* 28 June 2019 13:12 *To:* ghc-devs@haskell.org *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-p... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.microsoft.com%2Fen-us%2Fresearch%2Fpublication%2Fguarded-impredicative-polymorphism%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496244478&sdata=o8H3dd5tLDRCGpwzsq6BMwNwYepPQgmoKsrXtLbJQdk%3D&reserved=0 ].

For now I have produced a first attempt, which lives in https://gitlab.haskell.org/trupill/ghc https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc&data=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496244478&sdata=TGegIFjwdjJ7XPdmlVNY3wve385FalfVLaW1YLCiXlM%3D&reserved=0. 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 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc&data=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496254471&sdata=hXtR8j0th3U65DW7MvaofVW8tq7pubXUJqlyflGSBPw%3D&reserved=0 impredicative-ghc

...

cd impredicative-ghc

...

git remote add trupill git@gitlab.haskell.org:trupill/ghc.git

...

git fetch trupill

...

git checkout trupill master

Thanks very much in advance,

Alejandro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 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 (< matthewtpickering@gmail.com>) 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 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-p... ].

...

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 git@gitlab.haskell.org:trupill/ghc.git git fetch trupill git checkout trupill master

Thanks very much in advance, Alejandro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Hi, El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (< matthewtpickering@gmail.com>) 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 wrote:

...

No, up to now the only changes are in the type checking of applications

...

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 (< matthewtpickering@gmail.com>) 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 wrote:

...

Dear all,

We are trying to bring back `ImpredicativeTypes` into GHC by using

...

...

...

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

...

...

...

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

and variables. the ideas in the "Guarded Impredicative Polymorphism" paper [ https://www.microsoft.com/en-us/research/publication/guarded-impredicative-p... ]. the variable appears under a type constructor. these steps:

...

...

...

...

git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc cd impredicative-ghc git remote add trupill git@gitlab.haskell.org:trupill/ghc.git git fetch trupill git checkout trupill master

Thanks very much in advance, Alejandro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 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 () 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 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 () 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 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-p...].

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 git@gitlab.haskell.org:trupill/ghc.git git fetch trupill git checkout trupill master

Thanks very much in advance, Alejandro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs