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 (<arnaud.spiwack at tweag.io>)
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 <
> 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/630bba60/attachment.html>