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

Wed Aug 15 02:16:33 UTC 2018

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-committee
> >
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee