Linear Types: ready for review

[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