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

[Eric Seidel]

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 at 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 at haskell.org> *On Behalf Of *Spiwack, Arnaud
> > *Sent:* 17 October 2019 08:05
> > *To:* Iavor Diatchki <iavor.diatchki at gmail.com>
> > *Cc:* ghc-steering-committee <ghc-steering-committee at 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 at 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 at 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 at haskell.org
> >>  > >  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> >>  > >
> >>  > _______________________________________________
> >>  > ghc-steering-committee mailing list
> >>  > ghc-steering-committee at haskell.org
> >>  >  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> >>  _______________________________________________
> >>  ghc-steering-committee mailing list
> >> ghc-steering-committee at haskell.org
> >> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee____
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>