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

[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/