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

Hi, thanks, that’s better. It is still a pretty generic bet on the future (here is a general syntax that we now hope will be useful for multiple things that we don’t even know about yet). But that’s fine, especially if the bet wins. Do we actually need a dedicated language extension for it, though? Why not make this proposal “from now on, LinearHaskell uses this syntax, and we plan to use compatible syntax for other extensions”? (this is all there effectively really is, isn’t it? a tweak to LinearHaskell, and a pledge to follow this pattern) Cheers, Joachim Am Donnerstag, den 03.12.2020, 12:16 -0800 schrieb Alejandro Serrano Mena:

Dear Committee,

Richard has requested for us to consider the new version of this proposal. As opposed to the previous version, this one is only about reserving syntax for “modifiers”, which at the beginning would be used for things like linearity or matchability of arrows.

I think this is a good proposal, and one which would save us from re-considering syntax for every possible extension (and if linearity appears before the arrow and matchability after it, where would a future dimension go?). Thus I keep recommending acceptance on this new incarnation.

Regards, Alejandro

On 30 Nov 2020 at 20:52:26, 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 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 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:

...

...

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

Hi, Am Donnerstag, den 26.11.2020, 14:58 -0500 schrieb Alejandro Serrano Mena: 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@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

---

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/