I've got to say that I'm rather uncomfortable with the type-based meaning ascription of this proposal.

That being said, we do need a lightweight way to add such modifiers to arrows (and anything which can appear to the left of an arrows such as fields of data constructors, whether in record notation or not (though I'm fine with requiring GADT notation when not a record, that's what we did with Linear Types)). There is a staggering amount of possible such modifiers which have been conceptualised.

By far, this is the least awful such proposal that I've seen. It's the first time that such a proposal looks even remotely usable.

So the pragmatic in me is inclined to accept as well.

The need for such a lightweight mechanism to annotate terms, though, is quite a bit less clear to me. Because type disambiguation is rather novel in GHC, I'd rather be prudent in this area, and stage the term bits as future work. Keep the design, and revisit it once we have experience with the mechanism for arrow modifiers.

On Thu, Nov 26, 2020 at 8:58 PM Alejandro Serrano Mena <trupill@gmail.com> 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.

Regards,
Alejandro

On 21 Nov 2020 at 10:07:18, Joachim Breitner <mail@joachim-breitner.de> wrote:
Dear Committee,

this is your secretary speaking:

A syntax for modifiers
has been proposed by Richard Eisenberg (this time it’s true)
https://github.com/ghc-proposals/ghc-proposals/pull/370
https://dfinity.slack.com/archives/C01BJ73A893/p1605922403340800?thread_ts=1605913774.336600&cid=C01BJ73A893

I’ll propose Alejandro as the shepherd, as he has looked at i
t in detail already.

Please guide us to a conclusion as outlined in
https://github.com/ghc-proposals/ghc-proposals#committee-process

Thanks,
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