What do we need from the linear-types proposal?

Joachim Breitner

27 Nov 2017 27 Nov '17

2:53 p.m.

Dear committee, Mathieu Boespflug asks on https://github.com/ghc-proposals/ghc-proposals/pull/91#issuecomment-34712320...

...

Could the Committee define the items it expects before it can make a determination about this proposal? We've heard in this thread members of the Committee ask for a fleshed out linear base, more examples than are already in the proposal and in the paper, and also full code from other users at large. I can certainly understand where they are coming from. But at the same time, I am concerned about scope creep. Defining where the goal posts are from now would certainly help.

and I am not sure what to reply here… but “we’ll know that once we made a determination” is probably not helpful. Does anyone here feel like he could define the requirements that are necessary to allow us to consider the proposal properly? Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Attachments:

signature.asc (application/pgp-signature — 833 bytes)

Show replies by date

Simon Peyton Jones

27 Nov 27 Nov

2:58 p.m.

New subject: What do we need from the linear-types proposal?

The main thing I'd add, which applies to all proposals is this: * If a proposal requires a change to Core, that change should be described rather precisely. The justification for this is in my comments on the linear-types thread. Simon | -----Original Message----- | From: ghc-steering-committee [mailto:ghc-steering-committee- | bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 27 November 2017 14:54 | To: ghc-steering-committee@haskell.org | Subject: [ghc-steering-committee] What do we need from the linear-types | proposal? | | Dear committee, | | Mathieu Boespflug asks on | https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.c | om%2Fghc-proposals%2Fghc-proposals%2Fpull%2F91%23issuecomment- | 347123204&data=02%7C01%7Csimonpj%40microsoft.com%7C44b56cc9019549c8dc5f08 | d535a6ad85%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63647391234812744 | 2&sdata=LqVQJviHF8Wxbc3QHiPWe2C2pK%2FTXX12GbmxPLJEOi0%3D&reserved=0 | | > Could the Committee define the items it expects before it can make a | > determination about this proposal? We've heard in this thread members | > of the Committee ask for a fleshed out linear base, more examples than | > are already in the proposal and in the paper, and also full code from | > other users at large. I can certainly understand where they are coming | > from. But at the same time, I am concerned about scope creep. | > Defining where the goal posts are from now would certainly help. | | and I am not sure what to reply here… but “we’ll know that once we made a | determination” is probably not helpful. | | Does anyone here feel like he could define the requirements that are | necessary to allow us to consider the proposal properly? | | Thanks, | Joachim | | | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joach | im- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C44b56cc9019549c8d | c5f08d535a6ad85%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636473912348 | 127442&sdata=zDtUrSDruKvFJWEKfJHXeISRDM21q9juzyBdyjLYUzs%3D&reserved=0

Richard Eisenberg

10:04 p.m.

New subject: What do we need from the linear-types proposal?

...

On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones wrote:

* If a proposal requires a change to Core, that change should be described rather precisely.

Iavor Diatchki

28 Nov 28 Nov

2:15 a.m.

Hello, Coming up with a concrete list of suggestions is hard, but here are a couple things that would make it easier for me to understand large proposals (e.g., like the linear types one): 1. It is good if large proposals are "modular", meaning that you can understand them (and perhaps implement them), one piece at a time. For example, adding certain features to the language may enable us to make library changes, but that sort of thing can be disused separately. 2. I think that it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. One thing that works well for me is to see lots of examples which illustrate various aspects of the design. Generally, I find it much easier to understand and generalize from a set of examples, than a set of rules, especially if the rules are not accompanied by an explanation of the reasons for choosing them. -Iavor On Mon, Nov 27, 2017 at 2:04 PM Richard Eisenberg wrote:

...

...
On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones wrote:

* If a proposal requires a change to Core, that change should be described rather precisely.

In Greek or in Haskell? Less tersely: does a formalization in a paper suffice? Or should the proposal write out the new Haskell definition? These are closely related, but not the same. (For example, formalizations don't include the AppTy/TyConApp/FunTy distinction that is important for performance.)

My own view is that Greek is enough.

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

Simon Peyton Jones

10:25 a.m.

New subject: What do we need from the linear-types proposal?

it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. I don’t really agree with this. Papers tend to be the result of a great deal of focused attention and multiple iterations. It’s hard (and indeed wasteful) to duplicate that effort in a proposal. Better just to point to it. (On the rare occasions where there is a paper that squarely addresses the topic of the proposal.) But yes, more examples (not duplicate examples) are always good. Simon From: Iavor Diatchki [mailto:iavor.diatchki@gmail.com] Sent: 28 November 2017 02:16 To: Richard Eisenberg Cc: Simon Peyton Jones ; ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] What do we need from the linear-types proposal? Hello, Coming up with a concrete list of suggestions is hard, but here are a couple things that would make it easier for me to understand large proposals (e.g., like the linear types one): 1. It is good if large proposals are "modular", meaning that you can understand them (and perhaps implement them), one piece at a time. For example, adding certain features to the language may enable us to make library changes, but that sort of thing can be disused separately. 2. I think that it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. One thing that works well for me is to see lots of examples which illustrate various aspects of the design. Generally, I find it much easier to understand and generalize from a set of examples, than a set of rules, especially if the rules are not accompanied by an explanation of the reasons for choosing them. -Iavor On Mon, Nov 27, 2017 at 2:04 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote:

* If a proposal requires a change to Core, that change should be described rather precisely.

In Greek or in Haskell? Less tersely: does a formalization in a paper suffice? Or should the proposal write out the new Haskell definition? These are closely related, but not the same. (For example, formalizations don't include the AppTy/TyConApp/FunTy distinction that is important for performance.) My own view is that Greek is enough. 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

Iavor Diatchki

6:18 p.m.

I suspect we are in agreement here. What I was trying to capture is the fact that in my experience papers tend to contain both more and less than what I'd expect to find in a GHC proposal. They contain more, in that they may address important issues such as proofs of soundness, or other important properties, much more extended motivation, comparisons to other research, etc.. I don't think these belong in a proposal, but I think it is a big plus for a proposal to refer to a published papers addressing such issues. I think, however, sometimes (often?) papers also tend to aim at a fairly general explanation of concepts, that is not specific to a particular language. I think that GHC proposal should contain this extra detail, and be aimed at how the feature would be added to Haskell in particular (and even more concretely, to GHC). This involves discussing concrete syntax, interactions with other language features, and a lot of examples, so that a Haskell user can get a feel of what the new feature might feel like. Overall, I am a bit weary of publishing a list of "requirements" for a proposal, mostly because anything we publish could probably be interpreted in different ways, and I think---for me---it is much more important that we collectively think the proposal is a good idea, than there being a check-list that has been completely checked-off. -Iavor On Tue, Nov 28, 2017 at 2:25 AM Simon Peyton Jones wrote:

...

it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers.

I don’t really agree with this. Papers tend to be the result of a great deal of focused attention and multiple iterations. It’s hard (and indeed wasteful) to duplicate that effort in a proposal. Better just to point to it. (On the rare occasions where there is a paper that squarely addresses the topic of the proposal.)

But yes, more examples (not duplicate examples) are always good.

Simon

*From:* Iavor Diatchki [mailto:iavor.diatchki@gmail.com] *Sent:* 28 November 2017 02:16 *To:* Richard Eisenberg *Cc:* Simon Peyton Jones ; ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de> *Subject:* Re: [ghc-steering-committee] What do we need from the linear-types proposal?

Hello,

Coming up with a concrete list of suggestions is hard, but here are a couple things that would make it easier for me to understand large proposals (e.g., like the linear types one):

1. It is good if large proposals are "modular", meaning that you can understand them (and perhaps implement them), one piece at a time. For example, adding certain features to the language may enable us to make library changes, but that sort of thing can be disused separately.

2. I think that it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. One thing that works well for me is to see lots of examples which illustrate various aspects of the design. Generally, I find it much easier to understand and generalize from a set of examples, than a set of rules, especially if the rules are not accompanied by an explanation of the reasons for choosing them.

-Iavor

On Mon, Nov 27, 2017 at 2:04 PM Richard Eisenberg wrote:

...
On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones wrote:

* If a proposal requires a change to Core, that change should be described rather precisely.

In Greek or in Haskell? Less tersely: does a formalization in a paper suffice? Or should the proposal write out the new Haskell definition? These are closely related, but not the same. (For example, formalizations don't include the AppTy/TyConApp/FunTy distinction that is important for performance.)

My own view is that Greek is enough.

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

Simon Peyton Jones

29 Nov 29 Nov

8:38 a.m.

New subject: What do we need from the linear-types proposal?

Overall, I am a bit weary of publishing a list of "requirements" for a proposal, mostly because anything we publish could probably be interpreted in different ways, and I think---for me---it is much more important that we collectively think the proposal is a good idea, than there being a check-list that has been completely checked-off. Yes – but the more clarity we give the more likely we are to get good proposals, and to avoid misunderstandings. I think some effort is justified here. S From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 28 November 2017 18:18 To: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] What do we need from the linear-types proposal? I suspect we are in agreement here. What I was trying to capture is the fact that in my experience papers tend to contain both more and less than what I'd expect to find in a GHC proposal. They contain more, in that they may address important issues such as proofs of soundness, or other important properties, much more extended motivation, comparisons to other research, etc.. I don't think these belong in a proposal, but I think it is a big plus for a proposal to refer to a published papers addressing such issues. I think, however, sometimes (often?) papers also tend to aim at a fairly general explanation of concepts, that is not specific to a particular language. I think that GHC proposal should contain this extra detail, and be aimed at how the feature would be added to Haskell in particular (and even more concretely, to GHC). This involves discussing concrete syntax, interactions with other language features, and a lot of examples, so that a Haskell user can get a feel of what the new feature might feel like. Overall, I am a bit weary of publishing a list of "requirements" for a proposal, mostly because anything we publish could probably be interpreted in different ways, and I think---for me---it is much more important that we collectively think the proposal is a good idea, than there being a check-list that has been completely checked-off. -Iavor On Tue, Nov 28, 2017 at 2:25 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. I don’t really agree with this. Papers tend to be the result of a great deal of focused attention and multiple iterations. It’s hard (and indeed wasteful) to duplicate that effort in a proposal. Better just to point to it. (On the rare occasions where there is a paper that squarely addresses the topic of the proposal.) But yes, more examples (not duplicate examples) are always good. Simon From: Iavor Diatchki [mailto:iavor.diatchki@gmail.commailto:iavor.diatchki@gmail.com] Sent: 28 November 2017 02:16 To: Richard Eisenberg mailto:rae@cs.brynmawr.edu> Cc: Simon Peyton Jones mailto:simonpj@microsoft.com>; ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] What do we need from the linear-types proposal? Hello, Coming up with a concrete list of suggestions is hard, but here are a couple things that would make it easier for me to understand large proposals (e.g., like the linear types one): 1. It is good if large proposals are "modular", meaning that you can understand them (and perhaps implement them), one piece at a time. For example, adding certain features to the language may enable us to make library changes, but that sort of thing can be disused separately. 2. I think that it would be good if the proposal contains enough information to get a feeling for the core idea of the proposal, both how it might be used, and about how it might be implemented, without referring to external papers. One thing that works well for me is to see lots of examples which illustrate various aspects of the design. Generally, I find it much easier to understand and generalize from a set of examples, than a set of rules, especially if the rules are not accompanied by an explanation of the reasons for choosing them. -Iavor On Mon, Nov 27, 2017 at 2:04 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote:

* If a proposal requires a change to Core, that change should be described rather precisely.

Simon Peyton Jones

28 Nov 28 Nov

10:18 a.m.

New subject: What do we need from the linear-types proposal?

I agree -- Greek is enough providing it is complete enough to convince the reader that the transliteration will be routine. Simon | -----Original Message----- | From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] | Sent: 27 November 2017 22:04 | To: Simon Peyton Jones | Cc: Joachim Breitner ; ghc-steering- | committee@haskell.org | Subject: Re: [ghc-steering-committee] What do we need from the linear- | types proposal? | | | > On Nov 27, 2017, at 9:58 AM, Simon Peyton Jones | wrote: | > | > * If a proposal requires a change to Core, that change should be | > described rather precisely. | | In Greek or in Haskell? Less tersely: does a formalization in a paper | suffice? Or should the proposal write out the new Haskell definition? | These are closely related, but not the same. (For example, | formalizations don't include the AppTy/TyConApp/FunTy distinction that | is important for performance.) | | My own view is that Greek is enough. | | Richard

2779

Age (days ago)

2781

Last active (days ago)

List overview

Download

7 comments

4 participants

participants (4)

Iavor Diatchki
Joachim Breitner
Richard Eisenberg
Simon Peyton Jones