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-bounces@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/].

 

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