[ghc-steering-committee] Proposal #356: new syntax for linear arrows

[Spiwack, Arnaud]

After looking at the renderings in
https://github.com/ghc-proposals/ghc-proposals/pull/356#issuecomment-690221468
, I do prefer `^` over `%`. Not very strongly either.

On Mon, Sep 14, 2020 at 6:23 PM Joachim Breitner <mail at joachim-breitner.de>
wrote:

> How annoying, how can I now say “I’m trusting the shepherd’s
> judgement” … ;-)
>
> I guess in that case I’ll say I’m trusting Simon PJ, and will go with
> his vote, as I have no strong opinion of my own.
>
> Cheers,
> Joachim
>
>
> Am Sonntag, den 13.09.2020, 22:12 +0000 schrieb Richard Eisenberg:
> > Hi committee,
> >
> > Mathieu Boespflug has proposed a new syntax for linear arrows:
> https://github.com/ghc-proposals/ghc-proposals/pull/356
> >
> > Currently (from the original linear types proposal), we have #-> to
> denote a linear function, and # m -> to denote an arbitrary function whose
> argument has multiplicity m. This proposal suggests three changes:
> >
> > 1. Drop #-> entirely.
> > 2. Use ^ instead of # in the second form, but require that it be a
> *prefix* usage of ^ (that is, the character after the ^ must not be
> whitespace).
> > 3. Introduce a new lexeme ^1 that is used to denote linear functions.
> > Alternative: use % in place of ^; % is observed to be more visually
> apparent in some fonts than ^.
> >
> > In time, the hope is that rule (3) will no longer be needed, if we gain
> overloaded numbers at the type level (when 1 :: Multiplicity will
> type-check without a special rule).
> >
> > Motivations for this change come from the experience within Tweag of
> using linear types. The change away from # also is to avoid a conflict with
> overloaded labels, once those are allowed in types.
> >
> > The hope is that we can make a decision about this in time for release
> with GHC 9.0. This proposal is already implemented:
> https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4020
> >
> > In conflict with our usual protocol, I will not make a recommendation on
> this proposal, as I am conflicted with the proposer. However, I do hope
> that we can come to a conclusion on this quickly, to avoid making a
> backward-incompatible change after a release.
> >
> > We have four options:
> > A. Keep the syntax as it is.
> > B. Choose to go with ^
> > C. Choose to go with %
> > D. Choose to go with some other symbol. I don't think there is any
> particular preference for any one symbol over another.
> >
> > Richard
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> --
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20200915/1684dd85/attachment.html>