[ghc-steering-committee] #370: Syntax for Modifiers, Recommendation: Acceptance

[Eric Seidel]

I'm still a bit skeptical of the specifics around tying modifiers to types, but I think the proposal is well-motivated and that we should find *some* solution before arrows become too complex.

On Mon, Nov 30, 2020, at 14:52, Richard Eisenberg wrote:
> To my surprise, I found myself leaning against. So I updated and 
> simplified the proposal to remove Modifier. This makes modifiers a bit 
> more magical, but more likely to actually work in practice. The type 
> inference story previously may have been intractable.
> 
> I've requested that the committee consider the updates in parallel with 
> community feedback.
> 
> Thanks,
> Richard
> 
> > On Nov 30, 2020, at 2:36 PM, Alejandro Serrano Mena <trupill at gmail.com> wrote:
> > 
> > After some discussion in the GitHub thread, changes are going to arrive to the proposal. I think the best is to send the proposal back to the “Needs revision” state.
> > 
> > Regards,
> > Alejandro
> > 
> > On 29 Nov 2020 at 23:12:44, Eric Seidel <eric at seidel.io> wrote:
> >> I left a few comments and questions on the PR itself, but I'm leaning towards rejecting the proposal in its current form as well. This doesn't (yet) feel like a generic mechanism, in particular because the only modifier that has been specified would be deeply wired into GHC itself.
> >> 
> >> On Fri, Nov 27, 2020, at 04:46, Joachim Breitner wrote:
> >>> Hi,
> >>> 
> >>> Am Donnerstag, den 26.11.2020, 14:58 -0500 schrieb Alejandro Serrano
> >>> Mena:
> >>> > Dear all,
> >>> > This proposal suggests adding syntax for a general notion of
> >>> > modifiers, like the ones we’ve been talking about lately affecting
> >>> > linearity or matchability of arrows. For example, if linear types and
> >>> > unsaturated families are accepted as they stand, we would have `Int
> >>> > #1 -> @U Bool` (or something like that), whereas with this proposal
> >>> > we would have the more uniform `Int %1 %Unmatchable -> Bool`.
> >>> > 
> >>> > Since the amount of modifiers is likely to increase in the future, I
> >>> > think it’s a great idea to agree and reserve such syntax, instead of
> >>> > coming up with different ways on each proposal. I thus recommend
> >>> > acceptance of this proposal.
> >>> > 
> >>> > The proposal itself:
> >>> > (1) introduces syntax for modifiers in types and defines how to
> >>> > type/kind check them,
> >>> > (2) reserved such syntax for other uses in declarations and terms.
> >>> > 
> >>> > I think the proposal still has its merits only with (1), even though
> >>> > I lean towards accepting both parts of it.
> >>> 
> >>> I like the idea of reserving syntax here, but parts of the proposal
> >>> smell a bit like premature generalization to me. Are we confident that
> >>> all annotations we eventually would like to use with this feature can
> >>> be expressed as types of a kind that is an instance of Modifier? Or
> >>> should we reserve the ability to have annotations that don't fit that
> >>> model?
> >>> 
> >>> Would we ever have annotation that may affect phases earlier than than
> >>> typechecking? What if we want to use (%type e) and (%data e) to help
> >>> with the SingleNamepace issues? Look like useful annotations to me, but
> >>> I am not sure if they fit the framework proposed here.
> >>> 
> >>> The fact that we special-case %1 supports that.
> >>> 
> >>> The proposal explicitly has to state “No modifier polymorphism!”. But
> >>> isn't that indication that using the type system to model the various
> >>> modifiers might be the wrong tool?
> >>> 
> >>> I wonder if there is a way where the %(…) on it’s own only reserve
> >>> syntax, and the various uses of that syntax can be disambiguated
> >>> _statically_ based on the content of …. 
> >>> 
> >>> Not great syntax, because not concise, enough, but morally I’d feel
> >>> more at ease with
> >>> 
> >>>   Int %(multiplicity Many) -> Int
> >>>   Int %(multiplicity 1) -> Int
> >>>   Int %(multiplicity m) -> Int
> >>> 
> >>> where multiplicity is a modifier keyword, to express the existing
> >>> features (including implicit generalization of m). Then we can extend
> >>> this to
> >>> 
> >>>   Int %oneShot -> Int
> >>> 
> >>> and
> >>> 
> >>>   Int %(matchability M) -> Int
> >>> 
> >>> and maybe even
> >>> 
> >>>   foo (%type [a]) -- where foo :: forall a -> ()
> >>> 
> >>> which is a modifier that 
> >>> 
> >>> 
> >>> So at the moment, I am inclined to reject this proposal, until I am
> >>> convinced that we are not painting ourselves into a “all modifiers are
> >>> types of special kinds and that’s all the syntax and behaviour we ever
> >>> need” corner.
> >>> 
> >>> Minor detail: If we can annotate infix use of the (->) “type operator”,
> >>> should we also be able to annotate other infix operators, i.e.
> >>> 
> >>>   constr ::= (btype | ! atype) {modifier} conop (btype | ! atype) 
> >>>   infixexp ::= lexp {modifier} qop infixexp
> >>> 
> >>> 
> >>> 
> >>> Cheers,
> >>> Joachim
> >>> 
> >>> 
> >>> -- 
> >>> Joachim Breitner
> >>>   mail at joachim-breitner.de
> >>>   http://www.joachim-breitner.de/
> >>> 
> >>> 
> >>> _______________________________________________
> >>> 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
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>