Linear Types: ready for review

[Wolfgang Jeltsch]

Hi, again!

Here are the missing links to my previous e-mail:

[1] https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437271986
[2] https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476125233

All the best,
Wolfgang

Am Sonntag, den 05.05.2019, 14:02 +0300 schrieb Wolfgang Jeltsch:
> Am Freitag, den 03.05.2019, 11:52 +0200 schrieb Spiwack, Arnaud:
> >   * The file `Multiplicity`, which defines `type Mult = Type`, the 
> >     `Scaled` type and functions unrestricted, linear, pattern
> >      synonyms `One` and `Omega`, quick submultiplicity test submult
> 
> Could `Omega` **please** be changed to `Many`? I argued long time
> ago [1] already why `Omega` seems to be a bad choice and `Many` to be
> a much better alternative. Unfortunately, my arguments, while having
> been positively received, didn’t really have a considerable impact on
> the proposal and implementation; still today the proposal reflects
> only part of them, as it did 1½ months ago [2].
> 
> Notation is important, since good notation aids and bad notation
> confuses. Notation is something that is very likely to stay once it
> has been in use. Given that changing this one identifier shouldn’t be
> a big deal, I’m asking you keenly to make this change.
> 
> Following are my arguments again:
> 
>   1. It’s already questionable that the paper uses the symbol ω. The
>      choice of this symbol stems from its use for the smallest
>      transfinite ordinal number, the number that denotes the length of
>      an infinite list, if you so wish. This doesn’t match the use of ω
>      in this proposal, where it stands for the possibility to use a
>      value *any number* of times and thus rather corresponds to
>      something like ℕ ∪ {ω}.
> 
>   2. Even if ω is considered okay for being used in the theory, we
>      shouldn’t use the identifier `Omega` in Haskell. `Omega` doesn’t
>      name the multiplicity; instead it names the symbol that is used 
>      to denote the multiplicity.
> 
>   3. To people not into something like ordinal numbers or ω-words,
>      `Omega` doesn’t mean anything. Therefore its use would rather
>      confuse than enlighten those people.
> 
> I propose to pick multiplicity identifiers that capture the actual
> meanings of the multiplicities and are consistent with existing
> identifiers at the same time. `Control.Applicative` already uses the
> identifiers `some`, `many`, and `optional`. Thus we should use `Many`
> for what is now called `Omega` and `Optional` for the affinity
> multiplicity in case it’s added at some time. I think `One` is a good
> name and thus should be kept. The 0-multiplicity would probably be
> best named `None`.
> 
> All the best,
> Wolfgang