<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 9 July 2018 at 04:41, Richard Eisenberg <span dir="ltr"><<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I have volunteered to shepherd Proposal #111: Linear Types. The pull request is here: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/111" rel="noreferrer" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals/pull/<wbr>111</a><br>
<br>
The authors propose adding linear functions to GHC. The argument to a linear function must be used exactly once in the function body. Motivation for this feature abounds -- essentially, linear types allow for better static checking around resource allocation and deallocation. I refer you to the proposal (and published paper) for more details here. The proposal also contains multiplicity polymorphism, where a higher-order function can be polymorphic in the multiplicity of a supplied function. Datatypes are linear by default, with a long list of (in my opinion, non-obvious) rules around syntax and exceptions to those rules. Constructors have a different multiplicity when used in an expression than they do when used in a pattern, for example. The authors leave type inference as an open question and do not state how the feature would work with either view patterns or pattern synonyms. The proposal comes with a companion document detailing the changes to Core. These changes seem appropriate.<br>
<br>
The current proposal has a fair number of open questions. I've written a long comment on the GitHub trail detailing what I was uncertain of. The proposal is not currently near the level of crispness of the proposals we normally accept. For a smaller proposal, I would just send it back to the authors without really giving it to the committee. However, there has been a great deal of effort behind writing this proposal and building an implementation, and so I think it's only fair that we give some thought about the general direction being worked in here.<br>
<br>
As to the features themselves: I'm personally far from convinced. Though I see no better way to achieve the authors' goals, the feature they have proposed is full of both sharp and dark corners. If implemented, there would be regular questions cropping up as to why such-and-such is the case or why the design is the way it is. However, this is well motivated and eagerly anticipated. And I don't think we'll be able to conjure up a better design without gaining experience with the proposed design, however flawed.<br></blockquote><div><br></div><div>I'm feeling somewhat concerned about the power-to-weight ratio of linear types, especially given that it doesn't cover exceptions.</div><div><br></div>Speaking with my industrialist hat on, as I look at our sprawling system with a huge number of explicitly-managed resources, I should be squarely in the target audience, but I'm not sure that linear types are going to help us all that much.  Most resources are allocated with a bracket pattern (bracket allocate deallocate $ \resource -> do ...) or using a withFoo combinator.  These give clear scoping and exception-safety to resource allocation, and linear types don't offer any safety improvements here - as I understand it the bracket pattern will remain the safest way to manage explicit resources in cases where it can be used. Files are not typically opened and closed using separate 
operations, people use the withFile combinator, because it's much easier
 to get right. The same goes for most resources - common practice is to 
expose a withFoo combinator for every explicitly managed resource.<br><br><div>In our system there are a few places where the bracket pattern doesn't fit. The ones that spring to mind are where resources are allocated in C++ and released in Haskell or allocated in Haskell and then released in a different Haskell thread after receiving a message from C++. Linear types might help model correct lifetime in these cases, but our experience has been that safety in these cases has only been an issue where exceptions are concerned - and linear types doesn't help with that.  In the case of receiving a resource from C++ I need to carefully use Control.Exception.mask and an exception handler to avoid leaks, which is by far the hardest thing to get right. I would love to have some static checking that this was done correctly throughout our codebase.<br></div><br><div>Perhaps what I should do is a complete audit of our codebase to evaluate the opportunities for linear types to help.<br></div><div><br></div>I understand there are other motivations beyond explicit resource management. But resource management is a big one, and it seems like linear types don't help in some large fraction of cases, yet it's a deeply invasive change. That worries me quite a lot.</div><div class="gmail_quote"><br></div><div class="gmail_quote">(of course none of this should stop experimentation, but if we're taking the temperature of the committee, currently I'm somewhat lukewarm)<br></div><div class="gmail_quote"><br></div><div class="gmail_quote"><div>Cheers</div><div>Simon<br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I thus recommend: Encouragement to continue the proposal and implementation, with an eye toward acceptance. Furthermore, if/when merged, I would like to advertise that the feature is subject to change, with no backward compatibility guarantee, for several versions. If the feature is implemented and merged, we will learn more about it and then perhaps refine it in the future.<br>
<br>
Richard<br>
______________________________<wbr>_________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@<wbr>haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-<wbr>steering-committee</a><br>
</blockquote></div><br></div></div>