Guarded Impredicativity

[Spiwack, Arnaud]

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 at 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 <ghc-devs-bounces at haskell.org> *On Behalf Of *Alejandro
> Serrano Mena
> *Sent:* 28 June 2019 13:12
> *To:* ghc-devs at 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-polymorphism/
> <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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190704/be6044d7/attachment.html>