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.spiw...@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@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-boun...@haskell.org> *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-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 g...@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