[ghc-steering-committee] Fwd: Please review #640: Fix quantification order for a `op` b and a %m -> b (Recommendation: Accept)

[Simon Peyton Jones]

As I wrote on GH, I'm not convinced by the change for infix type
operators (the linear arrows change is fine).


I don't agree with your intuition on infix operators.  As I wrote on GH:

I sympathise with this, but *any* specification amounts to specify some
> linearisation of the tree. Your mental linearisation puts the function of
> (a op b) first; and mine does to. BUT I don't want us to have to specify
> a linearisation function, because *we already have one*: it's called
> "look at the left to right order of what the user wrote". It may not be a
> great linearisation function, but it is simple, easy to specify, no further
> explanation needed.


But I think you are now saying that *even if a left-to-right order was
"best", *there is a long-standing bug in GHC that puts `b` first in (a `b`
c`), and it's not worth the risk of change.   So instead we should
institutionalise the bug into the spec.

A change would break code like
f :: a `m` b -> (a,b)
...
foo = ...(f @Either @Int @Bool)...

where we have

   - An infix type operator that is a variable
   - Other type variables in the first argument of the infix application
   - No type-class constraint  (Wombat m => a `m` b) would put `m` first.
   - Visible type applications in at least one calls site

So yes, it's an un-forced breakage.  So maybe institutionalising the
exception into the spec is the right thing to do.

I would love to hear from other members of the committee with more
user-centric experience.

Simon

On Tue, 19 Mar 2024 at 08:18, Adam Gundry <adam at well-typed.com> wrote:

> As I wrote on GH, I'm not convinced by the change for infix type
> operators (the linear arrows change is fine). The odds of breakage are
> slight, but non-zero, and it's a particularly nasty form of breakage
> because a library may use an infix operator but the changed
> quantification order only affect downstream code using that library with
> TypeApplications. Perhaps nobody will be affected, but if someone is,
> they would have some justification to feel aggrieved at this change!
>
> If there was a compelling benefit to changing the status quo, this could
> be justifiable, but in this case I don't really see the harm in carving
> out an exception for infix operators from the usual "quantification is
> left-to-right" rule.
>
> Adam
>
>
> On 17/03/2024 14:15, Eric Seidel wrote:
> > I agree with Simon's intuition on GH, and support acceptance as-is.
> >
> > On Wed, Mar 13, 2024, at 02:57, Moritz Angermann wrote:
> >> I feel myself agreeing with Arnaud on this. The LH part is a no
> >> brainer, the infix op, i'm not fully convinced. But I'll trust Simon's
> >> intuition here.
> >>
> >> Simons comment reminded me I need to urgently get back to the
> >> -experimental proposal.
> >>
> >> On Tue, 12 Mar 2024 at 18:59, Simon Peyton Jones
> >> <simon.peytonjones at gmail.com> wrote:
> >>> I think we should accept the proposal as-is.  See my comment:
> https://github.com/ghc-proposals/ghc-proposals/pull/640#issuecomment-1991255204
> >>>
> >>> Simon
> >>>
> >>> On Tue, 12 Mar 2024 at 09:33, Arnaud Spiwack <arnaud.spiwack at tweag.io>
> wrote:
> >>>> I think that the linear types part is a no-brainer.
> >>>>
> >>>> The infix operator one is less clear. Adam feels that it'd be weird
> if “a `op` b” yielded a different order than “op a b” as is being proposed.
> It's definitely something you could go both ways about. I'm personally
> worried about backward compatibility. Admittedly, this case where we
> quantify implicitly over a variable in infix position is probably rare. But
> the breakage would be quite subtle. I'm just not sure it's worth it. Do we
> care enough about the order of implicit quantification that we want to
> change this long established one? Richard is more optimistic
> https://github.com/ghc-proposals/ghc-proposals/pull/640#issuecomment-1988401968
> >>>>
> >>>> So, anyway, I'm open to be swayed by arguments, but my current
> thinking is: make the change for a %m -> b, but not for a `op` b.
> >>>>
> >>>> On Sat, 9 Mar 2024 at 22:46, Malte Ott <malte.ott at maralorn.de> wrote:
> >>>>> Dear all,
> >>>>>
> >>>>> Vlad proposes to change the order of implicit quantification for type
> >>>>> variables occurring as type operators or in multiplicity annotations:
> >>>>>
> >>>>> https://github.com/ghc-proposals/ghc-proposals/pull/640
> >>>>>
> >>>>>
> https://github.com/int-index/ghc-proposals/blob/int-index/tyop-quantification-order/proposals/0000-tyop-quantification-order.rst
> >>>>>
> >>>>> The proposal is thankfully very simple. Change the implicit
> quantification order for
> >>>>>
> >>>>> "a `op` b" from "forall op a b" to "forall a op b".
> >>>>>
> >>>>> and
> >>>>>
> >>>>> "a %m -> b" from "forall a b m" to "forall a m b".
> >>>>>
> >>>>> The proposed new behavior corresponds to the original paper and our
> user guide.
> >>>>> This can be considered a bug fix and while we could also just change
> the
> >>>>> specification I think having a simple and memorable rule for
> quantification
> >>>>> order is valuable. Especially the currently implemented
> quantification order for
> >>>>> multiplicities is weird.
> >>>>>
> >>>>> The only painful point here is as usual a question of stability.
> What I don’t
> >>>>> like about this change is, that if any code base uses it (which Vlad
> doubts and
> >>>>> I tend to agree), the type error on GHC upgrade will be very
> incomprehensible
> >>>>> for users who didn’t read and understand the changelog.
> >>>>>
> >>>>> However multiplicities are new and explicitely unstable and I don’t
> really see a
> >>>>> reason why anyone would use infix notation on a qantified function.
> So I agree
> >>>>> that this very unlikely to happen in the wild. Also, users who rely
> on the type
> >>>>> application order right now should have noticed that something is
> off.
> >>>>>
> >>>>> Thus I recommend acceptance as is.
> >>>>>
> >>>>> Please voice your opinions!
> >>>>>
> >>>>> Malte
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, https://www.well-typed.com/
>
> Registered in England & Wales, OC335890
> 27 Old Gloucester Street, London WC1N 3AX, England
>
> _______________________________________________
> ghc-steering-committee mailing list
> 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/20240319/062d2f31/attachment-0001.html>