I don’t think relegating an accepted proposal to a fork is a reasonable alternative. Why go through the, for a large proposal, rather painful proposal process just so that you can do what you can also do without that blessing? In fact, if we are going to take that stance, I think, we will seriously discourage contributions to GHC that involve more substantial language changes. I think that would be a very bad development as it makes GHC a much less attractive vehicle for that sort of research. By their nature, proposals that fall into that category (that they have a serious impact on GHC) are also the ones that are the most painful to maintain as a fork. Serious impact means a large overlap with central elements of the compiler, which are constantly changing and hence require constant attention (rebasing, tracking bug fixes[1], etc) from the team maintaining the fork. Specifically concerning the linear types proposal, I can assure you that maintaining the fork has very significant costs (time which maybe would have been better spent on improving the contribution rather than just chasing after the main compiler). At some point, these costs need to pay their dues and lead to inclusion into the compiler; otherwise, the fork will die like many in GHC’s past have. I also don’t think, we can compare the situation to LH. Firstly, an extension needs to meet certain properties so that it can go into what is effectively a post-processor. Secondly, the structure of LH is currently rather incompatible with that of GHC (specifically generating type errors in a Core pass). So, having a separate implementation was probably the easier way to get started anyway. As for GHCJS, they do pay a high price and constantly lag behind the main compiler. Moreover, they do ”only” change the backend. The maintenance burden for an extension that affects everything starting from the frontend is much higher. In summary, I think, we need to bite the bullet. If the *potential* gain of an extension is sufficiently high and it passes the proposal process, I think, we need to allow it into the main compiler. Otherwise, GHC’s potential as a research vehicle will be seriously limited. Cheers, Manuel [1] Including running into bugs that have already been fixed in the main compiler and wasting precious development time on them.

Am 09.07.2018 um 15:43 schrieb Simon Peyton Jones via ghc-steering-committee :

| How feasible would it to have a “lghc” fork that early adaptors can use ?

Obviously not impossible. It'd imply a constant rebase burden. That's different to GHCJS and LH, which are much more modularly separable.

The key thing is the signal we send to the authors. It could mean "go on a fork so we don't need to worry about you any more" (After all, *anyone* can create a fork.... it does not need the committee's blessing.) Or it could mean "we really like this and want to get more experience of it". It'd be good to have a tangible way to express that difference.

Simon

| -----Original Message----- | From: ghc-steering-committee On | Behalf Of Joachim Breitner | Sent: 09 July 2018 14:35 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types | | Hi, | | Am Sonntag, den 08.07.2018, 23:41 -0400 schrieb Richard Eisenberg: | > 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 am wondering if we need in general a better way of allowing high- | risk/high-impact implementations to be tested in practice without needing to | merge them into the main compiler directly first. | | In a way Liquid Haskell is an example here. If Refinement Types were | proposed in a GHC proposal a few years ago we’d be in a similarly hard spot | judging its merit. But the LH people chose a different path: They (more or | less) forked GHC, users who want to play around with it have to install a | separate program, but development can happen independently, more rapidly and | without the commitments to stability that we expect from GHC. The downside | is, of course, less adoption, no integration into existing libraries and | maintenance overhead. | | GHCJS is another example of that model. | | How feasible would it to have a “lghc” fork that early adaptors can use ? | I’d allow us to learn more about this feature, in particular its user | experience, user needs and adoption? If indeed existing code will continue | work as is, then a user of “lghc” still has all of Hackage at their | fingertips, so it seems somewhat realistic that a user who is excited about | linear types will actually use “lghc”. | | Cheers, | Joachim | | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C842bbce9f6c2404a | 6ef108d5e5a0d59c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63666740129955 | 1567&sdata=28CjA6toUq8RsGk1CxzeFrzI9xUhMsAi4PxJxJzO2zM%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

| I want to second Manuel's arguments here -- I don't think we can suggest | that someone forks the compiler. +1. It's possible in theory, as I said, but in practice it'd kill the proposal. It's also worth bearing in mind that the proposers have made a very substantial investment in getting it this far, precisely because it is a "big" proposal. Simon | -----Original Message----- | From: Richard Eisenberg | Sent: 10 July 2018 01:01 | To: Manuel M T Chakravarty | Cc: Simon Peyton Jones ; ghc-steering- | committee@haskell.org; Joachim Breitner | Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types | | I want to second Manuel's arguments here -- I don't think we can suggest | that someone forks the compiler. In effect, this is already true during | development. Speaking as the developer of TypeInType (which I think is an | apt comparison in many respects to LinearTypes), operating on a fork cost me | a lot of time indeed. There's no other way to do it during development, but | it's not sustainable for very long. | | Simon M, you've made good points about the motivations. Perhaps could you | summarize your thoughts on the GitHub trail so we can get a response from | the proposal authors? | | Thanks, | Richard | | > On Jul 9, 2018, at 11:03 AM, Manuel M T Chakravarty | wrote: | > | > I don’t think relegating an accepted proposal to a fork is a reasonable | alternative. Why go through the, for a large proposal, rather painful | proposal process just so that you can do what you can also do without that | blessing? | > | > In fact, if we are going to take that stance, I think, we will seriously | discourage contributions to GHC that involve more substantial language | changes. I think that would be a very bad development as it makes GHC a much | less attractive vehicle for that sort of research. | > | > By their nature, proposals that fall into that category (that they have a | serious impact on GHC) are also the ones that are the most painful to | maintain as a fork. Serious impact means a large overlap with central | elements of the compiler, which are constantly changing and hence require | constant attention (rebasing, tracking bug fixes[1], etc) from the team | maintaining the fork. | > | > Specifically concerning the linear types proposal, I can assure you that | maintaining the fork has very significant costs (time which maybe would have | been better spent on improving the contribution rather than just chasing | after the main compiler). At some point, these costs need to pay their dues | and lead to inclusion into the compiler; otherwise, the fork will die like | many in GHC’s past have. | > | > I also don’t think, we can compare the situation to LH. Firstly, an | extension needs to meet certain properties so that it can go into what is | effectively a post-processor. Secondly, the structure of LH is currently | rather incompatible with that of GHC (specifically generating type errors in | a Core pass). So, having a separate implementation was probably the easier | way to get started anyway. | > | > As for GHCJS, they do pay a high price and constantly lag behind the main | compiler. Moreover, they do ”only” change the backend. The maintenance | burden for an extension that affects everything starting from the frontend | is much higher. | > | > In summary, I think, we need to bite the bullet. If the *potential* gain | of an extension is sufficiently high and it passes the proposal process, I | think, we need to allow it into the main compiler. Otherwise, GHC’s | potential as a research vehicle will be seriously limited. | > | > Cheers, | > Manuel | > | > [1] Including running into bugs that have already been fixed in the main | compiler and wasting precious development time on them. | > | >> Am 09.07.2018 um 15:43 schrieb Simon Peyton Jones via ghc-steering- | committee : | >> | >> | How feasible would it to have a “lghc” fork that early adaptors can | use ? | >> | >> Obviously not impossible. It'd imply a constant rebase burden. That's | different to GHCJS and LH, which are much more modularly separable. | >> | >> The key thing is the signal we send to the authors. It could mean "go on | a fork so we don't need to worry about you any more" (After all, *anyone* | can create a fork.... it does not need the committee's blessing.) Or it | could mean "we really like this and want to get more experience of it". | It'd be good to have a tangible way to express that difference. | >> | >> Simon | >> | >> | -----Original Message----- | >> | From: ghc-steering-committee | >> | On Behalf Of Joachim | >> | Breitner | >> | Sent: 09 July 2018 14:35 | >> | To: ghc-steering-committee@haskell.org | >> | Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types | >> | | >> | Hi, | >> | | >> | Am Sonntag, den 08.07.2018, 23:41 -0400 schrieb Richard Eisenberg: | >> | > 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 am wondering if we need in general a better way of allowing | >> | high- risk/high-impact implementations to be tested in practice | >> | without needing to merge them into the main compiler directly first. | >> | | >> | In a way Liquid Haskell is an example here. If Refinement Types | >> | were proposed in a GHC proposal a few years ago we’d be in a | >> | similarly hard spot judging its merit. But the LH people chose a | >> | different path: They (more or | >> | less) forked GHC, users who want to play around with it have to | >> | install a separate program, but development can happen | >> | independently, more rapidly and without the commitments to | >> | stability that we expect from GHC. The downside is, of course, | >> | less adoption, no integration into existing libraries and maintenance | overhead. | >> | | >> | GHCJS is another example of that model. | >> | | >> | How feasible would it to have a “lghc” fork that early adaptors can | use ? | >> | I’d allow us to learn more about this feature, in particular its | >> | user experience, user needs and adoption? If indeed existing code | >> | will continue work as is, then a user of “lghc” still has all of | >> | Hackage at their fingertips, so it seems somewhat realistic that a | >> | user who is excited about linear types will actually use “lghc”. | >> | | >> | Cheers, | >> | Joachim | >> | | >> | -- | >> | Joachim Breitner | >> | mail@joachim-breitner.de | >> | | >> | | >> | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww | >> | .joachim- | >> | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C842bbce | >> | 9f6c2404a | >> | | >> | 6ef108d5e5a0d59c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63666 | >> | 740129955 | >> | | >> | 1567&sdata=28CjA6toUq8RsGk1CxzeFrzI9xUhMsAi4PxJxJzO2zM%3D&r | >> | eserved=0 | >> _______________________________________________ | >> ghc-steering-committee mailing list | >> ghc-steering-committee@haskell.org | >> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-commit | >> tee | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ | > ee

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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

On Fri, Aug 17, 2018, at 06:06, Simon Peyton Jones wrote:

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.

Interesting point about modularity. The issue really does seem to come down to the allocation functions. I suggested in my GitHub comment that perhaps we could concoct a warning to identify suspicious allocation functions. I think that would pretty much nullify this concern.

On Mon, Aug 27, 2018, at 17:33, Richard Eisenberg wrote:

...

On Aug 7, 2018, at 1:50 AM, Iavor Diatchki wrote: 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.

I agree. I've mused about making (->) be indexed by a type-level record.

This is diverging a bit from the actual proposal, but I'm not convinced that the record index buys us much. The various overloadings of the function arrow add syntactic overhead that a record index could alleviate, but I'd be more concerned about the cognitive overhead. That being said, I'm less concerned about the overloading of the function arrow because Simon seems confident that we can reliably hide it when -XLinearTypes is disabled, even if datatypes are inferred linear. That makes it opt-in complexity, which I don't have a problem with.

...

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

Is this essentially proposing that we don't make any change to datatypes? That would mean that a library that wishes to have linear datatypes would have to explicitly declare them as such. I think this is a stable middle ground. But, if we can guarantee good error-message behavior, etc., I think the "default datatypes to linear" behavior is the right one.

Agreed completely.

Is this essentially proposing that we don't make any change to datatypes? That would mean that a library that wishes to have linear datatypes would have to explicitly declare them as such. I think this is a stable middle ground. Are you proposing that pairs, lists, Maybe etc all have non-linear types? Thus Just :: a -> Maybe a. That would negate one of the principal merits of the proposal, namely that it allows all the existing data types and library functions to work for linear types too. We don't want to force people to implement carbon copies of existing libraries! I think we want both (Just :: a -o Maybe a) and (fromJust :: Maybe a -o a); but suppressing the lollipops when printing for the user unless -XLinear is on. That is, without -XLinear we behave as if the Prelude data types were ordinary pre-linear types; but when you switch -XLinear on, you see that the Prelude types are in fact linear, so that they are useful in a linear setting. Or am I misunderstanding the "stable middle ground"? Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 27 August 2018 22:33 To: Iavor Diatchki Cc: ghc-steering-committee Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types Let's keep the conversation going here. I know this is a *big* proposal, but we owe it to the authors to form a quorum-based consensus (I'd love more voices in these threads!) and offer a response. On Aug 7, 2018, at 1:50 AM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: 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. I agree. I've mused about making (->) be indexed by a type-level record. Right now, that record would look like

data ArrowIndex = ArrowIndex { argRep :: RuntimeRep, resRep :: RuntimeRep } (->) :: forall (ind :: ArrowIndex). TYPE (argRep ind) -> TYPE (resRep ind) -> Type

With this proposal, we move up to

data ArrowIndex = ArrowIndex { argRep :: RuntimeRep, resRep :: RuntimeRep, multiplicity :: Multiplicity } (->) :: forall (ind :: ArrowIndex). TYPE (argRep ind) -> TYPE (resRep ind) -> Type

But I don't have great ideas of how to make this work syntactically -- never mind the fact we don't have type-level records yet. 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). Is this essentially proposing that we don't make any change to datatypes? That would mean that a library that wishes to have linear datatypes would have to explicitly declare them as such. I think this is a stable middle ground. But, if we can guarantee good error-message behavior, etc., I think the "default datatypes to linear" behavior is the right one. Richard

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. It's hard to argue that a different way of integrating linear types into Haskell could not be superior. Perhaps it could! But we can't tell without saying what that different way is. Later Iavor says I am not really making a proposal, but I was suggesting that it might be a simpler way to at least start experimenting with the proposal, without having to change the types of core Haskell concepts. What is "it" that might be simpler? I genuinely want to understand what you have in mind, because I want to be sure that I'm thinking about the same design choices that you are. Simon From: Richard Eisenberg Sent: 28 August 2018 14:27 To: Simon Peyton Jones Cc: Iavor Diatchki ; ghc-steering-committee Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types On Aug 28, 2018, at 6:49 AM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: Is this essentially proposing that we don't make any change to datatypes? That would mean that a library that wishes to have linear datatypes would have to explicitly declare them as such. I think this is a stable middle ground. Are you proposing that pairs, lists, Maybe etc all have non-linear types? I'm not proposing this -- I was trying to interpret Iavor's paragraph: 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). My "stable middle ground" comment is that such a design would work: be type-safe, expressive, etc. I don't think it's ergonomic, for the reasons you describe. I think we want both (Just :: a -o Maybe a) and (fromJust :: Maybe a -o a); but suppressing the lollipops when printing for the user unless -XLinear is on. Why fromJust? My understanding is that this proposal comes with no changes to `base`, meaning we would retain the existing fromJust. Richard

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

Now I get it, thank you for clarification. I agree with your recommendation. Vitaly вт, 28 авг. 2018 г., 19:39 Richard Eisenberg :

On Aug 28, 2018, at 9:32 PM, Vitaly Bragilevsky wrote:

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.

This is a good point. The truth is that the committee has no experience dealing with a proposal of the size of this one. It's hard (for me) to accept this proposal as is, because it's not a full specification. The big missing piece is inference. We also don't have a solid description of how much complexity the implementation will have to adopt. Yet, it would be very unfortunate for the authors to put in a ton of time into writing a paper, a proposal, and a prototype implementation only to get turned down. So, my understanding is that I'm recommending something of a conditional acceptance: we say, as a committee, that we're pleased with the general direction of travel and to encourage the authors to keep working. This means that we expect to accept, barring something large and unforeseen. The difference between conditional acceptance and outright acceptance is that it gives the committee further opportunities to suggest amendments to the proposed change. (Even an accepted proposal can effectively get retroactively denied if, say, the implementation requires a 10% slowdown on all programs to support an esoteric feature.)

Does this help to clarify?

Richard

I imagine the biggest trade off is that the current proposal allows for polymorphism in the multiplicity, while I was thinking maybe we could start without. Yes, that’s a total killer. Polymorphism is absolutely central to the design. I don’t think the design would hold water at all with two distinct function arrows. As I said before, though, perhaps we should not worry that much about the function space, and just go for it. I support that (albeit of course I have an interest in this, as a co-author). I’m imagining that, absent -XLinearTypes, we would suppress (a) linearity polymorphism (b) -o (printing it as -> instead. Every program that is accepted today would still be accepted. So the extra polymorphism in the function space would be invisible. Where would you get a bump in that road? Imagine you imported a function with type f :: (Int -o Int) -> Int and applied it to a function that did not have linear type. Now, we MUST produce a type error: the imported function f may rely on the linearity of its argument. But note that this could not happen without compiling f with -XLinearTypes. So, if you don’t use -XLinearTypes, you won’t see any bumps. Of course that’s an informal argument. Let’s see. But it convinces me enough to accept the proposal – subject (as Richard says, and true of any proposal) it later turns out to have unforeseen but unacceptable consequences. Simon From: ghc-steering-committee On Behalf Of Iavor Diatchki Sent: 29 August 2018 07:51 To: Vitaly Bragilevsky Cc: ghc-steering-committee Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types I was thinking about a design where the linear arrow is a completely separate type than the normal function type. I think that a choice like that would probably require additional annotations on other declarations to indicate when the linear machinery would kick in. For examplee, `data` declarations would need an extra tag to indicate that we should generate linear constructors, pattern matching, and single field selectors. Similarly, to declare linear functions we would either require a type signature, or some sort of a tag on the lambda/function declaration to indicate that it is linear. I haven't thought through all the details but this is what I was thinking about. Essentially, the difference is that the current proposal keeps track of these tags automatically in the multiplicity of the function space and I was thinking of a design where these things are specified manually. I imagine the biggest trade off is that the current proposal allows for polymorphism in the multiplicity, while I was thinking maybe we could start without. I am not arguing for this alternative design as I haven't really thought through all the details. I was just thinking of alternatives that leave the current function space alone. As I said before, though, perhaps we should not worry that much about the function space, and just go for it. I have some comments on the type functions for multiplicities, but I'll write them in the git hub. Iavor On Wed, Aug 29, 2018, 8:40 AM Vitaly Bragilevsky mailto:bravit111@gmail.com> wrote: Now I get it, thank you for clarification. I agree with your recommendation. Vitaly вт, 28 авг. 2018 г., 19:39 Richard Eisenberg mailto:rae@cs.brynmawr.edu>: On Aug 28, 2018, at 9:32 PM, Vitaly Bragilevsky mailto:bravit111@gmail.com> wrote: 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. This is a good point. The truth is that the committee has no experience dealing with a proposal of the size of this one. It's hard (for me) to accept this proposal as is, because it's not a full specification. The big missing piece is inference. We also don't have a solid description of how much complexity the implementation will have to adopt. Yet, it would be very unfortunate for the authors to put in a ton of time into writing a paper, a proposal, and a prototype implementation only to get turned down. So, my understanding is that I'm recommending something of a conditional acceptance: we say, as a committee, that we're pleased with the general direction of travel and to encourage the authors to keep working. This means that we expect to accept, barring something large and unforeseen. The difference between conditional acceptance and outright acceptance is that it gives the committee further opportunities to suggest amendments to the proposed change. (Even an accepted proposal can effectively get retroactively denied if, say, the implementation requires a 10% slowdown on all programs to support an esoteric feature.) Does this help to clarify? Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee