RE: GHC 6.12.1 and impredicative polymorphism

[Simon Peyton-Jones]

| Hello Simon and others,
| 
| unfortunately, I missed this e-mail.
| 
| Yes, removal of impredicative polymorphism hurts me, since impredicativity
| plays a crucial role in the Grapefruit FRP library at the moment. This is
| described in section 5 of my paper “Signals, Not Generators!” [5]. It’s
| probably possible to use a workaround involving a newtype wrapper, in case
| polymorphic fields in newtypes are still supported. However, this makes things
| more awkward for library users.

I plan to support impredicative polymorphism in some form; but you may need 
more type annotations.

I'll announce when there's something to test (it'll be a couple of months).

Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 6.12.1 and impredicative polymorphism

[Wolfgang Jeltsch]

Am Freitag, 30. Oktober 2009 10:51:37 schrieb Simon Peyton-Jones:
> Friends
> 
> One more update about GHC 6.12, concerning impredicative polymorphism.
> 
> GHC has had an experimental implementation of impredicative polymorphism
>  for a year or two now (flag -XImpredicativePolymorphism). But
> 
>   a) The implementation is ridiculously complicated, and the complexity
>  is pervasive (in the type checker) rather than localized.
>  I'm very unhappy about this, especially as we add more stuff to
>  the type checker for type families.
> 
>   b) The specification (type system) is well-defined [1], but is also
>  pretty complicated, and it's just too hard to predict which programs will
>  typecheck and which will not.
> 
> So it's time for a re-think.  I propose to deprecate it in 6.12, and remove
> it altogether in 6.14.  We may by then have something else to put in its
> place.  (There is no lack of candidates [2,3,4]!)
> 
> Fortunately, I don't think a lot of people use the feature in anger. 
> Please yell if you *are* using impredicative polymorphism for something
> serious.  But if you are, we need to think of a workaround.  The current
> situation seems unsustainable.
> 
> Simon
> 
> [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/
> [2] http://research.microsoft.com/en-us/um/people/crusso/qml/
> [3] http://research.microsoft.com/en-us/um/people/daan/pubs.html
> [4] http://gallium.inria.fr/~remy/mlf/

Hello Simon and others,

unfortunately, I missed this e-mail.

Yes, removal of impredicative polymorphism hurts me, since impredicativity 
plays a crucial role in the Grapefruit FRP library at the moment. This is 
described in section 5 of my paper “Signals, Not Generators!” [5]. It’s 
probably possible to use a workaround involving a newtype wrapper, in case 
polymorphic fields in newtypes are still supported. However, this makes things 
more awkward for library users.

Best wishes,
Wolfgang

[5] 
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 6.12.1 and impredicative polymorphism

[Dan Doel]

On Friday 30 October 2009 5:51:37 am Simon Peyton-Jones wrote:
> One more update about GHC 6.12, concerning impredicative polymorphism.
> 
> GHC has had an experimental implementation of impredicative polymorphism
>  for a year or two now (flag -XImpredicativePolymorphism). But
> 
>   a) The implementation is ridiculously complicated, and the complexity
>  is pervasive (in the type checker) rather than localized.
>  I'm very unhappy about this, especially as we add more stuff to
>  the type checker for type families.
> 
>   b) The specification (type system) is well-defined [1], but is also
>  pretty complicated, and it's just too hard to predict which programs will
>  typecheck and which will not.
> 
> So it's time for a re-think.  I propose to deprecate it in 6.12, and remove
>  it altogether in 6.14.  We may by then have something else to put in its
>  place.  (There is no lack of candidates [2,3,4]!)

This may be a side issue, but...

Someone was asking in #haskell yesterday about what exactly ImpredicativeTypes 
did, as it's a bit difficult to tell at first. I eventually came to the 
conclusion that some of the notation GHC uses may be rather poor.

In a lambda cube/pure type system setting, the difference between an 
impredicative and predicative system are the rules:

   ([], *, *) vs. ([], *, [])

Where the first rule says that, for instance:

  (Pi a:*. a -> a) : *

while the second says:

  (Pi a:*. a -> a) : []

The first is impredicative due to * containing (Pi a:*. a -> a) itself, so the 
expression quantifies over a 'set' containing itself.

But, if we ask GHC the kind of:

  forall a. a -> a

it tells us the answer is *, even without ImpredicativeTypes. But that *looks* 
like a statement that the type system is impredicative already. And in fact, 
we can stick a signature on the identity function like:

  id :: (forall a. a -> a) -> (forall a. a -> a)

which appears to allow impredicative instantiation of variables as long as 
they're only used in functions. But, of course, this fails for datatypes 
without the relevant flag. Maybe :: * -> *, but we're not allowed to apply it 
to (forall a. a -> a), even though GHC tells us the latter has type * 
(although, asking the kind of Maybe (forall a. a -> a) does not blow up; only 
trying to use it as a type does).

At some point in the discussion, someone quoted from the boxy paper that in 
HM, quantification ranges over monotypes. Presumably, GHC maintains such a 
distinction internally, which is roughly analogous[1] to tracking the 
difference between * and []. But, when it comes time to display sorts, it 
shows both * and [] as *, which makes it somewhat unclear why Maybe (forall a. 
a) is invalid.

So, to get to the point, whatever implementation is decided upon in the 
future, if predicativity is still around, I think it'd be useful to make that 
predicativity noticeable in the types/kinds/sorts, rather than the current 
situation, which to an observer looks like, "* contains both monotypes and 
polytypes, but quantification over * only really ranges over the monotypes 
(maybe)." I don't know how this would complicate GHC's current kind system, as 
I know it isn't set up like a pure type system, but it might be something to 
think about.

Cheers,
-- Dan

[1] It probably isn't a perfect correspondence. For instance (based on my 
experience implementing rather naive interpreters), in a predicative, lambda 
cube F2, the type:

  forall a. forall b. a -> b

is invalid, because 'forall b. a -> b' has sort [], and so the additional 
quantifier requires the rule ([],[],[]), which gets you to Fomega.

  forall a. (forall b. b) -> a = (forall b. b) -> (forall a. a)

are similarly invalid. But, it feels a bit accidental to me that the Fomega 
rule allows these, so one could probably keep a sort divide between monotypes 
and polytypes while allowing repeated and higher-rank quantification, and also 
not allowing higher-order types (although Haskell has the latter anyway).
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 6.12.1 and impredicative polymorphism

[Ben Moseley]

I expect we can - we'll investigate.

--Ben

On 2 Nov 2009, at 09:32, Simon Peyton-Jones wrote:


| Is there any difference between "-XImpredicativePolymorphism" and "-
| XImpredicativeTypes"?

No there isn't.  There's only one flag, -XImpredicativeTypes.

| Hyena uses the latter, and we're using Hyena somewhat "in anger".

Interesting.  I hope you can get along without it, perhaps with a  
bit more newtype wrapping/unwrapping code.  As I say, the current  
situation is not good.



Simon


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: GHC 6.12.1 and impredicative polymorphism

[Ganesh Sittampalam]

On Fri, 30 Oct 2009, Sittampalam, Ganesh wrote:


Simon Peyton-Jones wrote:


Fortunately, I don't think a lot of people use the feature in anger.
Please yell if you *are* using impredicative polymorphism for
something serious.  But if you are, we need to think of a workaround.
The current situation seems unsustainable.


I think darcs is using it. At least, I had to enable
ImpredicativePolymorphism to successfully build darcs with GHC 6.11 (a
snapshot from about February), although the flag is not required with
GHC 6.10. I haven't had a chance to try with the RC yet, but will do
this weekend.

I'll have to check the full details of why it's needed, but from memory
I think it can be worked around at the cost of more verbosity by using
some newtypes in appropriate places.


OK, I confirm the changes are fairly trivial. The main issue is that a 
couple of functions want to instantiate the argument to IO with a type 
scheme:


restrictBoring :: IO (forall t m. FilterTree t m => t m -> t m)

The newtype workaround works fine here and doesn't affect too much of the 
code. In one other place some code had type [(String, Foo)] where Foo is a 
type synonym for (forall x y . ), but it turned out the nested 
quantification wasn't required so (forall x y . [(String, )]) 
was ok in this case, if a little uglier.


(Patch sent to darcs-users)

Cheers,

Ganesh
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: GHC 6.12.1 and impredicative polymorphism

[Simon Peyton-Jones]

| Is there any difference between "-XImpredicativePolymorphism" and "-
| XImpredicativeTypes"?

No there isn't.  There's only one flag, -XImpredicativeTypes.

| Hyena uses the latter, and we're using Hyena somewhat "in anger".

Interesting.  I hope you can get along without it, perhaps with a bit more 
newtype wrapping/unwrapping code.  As I say, the current situation is not good.


Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 6.12.1 and impredicative polymorphism

[Ben Moseley]

Is there any difference between "-XImpredicativePolymorphism" and "- 
XImpredicativeTypes"?


Hyena uses the latter, and we're using Hyena somewhat "in anger".

--Ben

On 30 Oct 2009, at 09:51, Simon Peyton-Jones wrote:


Friends

One more update about GHC 6.12, concerning impredicative polymorphism.

GHC has had an experimental implementation of impredicative  
polymorphism for a year or two now (flag - 
XImpredicativePolymorphism). But


 a) The implementation is ridiculously complicated, and the complexity
is pervasive (in the type checker) rather than localized.
I'm very unhappy about this, especially as we add more stuff to
the type checker for type families.

 b) The specification (type system) is well-defined [1], but is also  
pretty

complicated, and it's just too hard to predict which programs will
typecheck and which will not.

So it's time for a re-think.  I propose to deprecate it in 6.12, and  
remove it altogether in 6.14.  We may by then have something else to  
put in its place.  (There is no lack of candidates [2,3,4]!)


Fortunately, I don't think a lot of people use the feature in  
anger.  Please yell if you *are* using impredicative polymorphism  
for something serious.  But if you are, we need to think of a  
workaround.  The current situation seems unsustainable.


Simon

[1] http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/
[2] http://research.microsoft.com/en-us/um/people/crusso/qml/
[3] http://research.microsoft.com/en-us/um/people/daan/pubs.html
[4] http://gallium.inria.fr/~remy/mlf/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: GHC 6.12.1 and impredicative polymorphism

[Sittampalam, Ganesh]

Simon Peyton-Jones wrote:

> Fortunately, I don't think a lot of people use the feature in anger. 
> Please yell if you *are* using impredicative polymorphism for
> something serious.  But if you are, we need to think of a workaround.
> The current situation seems unsustainable.   

I think darcs is using it. At least, I had to enable
ImpredicativePolymorphism to successfully build darcs with GHC 6.11 (a
snapshot from about February), although the flag is not required with
GHC 6.10. I haven't had a chance to try with the RC yet, but will do
this weekend.

I'll have to check the full details of why it's needed, but from memory
I think it can be worked around at the cost of more verbosity by using
some newtypes in appropriate places.

Cheers,

Ganesh

=== 
 Please access the attached hyperlink for an important electronic 
communications disclaimer: 
 http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html 
 
=== 
 
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users