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

[Simon Peyton Jones]

Richard writes

|  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 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.

I'm mostly with Richard here.  Linearity is a "big feature".  We have to change Core, and that's something we do very seldom.  (The TypeInType stuff is comparable.)

I'm a bit more positive than Richard.  I've spent years looking for a way to make sense of linearity, and this is the first time I have seen a proposal that
- fits with the language
- looks as if it could pay its way

But it is "big" and without experience we don’t have a good way to evaluate it.  It's a chicken and egg problem: we can't get that experience without trying it.  Neither the costs nor the benefits are apparent yet.  But it's too interesting to drop.

I think we should be encouraging.  The next hurdle is to see whether the implementation turns out reasonable, or if it litters the compiler with ad-hoc gubbins. We'll see.  Matthew is on the job.

Declaration of interest: I'm a co-author.

Simon

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On
|  Behalf Of Richard Eisenberg
|  Sent: 09 July 2018 04:42
|  To: ghc-steering-committee <ghc-steering-committee at haskell.org>
|  Subject: [ghc-steering-committee] Proposal #111: Linear Types
|  
|  I have volunteered to shepherd Proposal #111: Linear Types. The pull request
|  is here:
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%
|  2Fghc-proposals%2Fghc-
|  proposals%2Fpull%2F111&data=02%7C01%7Csimonpj%40microsoft.com%7C90f84d3b
|  5c3b42dfa7b108d5e54de405%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636667
|  045071264050&sdata=EB82E10Yedfp0E83OuTjK5F%2BfHX7CHKP%2Fuf7NRytlxM%3D&am
|  p;reserved=0
|  
|  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 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