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

The proposal mentions pedagogy at least twice. As an educator I'd like to raise my voice in this discussion. 1) The proposal says However, for pedagogical reasons, to prevent linear types from interfering with newcomers' understanding of the Prelude, this proposal does not modify base. Instead, we expect that users will publish new libraries on Hackage including more precisely typed base functions. I believe these reasons are somewhat misleading. I am not sure that not having linear arrows in base is better than having another "better" base with linear arrows there. Anyway, authors says that it's inevitable to change type of ($). Well, why not change other functions then? As long as authors struggle for hiding linear arrows in printing it's perfectly alright to have that stuff in base thus avoiding having another base. 2) I'd like to see examples of :type output and error messages in the absence of -XLinearTypes in the proposal. These examples should be respected then very carefully in the implementation. I am not satisfied with the guarantees given in This proposal tries hard to make the changes unintrusive to newcomers, or indeed to the existing language ecosystem as a whole. As for the committee recommendation, I don't understand the meaning of "the road towards acceptance". Doesn't it mean discussing the proposal forever? I think we should accept it instead as it is or at least set strict timeframe for the final decision. Regards, Vitaly On Thu, Aug 2, 2018 at 3:41 PM Richard Eisenberg 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-4067234...

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