[ghc-steering-committee] Please review #641: Wildcard binders in type declarations
Adam Gundry
adam at well-typed.com
Tue Mar 26 21:12:29 UTC 2024
The examples with redundant parentheses or duplicate kind signatures are
not very compelling, indeed. But if I understand correctly, this
proposal also permits using a wildcard binder for a visibly-quantified
variable, like this:
type T :: forall k (a :: k) -> Type
data T _ _ where
MkT :: T _ _
While this is not exactly an essential feature (one can work around it
by giving unused names), it seems a more reasonable thing to want.
I doubt the impact on TH will be very significant if we use pattern
synonyms to support the old constructors.
Adam
On 22/03/2024 18:19, Simon Peyton Jones wrote:
> >From my understanding the biggest argument against this is the
> change in
> template-haskell?
>
>
> Not specifically. My reservation is that
>
> * it's an unforced change,
> * with no user demand
> * but some real user impact (you mention TH)
> * and some implementation cost (modest but very non-zero)
> * aiming to anticipate as-yet-unknown future requirements
>
> That's not a combination I like. Pain now for possible (but uncertain)
> gain in the future.
>
> I don't object to making types and terms behave similarly -- indeed I
> have invested lots of time working with Richard, Vlad, Andrei and others
> on proposals and MRs that move in this direction. I'm just very
> unconvinced about *this *proposal.
>
> One minor point. In patterns we allow this:
> f ((,) @Int @[a] x y) = ...
> Here the type arguments are not type variables but full-blown types, and
> of course nested parens etc come "for free". But this proposal concerns
> data type declarations in which we definitely don't want fulll-blown
> types. So it's more than a "terms and types should be the same" discussion.
>
> Simon
>
>
>
> On Fri, 22 Mar 2024 at 14:47, Malte Ott <malte.ott at maralorn.de
> <mailto:malte.ott at maralorn.de>> wrote:
>
> From my understanding the biggest argument against this is the
> change in
> template-haskell?
> I am wondering how many users will actually be affected by that.
> TypeAbstractions are quite recent so I wouldn’t be surprised if not much
> template-haskell code is using the corresponding constructors.
> That might also be an argument to do this change now before the
> ecosystem has
> more time to settle on this.
>
> Simon, I am also curious. Why are you not convinced by the goal to
> make types
> and terms as similar as possible?
>
> Best
> Malte
>
> On 2024-03-22 14:23, Arnaud Spiwack wrote:
> > I'm happy to follow you on this. Especially since in the future
> that Vlad
> > hopes, where there'd be less difference between terms and types, this
> > particular feature may fall naturally, so it may be worth
> revisiting then
> > rather than paying the cost now.
> >
> > On Fri, 22 Mar 2024 at 09:53, Simon Peyton Jones <
> > simon.peytonjones at gmail.com <mailto:simon.peytonjones at gmail.com>>
> wrote:
> >
> > > Do you worry about the implementation because of future
> maintenance costs?
> > >> Or because of the immediate cost of developing the feature?
> > >
> > >
> > > Mostly the former. It's just a bit more un-forced complexity.
> > >
> > > As far as I can see, there aren't other objections to this
> design besides
> > >> the cost, right? There's no real possibility of an alternate,
> conflicting
> > >> design for data type arguments, is there?
> > >>
> > >
> > > It's just Occam's razor. No one is asking for this. And I'm
> unconvinced
> > > by "future proofiing" because it's hard to correctly anticipate
> the future.
> > >
> > > Simon
> > >
> > > On Fri, 22 Mar 2024 at 08:13, Arnaud Spiwack
> <arnaud.spiwack at tweag.io <mailto:arnaud.spiwack at tweag.io>>
> > > wrote:
> > >
> > >> Simon,
> > >>
> > >> Do you worry about the implementation because of future
> maintenance
> > >> costs? Or because of the immediate cost of developing the feature?
> > >>
> > >> As far as I can see, there aren't other objections to this
> design besides
> > >> the cost, right? There's no real possibility of an alternate,
> conflicting
> > >> design for data type arguments, is there?
> > >>
> > >> On Thu, 21 Mar 2024 at 10:57, Simon Peyton Jones <
> > >> simon.peytonjones at gmail.com
> <mailto:simon.peytonjones at gmail.com>> wrote:
> > >>
> > >>> Dear Steering Committee
> > >>>
> > >>> Vlad proposes to amend proposal #425
> > >>>
> <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>>to
> > >>> permit more wildcard binder forms in type declarations:
> > >>> https://github.com/ghc-proposals/ghc-proposals/pull/641
> <https://github.com/ghc-proposals/ghc-proposals/pull/641>
> > >>>
> > >>> You may find it easiest to look at the rich diff
> > >>>
> <https://github.com/ghc-proposals/ghc-proposals/pull/641/files?short_path=cb2a762#diff-cb2a762676d938436a07317bbd007570b5efdfa00b40763b897ee920694bcbb5 <https://github.com/ghc-proposals/ghc-proposals/pull/641/files?short_path=cb2a762#diff-cb2a762676d938436a07317bbd007570b5efdfa00b40763b897ee920694bcbb5>>
> > >>> .
> > >>>
> > >>> This is a pretty small generalisation which would allow
> > >>>
> > >>> data T (( (a :: k1) :: k2)) = ...
> > >>>
> > >>> in which the binder has multiple kind signatures and
> redundant parens.
> > >>> The change is *not driven by user need*, but rather solely by
> > >>> *uniformity*: these same forms are permitted in function
> definitions:
> > >>>
> > >>> f :: forall (a :: k). blah
> > >>> f @(((a::k1)::k2))) = ...
> > >>>
> > >>> is permitted.
> > >>>
> > >>> It imposes a change on Template Haskell syntax too.
> > >>>
> > >>> The implementation becomes a bit more complicated; more
> recursive data
> > >>> types, etc. Nothing hard, but more.
> > >>>
> > >>> It's not a big deal either way. Very few people expressed a
> view on
> > >>> GitHub. My personal view is that the modest (albeit
> non-zero) gain does
> > >>> not justify the definite (albeit modest) pain. I would leave
> this until
> > >>> someone actually wants it.
> > >>>
> > >>> Vlad argues for future-proofing, but my experience is that an
> eye to the
> > >>> future is sensible when you are making changes anyway; but
> making unforced
> > >>> changes solely for the future risks incurring pain now that,
> when the
> > >>> future comes, turns out to have been a poor investment. We
> may have
> > >>> correctly anticipated, or we may not.
> > >>>
> > >>> So my recommendation is to park this until we get a real user
> demand.
> > >>>
> > >>> It's a perfectly sensible proposal, but adopting it is a
> judgement call.
> > >>> I'll leave a week for committee responses, and then we can
> just vote.
> > >>>
> > >>> Simon
> > >>>
> > >>> On Thu, 21 Mar 2024 at 08:07, Adam Gundry
> <adam at well-typed.com <mailto:adam at well-typed.com>> wrote:
> > >>>
> > >>>> Dear Committee,
> > >>>>
> > >>>> Vlad proposes to amend proposal #425 to permit more wildcard
> binder
> > >>>> forms in type declarations:
> > >>>>
> > >>>> https://github.com/ghc-proposals/ghc-proposals/pull/641
> <https://github.com/ghc-proposals/ghc-proposals/pull/641>
> > >>>>
> > >>>> I'd like to nominate Simon PJ as the shepherd.
> > >>>>
> > >>>> Please guide us to a conclusion as outlined in
> > >>>>
> https://github.com/ghc-proposals/ghc-proposals#committee-process
> <https://github.com/ghc-proposals/ghc-proposals#committee-process>
> > >>>>
> > >>>> Cheers,
> > >>>>
> > >>>> Adam
--
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
More information about the ghc-steering-committee
mailing list