[ghc-steering-committee] Linear types design decisions

[Richard Eisenberg]

Hi committee,

As the shepherd for the Linear Types proposal (https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst <https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst>), I've been asked to forward a few design decisions to this committee. These are outlined in https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476276874 <https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476276874>, but this email is meant to be mostly self-contained on the issues to consider. We have three main issues before us. I describe the issues first, and then make recommendations separately.

1. The concrete syntax for linear types. The current proposal is:

- `arg # mult -> res` for arrow types. That is, `... # ... -> ...` essentially becomes a ternary operator in the language. There is a proposed BNF of this syntax at https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id26 <https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id26>, but as of this writing, that BNF is, I believe, ambiguous for an input like `Int # Omega -> Int -> Int`, where the first arrow might or might not be part of the multiplicity. We clearly want "not", but the BNF does not currently reflect that. I am asking for Arnaud to take another stab. There is no treatment that I see of what to do if an upstream module declares a type operator named (#), but that shouldn't be hard to resolve, either by using prefix notation (#) or a qualified name Int Foo.# Bool.

- `field # mult :: ty` for record field declarations and `pat # mult :: ty` for pattern bindings. This reverses the previous order. Also, because the `:: ty` is optional for a pattern binding, there is a potential ambiguity there, too, for `x # One = blah`: is that a pattern binding for x or a function binding for the term-level (#)? Presumably, the latter, and perhaps the former should require parentheses. (But note that `x :: Int = 5` is allowed today, without parens.)

- The abbreviation #-> (one lexeme) for `# One ->`. I suppose this could just be an ordinary type-level operator exported from some module, but the proposal does not address this point. (Indeed, the proposal does not really propose this abbreviation -- only the commentary does. But we have been asked to decide on how to update the proposal.)

- NB: The proposal introduces FUN :: Multiplicity -> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep). TYPE r1 -> TYPE r2 for the full raw function type.

Some alternatives are at https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id58

2. How to update Template Haskell.

- Should ArrowT be updated somehow? Or should we have a new MulArrowT (that presumably takes three arguments), leaving ArrowT alone?

- What happens when we reify a constructor? TH's Info type contains `DataConI Name Type ParentName`, which is returned when reifying a constructor. Recall that, with linear types, constructors are multiplicity-polymorphic. Should that be reflected in the Type in the DataConI? Or do we keep things simpler? Does it depend on whether -XLinearTypes is on?

- What happens when we reify a function? If the function is, say, multiplicity-polymorphic and we reify it in a module without -XLinearTypes, what do we see? Do we see the multiplicity polymorphism?

3. What to name the unrestricted multiplicity. Is it Omega or Many?

--------------------
Recommendations:

1. I recommend accepting the new syntax (provided we can sort out the BNF). I don't think I can top the argument in favor of this syntax at https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437512457 <https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437512457> so I won't try.

2.
- I would leave ArrowT as-is and introduce a new three-paramater MulArrowT in TH's Type datatype. ArrowT is heavily used in TH code, and it seems willfully destructive to change it. TH's syntax is already not-orthogonal in countless ways, and I think this is a fine time to add another.
- I recommend that the behavior of reification be independent of what extensions are enabled. Otherwise, the possibilities for confusion and mistakes abound.
- The subtleties of constructor types are described at https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id29 <https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id29>   If I understand this correctly, this section means that constructors cannot be classified by normal Haskell types any more, but instead need some other descriptor. The best route forward, then, is to update DataConI to be able to describe data constructors correctly, perhaps by using TH's `Con` type. This would be a breaking change, but it seems worthwhile.
- Functions should be reified with their multiplicities intact.

It's unclear how much the change in reification would break existing code. I recommend that, once this is implemented, we run smoke tests (compiling all of Stackage is a good way to do this) to determine the extent of the breakage. If things are bad, we can reconsider.

3. Many. It's very easy for us pointy-headed types to use fancy Greek things that look, well, Greek to everyone else. `Many` is potentially misleading is that something used `Many` times might actually be used 0 times. `Unrestricted` is really a mouthful though, and I don't think it will be hard for users to internalize that `Many` just means an undetermined amount.

Let me know your thoughts on these points. As usual, silence will be taken to mean that you agree with my recommendations.

Thanks,
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190502/8afd9f80/attachment-0001.html>