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@haskell.org> On | Behalf Of Eric Seidel | Sent: 15 August 2018 03:17 | To: ghc-steering-committee@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@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@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@haskell.org | > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-commi | > > ttee | > > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ | > ee | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee