| 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 don't think so -- it just weakens it so that it works in fewer cases. Best to ask Alejandro -- by putting this technical discussion on the thread rather than on the committee list. S | -----Original Message----- | From: ghc-steering-committee <ghc-steering-committee-bounces@haskell.org> | On Behalf Of Eric Seidel | Sent: 17 October 2019 14:01 | To: ghc-steering-committee@haskell.org | Subject: 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 | > <simonpj@microsoft.com> 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 <ghc-steering-committee- | bounces@haskell.org> *On Behalf Of *Spiwack, Arnaud | > > *Sent:* 17 October 2019 08:05 | > > *To:* Iavor Diatchki <iavor.diatchki@gmail.com> | > > *Cc:* ghc-steering-committee <ghc-steering-committee@haskell.org> | > > *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 | <iavor.diatchki@gmail.com> 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 <eric@seidel.io> 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 | > | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee