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 <[email protected]> On Behalf Of Alejandro Serrano Mena Sent: 28 June 2019 13:12 To: [email protected] 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 > [email protected]:trupill/ghc.git<mailto:[email protected]:trupill/ghc.git> > git fetch trupill > git checkout trupill master Thanks very much in advance, Alejandro
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
