<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi committee,<div class=""><br class=""></div><div class="">As the shepherd for the Linear Types proposal (<a href="https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst" class="">https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst</a>), I've been asked to forward a few design decisions to this committee. These are outlined in <a href="https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476276874" class="">https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476276874</a>, 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.</div><div class=""><br class=""></div><div class="">1. The concrete syntax for linear types. The current proposal is:</div><div class=""><br class=""></div><div class="">- `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 <a href="https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id26" class="">https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id26</a>, 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.</div><div class=""><br class=""></div><div class="">- `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.)</div><div class=""><br class=""></div><div class="">- 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.)</div><div class=""><br class=""></div><div class="">- NB: The proposal introduces FUN :: Multiplicity -> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep). TYPE r1 -> TYPE r2 for the full raw function type.</div><div class=""><br class=""></div><div class="">Some alternatives are at <a href="https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id58" class="">https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id58</a></div><div class=""><br class=""></div><div class="">2. How to update Template Haskell.</div><div class=""><br class=""></div><div class="">- Should ArrowT be updated somehow? Or should we have a new MulArrowT (that presumably takes three arguments), leaving ArrowT alone?</div><div class=""><br class=""></div><div class="">- 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?</div><div class=""><br class=""></div><div class="">- 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?</div><div class=""><br class=""></div><div class="">3. What to name the unrestricted multiplicity. Is it Omega or Many?</div><div class=""><br class=""></div><div class="">--------------------</div><div class="">Recommendations:</div><div class=""><br class=""></div><div class="">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 <a href="https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437512457" class="">https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437512457</a> so I won't try.</div><div class=""><br class=""></div><div class="">2.</div><div class="">- 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.</div><div class="">- I recommend that the behavior of reification be independent of what extensions are enabled. Otherwise, the possibilities for confusion and mistakes abound.</div><div class="">- The subtleties of constructor types are described at <a href="https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id29" class="">https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst#id29</a> 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.</div><div class="">- Functions should be reified with their multiplicities intact.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Let me know your thoughts on these points. As usual, silence will be taken to mean that you agree with my recommendations.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div></body></html>