Re: [ghc-steering-committee] Quick look impredicativity (#274) — recommendation: accept

We can't remove the discussion entirely, right? Removing contravariance is necessary for QuickLook to work for the most common case of impredicative instantiation. I would, however, support returning the proposal to its previous recommendation to 1. introduce `-X[No]ContravariantFunctions` 2. enable `-XContravariantFunctions` by default` 3. make `-XImpredicativeTypes` imply `-XNoContravariantFunctions` and move discussion of deprecating contravariance (and any other excesses in the type system) to a follow-on proposal. It seems to me that the above steps are the minimum for the QuickLook proposal to be acceptable on its own. On Thu, Oct 17, 2019, at 07:27, Spiwack, Arnaud wrote:

Sweet!

Should we, therefore, consider removing the contravariance discussion from the quick look impredicativity proposal?

On Thu, Oct 17, 2019 at 1:24 PM Simon Peyton Jones wrote:

...

Any other opinion on deprecation of `-XContravariantFunctions`? I'd like this to be planned and to have a schedule. Maybe, as Simon suggested in the Github thread, this should be another discussion, though?____

...

__ __

...

I have produced a GHC Proposal____

...

https://github.com/ghc-proposals/ghc-proposals/pull/287____

...

__ __

...

Simon____

...

__ __

...

*From:* ghc-steering-committee *On Behalf Of *Spiwack, Arnaud *Sent:* 17 October 2019 08:05 *To:* Iavor Diatchki *Cc:* ghc-steering-committee *Subject:* Re: [ghc-steering-committee] Quick look impredicativity (#274) — recommendation: accept____

...

__ __

...

Support seems unanimous so far. Unless someones voices a second opinion by then, I'll accept the proposal early next week.____

...

__ __

...

Any other opinion on deprecation of `-XContravariantFunctions`? I'd like this to be planned and to have a schedule. Maybe, as Simon suggested in the Github thread, this should be another discussion, though?____

...

__ __

...

On Wed, Oct 16, 2019 at 7:45 PM Iavor Diatchki wrote:____

...

...

I haven't had time to read through this proposal, but I am comfortable accepting it based on the recommendations of others.

On Mon, Oct 14, 2019 at 5:52 PM Eric Seidel wrote:

...

I support acceptance too, modulo a few small comments that I left on the GH discussion.

On Mon, Oct 14, 2019, at 02:53, Spiwack, Arnaud wrote:

...

Dear all,

As the title implies: I'm hereby recommending accepting the Quick look impredicativity proposal.

Summary:

The proposal modifies the `-XImpredicativeTypes` extension with a well defined semantics which consists in considering n-ary applications, rather than binary. And look, in such an application, for arguments which absolutely require impredicative instantiation (either universally quantified type applications, or arguments where a universal type is guarded by an invariant type constructor).

In order to have the expected behaviour for `($)` and `(.)`, the proposal also makes the left-hand argument of the arrow invariant with respect to instantiation (currently: contravariant). The proposal is to make this change effective, even if `-XRankNTypes` is turned on, but not `-XImpredicativeTypes`. The proposal also introduces an extension `-XContravariantFunctions` to restore the old behaviour, for compatibility.

Rational:

`-XImpredicativeTypes` is a useful extension which is currently in a rather sad state. I'm happy to see it stabilise to a clear semantics. The semantics in the proposal covers a ton of use cases. It strikes a very good balance between usefulness and predictability.

The use of n-ary application in the type system also has good theoretical roots: sequent calculi have n-ary applications. (in manyrespects, bidirectional type systems are also about n-ary application). So I don't consider it a wart at all.

The propsal's semantics, including the absence of contravariant functions, goes in the direction of _guessing less things_. This is a direction that many GHC features have taken lately. I think it's a very very good direction! Guessing can be damaging for predictability, but. more importantly, guessing has a tendency to compose badly with other typing features. (it is to be noted, too, that the implementation of contravariant functions. in GHC, eta-expands the function, which can casually change its semantics, if the function was bottom).

So, everything in this proposal does look good to me, except that, I think, I would like a deprecation route for the `-XContravariantFunctions` extension. Otherwise, we will be stuck with legacy code forever.

Best, Arnaud _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee____

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee