[ghc-steering-committee] Quick look impredicativity (#274) — recommendation: accept
Simon Peyton Jones
simonpj at microsoft.com
Thu Oct 17 13:09:05 UTC 2019
| 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 at haskell.org>
| On Behalf Of Eric Seidel
| Sent: 17 October 2019 14:01
| To: ghc-steering-committee at 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 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
| >
| _______________________________________________
| ghc-steering-committee mailing list
| ghc-steering-committee at haskell.org
| https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
More information about the ghc-steering-committee
mailing list