[ghc-steering-committee] #425: invisible binders in type declarations; rec: accept

Thu Apr 7 09:15:51 UTC 2022

Hi,

I didn’t hear any dissent, so I’ll mark this as accepted and will merge
it now.

Cheers,
Joachim

Am Samstag, dem 26.03.2022 um 16:10 +0100 schrieb Joachim Breitner:
> Hi,
> 
> sounds good to me, thanks for the good summary.
> 
> Cheers,
> Joachim
> 
> Am Donnerstag, dem 24.03.2022 um 18:47 +0000 schrieb Richard Eisenberg:
> > Hi committee,
> > 
> > I re-recommend acceptance for this proposal.
> > 
> > The main payload of the proposal is to allow definitions like
> > 
> > > data Proxy @k (a :: k) = Proxy
> > 
> > instead of today's
> > 
> > > data Proxy (a :: k) = Proxy
> > 
> > which has no explicit binding site for k.
> > 
> > This new syntax solves a number of smallish syntax conundra, as very
> > well outlined in the proposal.
> > 
> > Along with this primary change, there is some cleanup of (loosely)
> > related syntax:
> >  - a type synonym declaration is now required to mention all kind
> > variables on its left-hand side (previously, you could introduce a
> > kind variable only on the right in some circumstances)
> >  - arity inference for type synonyms and families with trailing
> > invisible quantifiers is simplified (you've never written such a
> > thing, I'm sure -- and yet GHC currently has special handling for
> > this bit of esoterica)
> >  - a type family equation must now mention all kind variables on its
> > left-hand side (just like the new rule for type synonyms)
> >  - a type family equation must now determine instantiation of all
> > kind variables via the left-hand side patterns (this vastly increases
> > readability and avoids some confusing behavior)
> > 
> > The cleanups can all break existing code. And so I posted on
> > Discourse seeking community feedback. The feedback did not suggest
> > this breakage would cause wide harm. And thus this re-recommendation
> > of acceptance.
> > 
> > Please let us know what you think. I will go on holiday after April
> > 4, so I hope to accept this proposal then.
> > 
> > Thanks!
> > Richard
> > 
> > 
> > > On Oct 25, 2021, at 3:24 AM, Spiwack, Arnaud
> > > <arnaud.spiwack at tweag.io> wrote:
> > > 
> > > My weak objections are no match for Simon's strong keenness :-) .
> > > 
> > > I should say that, egoistically, I'd also like 5,6,7 to happen. I
> > > was only expressing concerns about the price.
> > > 
> > > On Fri, Oct 22, 2021 at 1:00 PM Simon Peyton Jones
> > > <simonpj at microsoft.com> wrote:
> > > > I’m in strong support.  This tidies up the design nicely.
> > > >  
> > > > I am particularly keen on 5,6,7; indeed I wrote a whole proposal
> > > > about it, which Vlad has #included here
> > > >  
> > > > https://github.com/ghc-proposals/ghc-proposals/pull/386
> > > >  
> > > > Simon
> > > >  
> > > > PS: I am leaving Microsoft at the end of November 2021, at which
> > > > pointsimonpj at microsoft.com will cease to work. 
> > > > Usesimon.peytonjones at gmail.com instead.  (For now, it just
> > > > forwards to simonpj at microsoft.com.)
> > > >  
> > > > From: ghc-steering-committee
> > > > <ghc-steering-committee-bounces at haskell.org>On Behalf Of Spiwack,
> > > > Arnaud
> > > > Sent: 21 October 2021 08:03
> > > > To: Richard Eisenberg <rae at richarde.dev>
> > > > Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
> > > > Subject: Re: [ghc-steering-committee] #425: invisible binders in
> > > > type declarations; rec: accept
> > > >  
> > > > I'm generally in favour. But I'm not convinced that the secondary
> > > > changes (points 4–7) are worth it. They are certainly better
> > > > place than we are today, but are they worth breaking existing
> > > > code for? Point 5–7 can probably be replaced by warnings. I don't
> > > > know about 4.
> > > >  
> > > > On Tue, Oct 19, 2021 at 11:20 PM Richard Eisenberg
> > > > <rae at richarde.dev> wrote:
> > > > > Hi all,
> > > > > 
> > > > > I am the shepherd for proposal #425,
> > > > > https://github.com/ghc-proposals/ghc-proposals/pull/425,
> > > > > proposing to add invisible binders in type declarations.
> > > > > 
> > > > > The main payload of the proposal is to allow definitions like
> > > > > 
> > > > > > data Proxy @k (a :: k) = Proxy
> > > > > 
> > > > > instead of today's
> > > > > 
> > > > > > data Proxy (a :: k) = Proxy
> > > > > 
> > > > > which has no explicit binding site for k.
> > > > > 
> > > > > This new syntax solves a number of smallish syntax conundra, as
> > > > > very well outlined in the proposal.
> > > > > 
> > > > > In addition, the proposal includes two small unrelated tweaks
> > > > > to the syntax of type family instances; these are points (6)
> > > > > and (7) in the proposal. Both changes will break some obscure
> > > > > (but still realistic, knowing Haskell) programs, but both fixes
> > > > > are backward compatible.
> > > > > 
> > > > > ---
> > > > > 
> > > > > I recommend acceptance. The proposal is motivated nicely (do
> > > > > check out the examples) and solves a real problem. The new
> > > > > syntax fits in with other similar features. The small cleanups
> > > > > to existing syntax will lead to better error messages.
> > > > > 
> > > > > The one drawback, as I see it, is that this proposal includes
> > > > > point (5), which is a breaking change to the way type synonyms
> > > > > work. Right now, we can say
> > > > > 
> > > > > > type P = (Proxy :: k -> Type)
> > > > > 
> > > > > and GHC will infer P :: forall k. k -> Type. Under this
> > > > > proposal, you would have to write
> > > > > 
> > > > > > type P @k = (Proxy :: k -> Type)
> > > > > 
> > > > > bringing k into scope explicitly. The fix is not backward
> > > > > compatible, and so I think this proposal should come with a
> > > > > migration strategy, where we warn about the former version for
> > > > > some releases before banning it. (Continuing to support it is
> > > > > possible, but it's very awkward to have a variable mentioned
> > > > > only in a synonym's right-hand side.)
> > > > > 
> > > > > Sorry for the delay in producing this recommendation!
> > > > > Richard
> > > > > _______________________________________________
> > > > > 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
> 

-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/