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

[Simon Peyton Jones]

Reasonable questions -- maybe put them on the GitHub thread so that Arnaud can respond.

|  2. Am I correct in understanding that the only way to guarantee resource
|  safety in this proposal is to write all allocation functions in CPS with a
|  linear continuation? If so, this seems to be a substantial divergence from
|  the intuitive notion of type safety.

It's more modular than that.  In the paper we give the API for mutable arrays.  Yes, the ability to do in-place update on those arrays depends on that API; the type system along does not guarantee it.  It's the type system plus the API.   But its guarantees do not depend on *other* allocators.

|  The linearity-in-the-kind and uniqueness
|  alternatives (I don't quite understand the difference) seem better in this
|  respect; I want ALL sockets/handles/MArrays/etc to be linear.

These all have big problems too.  It's a big fork in the road; our paper takes one fork.  Maybe there are better paths.  But none that I have seen.

The challenge is that we don't know a Best Way with certainty (yet anyway).  But it's worth trying out at least One Way.  If someone else has a well-worked out alternative design, let's discuss that too.

Simon

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On
|  Behalf Of Eric Seidel
|  Sent: 15 August 2018 03:17
|  To: ghc-steering-committee at haskell.org
|  Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types
|  
|  I also have a few concerns about the proposal.
|  
|  1. The proposal suggests making all data constructors linear when -
|  XLinearTypes is disabled. Can we guarantee that this will not cause
|  multiplicities to leak into type errors where -XLinearTypes is disabled? The
|  proposal doesn't say, and Richard seems to think not based on his email
|  above. I can understand having to deal with linearity if I've imported
|  modules that use -XLinearTypes, but not if I just use types that were
|  silently inferred to be linear. -XLinearTypes ought to be opt-in.
|  
|  2. Am I correct in understanding that the only way to guarantee resource
|  safety in this proposal is to write all allocation functions in CPS with a
|  linear continuation? If so, this seems to be a substantial divergence from
|  the intuitive notion of type safety. I don't have to worry about my API
|  design to ensure my program won't segfault, GHC guarantees that for me (and
|  we give the inevitable escape hatches scary names). Similarly, I think users
|  will expect GHC to prevent them from writing programs that misuse resources,
|  but this guarantee is only provided if the API is designed correctly, ie
|  with CPS'd allocators. We don't generally think of type safety as being
|  conditional on API design. The linearity-in-the-kind and uniqueness
|  alternatives (I don't quite understand the difference) seem better in this
|  respect; I want ALL sockets/handles/MArrays/etc to be linear.
|  
|  I wonder if we could somehow take advantage of the fact that allocators are
|  already implicitly CPS'd (as monadic functions) to allow users to write code
|  in the natural style while retaining the linear guarantees?
|  
|  On Tue, Aug 7, 2018, at 01:50, Iavor Diatchki wrote:
|  > Hello,
|  >
|  > I am not sure that the amount of effort that went into writing a
|  > proposal should be a deciding factor about if the proposal is
|  > accepted.  We don't want to discourage folks, but also, once things
|  > get into GHC they are hard to get out, so I think caution is warranted.
|  >
|  > I find this proposal to be constructed rather poorly.  I read the
|  > previous version, and I also read this one, and I find it to be a
|  > rather small improvement, if at all.  For a relatively complex
|  > proposal change, the proposal had hardly any examples.  To me, it read
|  > as a patchwork of paragraphs, that are an uneasy mix of informal
|  > explanations with no examples, overly formal explanations, potential
|  > things one might use this for (RIO??), and what seem to be answers to
|  > questions from the GitHub discussion, which are just perplexing if you
|  > read the proposal before the discussion.
|  >
|  > This makes it quite hard to grasp the main idea.  Having said that I
|  > think I get what is being proposed and I like parts of it.
|  >
|  > The main high level concern I have is the overloading of the function
|  > space arrow.  We already have it overloaded in all kinds of ways, and
|  > adding one more dimension without any kind of underlying system seems
|  > too much.  I am not at all convinced that we will be able to "hide"
|  > multiplicities when the extension is not enabled.
|  >
|  > Overall, while I like the core ideas, I would prefer a different way
|  > of integrating them into Haskell, one that is more modular, even at
|  > the cost of having to duplicate some code.  My reasoning is that while
|  > linearity might be useful in some cases, most of the time it is not
|  > something that we'd care about much, so we should not add it (at least
|  > straight away) to the core part of the language (functions and data
|  types).
|  >
|  > -Iavor
|  >
|  >
|  > On Fri, Aug 3, 2018, 1:41 AM Richard Eisenberg <rae at cs.brynmawr.edu>
|  wrote:
|  >
|  > > Conversation seems to have died down on this trail, both on GitHub
|  > > and here in committee. As the shepherd, it's my job to kick us back into
|  action.
|  > >
|  > > After much conversation on GitHub, there are still a few dangling
|  > > loose ends to this proposal:
|  > >
|  > > - The proposal defined *consume exactly once*, but I don't that
|  > > definition is fully correct and it's not general enough. For
|  > > example, it doesn't treat abstract types or unboxed ones. Simon has
|  > > suggested that it's meant purely for intuition (for which it works
|  > > well) but is not meant to be a technical specification. The other
|  > > proposal authors seem to disagree with this, but I'm yet to be satisfied
|  by an attempt at defining this.
|  > >
|  > > - The proposal says nothing on the subject of type inference. This
|  > > is understandable, because it's really hard to know what will work best.
|  > > However, there has not yet been a commitment that type inference
|  > > will be backward-compatible. The authors want the presence/absence
|  > > of -XLinearTypes not to affect type inference, and they also want
|  > > sometimes to infer linear types. I think these, together, imply that
|  > > the proposal isn't fully backward compatible. See
|  > > https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment
|  > > -406723478
|  > >
|  > > - The proposal mentions the idea of unification of multiplicities up
|  > > to semiring equalities, but then the authors claim that such a
|  > > procedure is undecidable. It's unclear where this stands.
|  > >
|  > > - There is no design that will stop Haskell learners from seeing
|  > > linear types in error messages, though it appears they won't appear with
|  :type.
|  > >
|  > > - Simon M has pushed on the motivations of the proposal, trying to
|  > > understand better exactly what problems this proposal solves. I have
|  > > not followed this sub-thread terribly closely, and will take
|  > > advantage of the fact that Simon is on this committee and can speak
|  > > for himself on these issues.
|  > >
|  > > Despite these dangling pieces, I do think they all can be resolved.
|  > > (Except perhaps the motivation piece if it's problematic enough.) I
|  > > thus recommend that we officially encourage this proposal on the
|  > > road toward acceptance. This recommendation is based on the
|  > > excitement in the community around linear types and the high degree
|  > > of effort and commitment the authors have shown.
|  > >
|  > > If you disagree with this recommendation, please speak up. As usual,
|  > > I will take silence as agreement and make an official pronouncement
|  > > to the authors in due course.
|  > >
|  > > Thanks,
|  > > Richard
|  > >
|  > > On Jul 8, 2018, at 11:41 PM, 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 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-commi
|  > > ttee
|  > >
|  > _______________________________________________
|  > ghc-steering-committee mailing list
|  > ghc-steering-committee at haskell.org
|  > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ
|  > ee
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee