[ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept
Vladislav Zavialov (int-index)
vlad.z.4096 at gmail.com
Fri Oct 29 15:01:19 UTC 2021
The problem with ‘@‘, as explained by Richard, is cited right next to the Alternative 5.
However, I agree with Eric that the ’type’ herald feels excessive. It’s not something I personally intend to use. However, I remember Simon PJ and Iavor liked it (if I recall correctly), hence its inclusion in the proposal.
I don’t think it hurts either, though. We can accommodate different programming styles.
- Vlad
> On 29 Oct 2021, at 17:53, Simon Peyton Jones via ghc-steering-committee <ghc-steering-committee at haskell.org> wrote:
>
> | 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall,
> | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous
>
> Perhaps it would help, in the proposal, to make explicit the argument *against* using @ as the herald for all type arguments. I remember that there *is* such an argument, and I found it quite convincing, but I can't remember it now. Maybe it is there somewhere?
>
> Vlad/Richard?
>
> Simon
>
> PS: I am leaving Microsoft at the end of November 2021, at which point simonpj at microsoft.com will cease to work. Use simon.peytonjones at gmail.com instead. (For now, it just forwards to simonpj at microsoft.com.)
>
> | -----Original Message-----
> | From: ghc-steering-committee <ghc-steering-committee-
> | bounces at haskell.org> On Behalf Of Eric Seidel
> | Sent: 29 October 2021 02:16
> | To: ghc-steering-committee at haskell.org
> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall"
> | in terms; rec: accept
> |
> | I would still prefer alternative 5 (using @ as the type herald). I
> | really dislike that we would now have three ways to specify a type
> | argument:
> |
> | 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall,
> | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous
> |
> | Ideally I would have single syntax for specifying type arguments,
> | which was historically (1). I know that many people would like to
> | unify the term and type syntaxes, so I'm ok with (2) as well even
> | though the T2T algorithm seemed quite involved. But adding (3) really
> | feels excessive.
> |
> | But I believe I'm a small minority in this opinion, so I don't want to
> | stand in the way of a very useful feature.
> |
> | On Wed, Oct 27, 2021, at 09:56, Richard Eisenberg wrote:
> | > It has been two weeks. I have heard no argument against this
> | proposal,
> | > but Simon Marlow (in the springtime) expressed some puzzlement.
> | Simon,
> | > what are you thinking about this now? With no further response, I
> | will
> | > accept this proposal on Friday.
> | >
> | > Others are also very welcome to chime in!
> | >
> | > Thanks, all!
> | > Richard
> | >
> | >> On Oct 27, 2021, at 5:30 AM, Spiwack, Arnaud
> | <arnaud.spiwack at tweag.io> wrote:
> | >>
> | >> I think that the proposal makes a great job at listing the issues.
> | It's quite transparent about this, I'm not sure what I could add.
> | >>
> | >> On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones
> | <simonpj at microsoft.com> wrote:
> | >>> I was indeed confused! Apologies.
> | >>>
> | >>> But my main point remains: enumerating a list of inconvenient side
> | effects and corner cases would be a great service.
> | >>>
> | >>> Simon
> | >>>
> | >>> PS: I am leaving Microsoft at the end of November 2021, at which
> | >>> point simonpj at microsoft.com will cease to work. Use
> | >>> simon.peytonjones at gmail.com instead. (For now, it just forwards
> | to
> | >>> simonpj at microsoft.com.)
> | >>>
> | >>> | -----Original Message-----
> | >>> | From: Vladislav Zavialov (int-index) <vlad.z.4096 at gmail.com>
> | >>> | Sent: 27 October 2021 10:10
> | >>> | To: Simon Peyton Jones <simonpj at microsoft.com>
> | >>> | Cc: Spiwack, Arnaud <arnaud.spiwack at tweag.io>; Richard
> | Eisenberg
> | >>> | <rae at richarde.dev>; ghc-steering-committee <ghc-steering-
> | >>> | committee at haskell.org>
> | >>> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible
> | "forall"
> | >>> | in terms; rec: accept
> | >>> |
> | >>> | Simon, perhaps you're thinking of another proposal that is
> | >>> | currently under committee's consideration?
> | >>> |
> | >>> | Arnaud was commenting on #281, and you seem to be talking about
> | #425.
> | >>> |
> | >>> | - Vlad
> | >>> |
> | >>> | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc-
> | steering-
> | >>> | committee <ghc-steering-committee at haskell.org> wrote:
> | >>> | >
> | >>> | > There are a lot of inconvenient side effects and corner cases
> | >>> | > > Arnaud, could you enumerate them? Even if (as I strongly
> | >>> | hope) we accept this proposal, it's good to have a concrete
> | list
> | >>> | of things to
> | >>> | bear in mind. I for one do not have such list in my head.
> | >>> | >
> | >>> | > One principle that the proposal espouses (but perhaps does
> | not
> | >>> | call out explicitly) is that it should be possible to write an
> | explicit
> | >>> | binder for every in-scope variable. So instead of
> | >>> | > data T (a :: k -> k) = ... I want to write
> | >>> | > data T @k (a :: k -> k) = ... with an explicit
> | binder
> | >>> | > for k.
> | >>> | >
> | >>> | > So I see the proposal as removing an ad-hoc wart in the
> | language.
> | >>> | But I may be blind to the "inconvenient side effects and corner
> | cases"
> | >>> | and I'd welcome a list of such cases.
> | >>> | >
> | >>> | > Simon
> | >>> | >
> | >>> | >
> | >>> | > PS: I am leaving Microsoft at the end of November 2021, at
> | >>> | which point > simonpj 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: 27 October 2021 09:20 > To: Richard Eisenberg
> | >>> | <rae at richarde.dev> > Cc: ghc-steering-committee
> | >>> | <ghc-steering-committee at haskell.org>
> | >>> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible
> | >>> | "forall"
> | >>> | > in terms; rec: accept
> | >>> | >
> | >>> | > I've been struggling to have an opinion on this PR. I'm very
> | >>> | sympathetic to the goal of the proposal (and this latest
> | rendition
> | >>> | of the proposal is a really good document). There are a lot of
> | >>> | inconvenient side effects and corner cases (but, to be fair,
> | these
> | >>> | are not special to this proposal: they are inherent to the
> | >>> | dependent types plan). But I'm fairly convinced that this is
> | the
> | >>> | best possible approach, or close enough.
> | >>> | >
> | >>> | >
> | >>> | >
> | >>> | > So yes, I don't really feel strongly about it. But on
> | balance,
> | >>> | I think that I'm in favour.
> | >
> | > _______________________________________________
> | > ghc-steering-committee mailing list
> | > ghc-steering-committee at haskell.org
> | >
> | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail
> | > .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-
> | committee&a
> | >
> | mp;data=04%7C01%7Csimonpj%40microsoft.com%7C69ae5d5e09784d08370708d99a
> | >
> | 79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637710670242799539
> | >
> | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I
> | >
> | k1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3QCuMUXrxSwl
> | > cjEH89KLcy5A%3D&reserved=0
> | _______________________________________________
> | ghc-steering-committee mailing list
> | ghc-steering-committee at haskell.org
> | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail
> | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-
> | committee&data=04%7C01%7Csimonpj%40microsoft.com%7C69ae5d5e09784d0
> | 8370708d99a79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6377106
> | 70242799539%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz
> | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3
> | QCuMUXrxSwlcjEH89KLcy5A%3D&reserved=0
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
More information about the ghc-steering-committee
mailing list