[ghc-steering-committee] Proposal #111: Linear Types

[Simon Marlow]

On 9 July 2018 at 04:41, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:

> I have volunteered to shepherd Proposal #111: Linear Types. The pull
> request is here: https://github.com/ghc-proposals/ghc-proposals/pull/111
>
> 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.
>
> 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.
>
> 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.
>

I'm feeling somewhat concerned about the power-to-weight ratio of linear
types, especially given that it doesn't cover exceptions.

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.

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.

Perhaps what I should do is a complete audit of our codebase to evaluate
the opportunities for linear types to help.

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.

(of course none of this should stop experimentation, but if we're taking
the temperature of the committee, currently I'm somewhat lukewarm)

Cheers
Simon

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.
>
> Richard
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180709/0d7d696b/attachment-0001.html>