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

[Simon Peyton Jones]

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<mailto: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<mailto: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<mailto: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<mailto: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<mailto:ghc-steering-committee at haskell.org>
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20191017/5aa9994b/attachment-0001.html>