[ghc-steering-committee] Our process and BIG ideas
Simon Peyton Jones
simonpj at microsoft.com
Wed Nov 15 09:38:58 UTC 2017
I’m basically with you, but I do think that check [2] is qualitatively different to [1]. You say
(b) The implementation is good, but the implementation turned out to be more costly than originally anticipated. In this case, code review will ask the contributor to revise their proposal, go back to the GHC Steering Committee, and get the revision approved. Now, this is the moment where the committee is asked to review the proposal in the light of the newly gained experience.
My concern about the slow accretion of hidden costs is more about the [1] than [2]. In principle, an implementation could be simple, while yet imposing previously unanticipated complexity on the language design.
An example: a type inference algorithm might be easy to implement, but it might behave unpredictably – e.g. if you change (e1,e2) to (e2,e1) the type inference fails – that is, it might be hard to specify in a programmer-accessible way. Actually linear types could be like this. The paper explicitly does not handle type inference; and neither does the proposal. I’d be surprised if we couldn’t come up with an inference algorithm we all considered acceptable in language-design terms – not just in implementation terms – but still, it’s something we won’t know for a while.
I’m only saying that at checkpoint [2] the criteria are not just code/implementation quality and complexity; it also implicitly includes a review of the judgement made at checkpoint [1], in case the “slow accretion” has happened.
I don’t think there’s any disagreement here. No one wants a feature to end up in GHC that, in retrospect, we can see is mis-designed! We have to balance that with giving contributors confidence, and enough certainty to invest their most precious resource (their own time) in GHC.
Nevertheless, we do *not* need a priori and inherently imprecise evaluation of whether a proposal is ”big” or complex. In fact, our process (the whole pipeline above) is adaptive
Yes – I’m not particularly seeking an a-priori evaluation of size (although, thinking aloud, I did speculate about such a thing). But being adaptive is important. A fly and an elephant are creatures on a continuous scale of creature sizes. There is no point at which we can say “this creature is Big and the next smallest one is NotBig”. And yet in the end elephants and flies really do need rather different treatment.
Simon
From: Manuel M T Chakravarty [mailto:chak at justtesting.org]
Sent: 15 November 2017 02:26
To: Simon Peyton Jones <simonpj at microsoft.com>
Cc: Richard Eisenberg <rae at cs.brynmawr.edu>; ghc-steering-committee at haskell.org
Subject: Re: [ghc-steering-committee] Our process and BIG ideas
Simon,
I think, the suggestion to add a formal point about detailing the effect of an extension on Core is fabulous! We should absolutely do that.
It seems the sticky point is your first, the slow accretion of hidden costs. It totally agree that this is the most tricky scenario. However, I am not so sure that there is no moment, where that costs are checked. There is none if we look at this committee in isolation. However, there is one if we look at the entire process of getting an extension into GHC (and I think, this is key to making this all work elegantly). Here is the pipeline:
Proposal
|
v
[1] (GHC Steering Committee)
|
Pull Request/Differential
|
v
[2] (Code reviewers)
|
Development version
|
v
[3] (Release Manager)
|
v
Released feature
For anything to get into a stable release, there are three checks [1], [2] & [3] that need to be passed. What I propose is that failure to pass one of the checks doesn’t just prevent you from getting further, but that it may throw you back to an earlier stage.
In the proposal, we do ask about the implementation costs and costs of feature interaction etc. I like to suggest that if a code contribution backed by a proposal is submitted for consideration for merging, the code reviewers check that the code contribution actually meets the promises made in the proposal about, for example, implementation costs. If these promises are not met, there are two possibilities:
(a) The implementation is just not very good. In that case, the contributors can try to improve their code and try again.
(b) The implementation is good, but the implementation turned out to be more costly than originally anticipated. In this case, code review will ask the contributor to revise their proposal, go back to the GHC Steering Committee, and get the revision approved. Now, this is the moment where the committee is asked to review the proposal in the light of the newly gained experience.
For example, following your suggestion about explicitly asking proposal authors to detail the impact of an extension on Core. A proposal may claim to not have to change Core at all. Then, it turns out the implementation actually does change Core, maybe just in a small way. Nevertheless, this clearly signals to code review that the proposal was inaccurate. Hence, the proposal has to go back to the GHC Steering Committee and be re-approved.
As another example, assume that we have got a big complex proposal and the authors write that they are —at this stage— unsure about the exact impact on Core. In this case, just as with the or-patterns and GADTs, we may review the proposal, but make final approval contingent on understanding the actual impact on Core.
In this manner, the committee gets to re-check proposals, where substantial new experience was gained during the implementation that altered trade offs of implementation costs, feature interaction etc. Nevertheless, we do *not* need a priori and inherently imprecise evaluation of whether a proposal is ”big” or complex. In fact, our process (the whole pipeline above) is adaptive. The less accurate a proposal turns out to be (due to complexity or other factors), the more often it’ll be thrown back and re-evaluated. And maybe the fact that a proposal is thrown back multiple times will make us weary of it and cause us to eventually reject it.
Manuel
Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>>:
I’m ok with what Manuel says, especially the bit about being more explicit about the implicit conditionality. But I would add
* Acceptance is always a balance of judgement. Is the extra language and implementation complexity justified by the benefits to the programmer? For “big” features, that balance may change as we learn more about it.
Manuel takes outright unsoundness as an example, and it is a comforting one because it’s so clear-cut. But in reality I think that it’s more likely that there’ll be a slow accretion of hidden costs that slowly become apparent. Then it might seem more capricious if the committee’s judgement changed; and in any case there’d be no moment at which the committee was asked to review the proposal in the light of experience.
* I think we could address some of this by making the conditionality in acceptance more explicit, just as Manuel says. But in specific terms, not just in general ones. For example, for or-patterns I think we are edging towards “accept, provided we can resolve the issues around GADTs etc”. For a “bigger” proposal we might have a longer list of things we regarded as danger spots.
* I suggest that we add to our criteria what effect (if any) the proposal has on Core. You may see Core as merely an implementation mechanism, but I regard it as a solid sanity check. We simply do not have a formal specification for all of Haskell. It’s too big, and if we insisted on that we ‘d never do anything. But we DO have a formal spec for Core<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc%2Fghc%2Ftree%2Fmaster%2Fdocs%2Fcore-spec&data=02%7C01%7Csimonpj%40microsoft.com%7C7e5a91349d674f6305af08d52bd03441%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636463095632609403&sdata=2oE9QdPs5zQ%2FxY%2F3Y%2FPEDeXoujEx3LN212xwvirFgks%3D&reserved=0>. It is small enough to be intellectually tractable. And, for better or worse, GHC is one of the very few production compilers in the world (I actually do now know of any others) that maintain a statically typed IR right through optimisation up to code generation.
Most proposals don’t change Core one whit. But for those that do, I think it would be reasonable to ask for a pretty solid spec of what changes are proposed. That would reassure us that the proposal is in fact sound. All the rest is syntactic sugar, as it were.
Simon
From: Manuel M T Chakravarty [mailto:chak at justtesting.org]
Sent: 14 November 2017 01:10
To: Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>>
Cc: Richard Eisenberg <rae at cs.brynmawr.edu<mailto:rae at cs.brynmawr.edu>>; ghc-steering-committee at haskell.org<mailto:ghc-steering-committee at haskell.org>
Subject: Re: [ghc-steering-committee] Our process and BIG ideas
All approval is conditional
~~~~~~~~~~~~~~~~~~~~
I get the feeling that this discussion is actually really about,
> What does approval mean?
Currently, the ghc-proposals' README states,
Acceptance of the proposal implies that the implementation will be accepted into GHC provided it is well-engineered, well-documented, and does not complicate the code-base too much.
So, obviously and explicitly all acceptance of proposals by this committee is conditional (there is no unconditional approval). Everything is conditional on a good implementation.
However, I would argue that —in actual fact— there are some conditions that we have never made explicit as well, and those implicit conditions are at the core of the current discussion. For example, proposals like TypeInType, linear types, or dependent types may well turn out to be impossible to implement *without complicating the code-base too much* (e.g., because they need to change Core in ways that are too intrusive). In other words, if the required engineering constraints are impossible to meet for a proposal, then, despite it originally being accepted, we wouldn’t allow it into a shipping compiler.
I will go further and argue that there are conditions that are not mentioned at all. For example, let’s assume I make a convincing argument for a type extension and I have a conference paper and a proof of progress and preservation, and the committee accepts my proposal. If, during implementation, I or somebody else find that my proof is actually faulty and the system is unsound, would we allow it into the compiler only because we accepted the proposal? Of course not!
Hence, all accepted proposals are also conditional on that the properties and assumptions stated in the proposal are actually correct. If a proposal claims that an extension is sound, it must be sound. If it states that it doesn’t conflict with other type extension, it may not conflict. If it argues, the implementation will be efficient, it must be efficient, and so on. If anything turns out to be wrong, the approval, which was issued under these assumptions, is void. (Think of it as a contract that is voided once any of the clauses is violated.)
So, I hope we can agree that all approval is conditional. What we need to do is to specify the conditions that we implicitly assign beyond the engineering focused condition that is currently in the README. (Having conditions is fine, but to be fair to proposal authors, IMHO we need to be explicit about them.)
Size doesn’t matter
~~~~~~~~~~~~~~~
I like to argue that the size of a proposal is much less important than we might think. Fairly small changes can easily turn into a pit of vipers. For example, take generalised new type deriving. It was such a small simple change and easy to do with System FC’s equality constraints. If we had had GHC proposals at the time, this would have been a small proposal relative to the fancy type family additions and GADTs going on at the time. Nevertheless, I’d argue, generalised newtype deriving was probably the biggest type soundness nightmare GHC ever had. (How many papers did it take to fix it…kind of?)
Whether a proposal is long or short, whether it involves complex types, or whether it is just syntax (that may always turn out to be really hard to implement with LALR(1)), I think, we want the same rules and the same conditions attached to approval of the proposal.
* There needs to a well-engineered implementation.
* It shouldn’t complicate the codebase too much.
* It must not have unexpected interactions with other language features.
* It must not unduly affect the performance of the compiler (neither of compilation nor of the generated code).
* It must not turn out to be unsound.
* It must not turn out to lead to impossible to understand error messages.
* What else?
All these conditions must be met by *all* proposals, large or small. Every approval is always conditional on all of these conditions.
What if a condition is violated
~~~~~~~~~~~~~~~~~~~~~~
That depends on whether the problem can be fixed and what kind of fix is needed.
Anything that is ”just” a matter of code quality is a matter for the code reviewers to hold back until it is good enough. Anything destabilising the compiler or turning out to affect performance too much is up to the release manager to prevent going into an actual release. These issues are not a concern of this committee.
However, if a conceptual problem is found, a system is unsound, or generally any of the assumptions or statements in the proposal *on which approval was based* turns out to be wrong, the proposal needs to be changed. Once it is changed, it needs to be approved again. If no acceptable change can be found, the proposal is out.
Summary
~~~~~~~
I propose to make the conditions (that always existed) explicit, check them while a proposal gets refined and potential issues discovered during implementation, and bounce any (significant) changes that need to be made back to the committee. In this way, I hope, we can address the concerns voiced by Simon and Richard, while being completely transparent to proposal authors.
Moreover, we don’t need any a priori judgement about whether a proposal is small or large (and where exactly is that boundary). Instead, naturally, anything that leads to issues will be sent back to the committee, which allows for iteration exactly where this is necessary.
Cheers,
Manuel
Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>>:
| However, I'm leery of unconditional approval of something as large as the
| linear types proposal.
If "unconditional approval" means " we agree to include this feature in GHC, regardless of the consequences", then I guess everyone would agree with Richard. It's not just the implementation consequences either: we have to think about the interaction of a big new feature with all the other aspects of the surface language, and that is really hard to do in advance.
For little proposals (like commas in export lists) we can be pretty confident that we aren't going to get any major surprises. For big ones like this, our confidence is much lower.
But we must think of it from the contributors' point of view too. Contributors to GHC want to see a transparent and somewhat predictable pipeline of steps that successively make it more and more likely that a proposal will end up in mainstream GHC. For big proposals maybe we need more steps. E.g.
1. Philosophically, we like the direction of travel. If there are no surprises, we'd like to have this in the language.
2. Details. Now there are lot of specifics. Interactions with other features of Haskell. If there are going to be changes in Core, a precise specification of those changes would be helpful. (I know that Core is an internal matter, but it's an outstandingly good sanity-check.)
3. Implementation. Now we have an implementation.
4. Merge into HEAD
We have previously conflated (1) and (2) and that seems fine for a small proposal, but for a big one like this we might want to split the steps, to offer authors the confidence to invest in (2).
Actually (2) and (3) are likely to be symbiotic, I think.
Does that make sense?
Simon
| -----Original Message-----
| From: ghc-steering-committee [mailto:ghc-steering-committee-
| bounces at haskell.org<mailto:bounces at haskell.org>] On Behalf Of Richard Eisenberg
| Sent: 13 November 2017 03:25
| To: Manuel M T Chakravarty <chak at justtesting.org<mailto:chak at justtesting.org>>
| Cc: ghc-steering-committee at haskell.org<mailto:ghc-steering-committee at haskell.org>
| Subject: Re: [ghc-steering-committee] Our process and BIG ideas
|
| I fully agree that proposals for large new features can reference an
| accompanying paper.
|
| However, I'm leery of unconditional approval of something as large as the
| linear types proposal. GHC is a very large, complex system, and no one can
| anticipate all the interactions that a proposal may have with existing
| features. It's quite possible that something which seems like a good idea
| has a disastrous interaction with some other part of the compiler/language
| definition.
|
| Instead, I would favor a conditional approval that would turn to rejection
| only if further experience (gained through a [partial] implementation)
| reveals a theoretical sticking point. I use "theoretical" here to mean that
| the rejection wouldn't be based on poor code quality or an implementation
| challenge, per se, but by running into a scenario where we are unable to
| specify the correct behavior of the system.
|
| In truth, even an approval that we described as unconditional would really
| be as in the paragraph above -- we simply can't do better. So I guess I'm
| favoring calling such an approval as conditional, just to be clear to
| proposers what we mean.
|
| Richard
|
| > On Nov 12, 2017, at 10:07 PM, Manuel M T Chakravarty
| <chak at justtesting.org<mailto:chak at justtesting.org>> wrote:
| >
| > In the light of the linear types proposal PR, SimonPJ’s comment
| >
| >
| https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%25>
| 2Fghc-proposals%2Fghc-proposals%2Fpull%2F91%23issuecomment-
| 343457821&data=02%7C01%7Csimonpj%40microsoft.com<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2F40microsoft.com&data=02%7C01%7Csimonpj%40microsoft.com%7C15f65c21dafe4d34386108d52afc7993%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636462186227822124&sdata=hMwpjjqTh6opD3RikzrDHIikPnly9z%2B8QaeiN4IxjSY%3D&reserved=0>%7C76a50b24b6dc436c9c4808d52
| a463534%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636461403387929271&sdat
| a=%2FGtP16v%2BiJEDwkd0TpX6yKpXS0bZaOh1HWDCEsPTiDg%3D&reserved=0
| >
| > and some uncertainty about the proposal process that has been communicated
| to me via a side channel, it might be worthwhile clarifying our expectations
| for large complex proposals. (I know, we basically punted on these questions
| in our initial discussion on the process with the intention to revisit after
| we gained some experience. It seems this time has come.)
| >
| > Firstly, we usually require proposals to be self-contained. This makes a
| lot of sense for small to medium-sized proposals to limit the time needed by
| the committee to hunt down all the required information. However, in a case,
| such as the linear types work, where there is a highly polished text in the
| form of a research paper (or similar), it seems reasonable to refer to that
| existing work — not only because type rules are a lot nicer to read when
| rendered by LaTeX instead of Markdown.
| >
| > Concretely, I’d like us to give some guidance wrt to this issue to
| proposal authors and document that at
| https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%25>
| 2Fghc-proposals%2Fghc-proposals%23ghc-
| proposals&data=02%7C01%7Csimonpj%40microsoft.com<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2F40microsoft.com&data=02%7C01%7Csimonpj%40microsoft.com%7C15f65c21dafe4d34386108d52afc7993%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636462186227822124&sdata=hMwpjjqTh6opD3RikzrDHIikPnly9z%2B8QaeiN4IxjSY%3D&reserved=0>%7C76a50b24b6dc436c9c4808d52
| a463534%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636461403387929271&sdat
| a=Z8x%2FqlkWGH4dt43vQYpU9yP7YGGBZ4NR920%2FBS6EMA4%3D&reserved=0
| >
| > Secondly, Simon, you seem to suggest that a large proposal like this
| wouldn’t be either accepted or rejected, but put into a kind a limbo state
| of further evaluation as seen fit. I agree that instead of outright
| rejection of a proposal that we consider flawed but not hopeless, we might
| request further elaboration and resubmission as we have done in the past.
| However, if a proposal passes muster, I think, we should accept it
| unconditionally, even if it is a large change. (If, say, at the end, the
| implementation is not up to scratch, then it is up to the code reviewers to
| reject the patches, but I don’t think, it is this committee’s job anymore.)
| >
| > In any case, I think, it is important make the process as clear as
| possible to authors, so they know what they are in for.
| >
| > What do you all think?
| >
| > Cheers,
| > Manuel
| >
| > _______________________________________________
| > ghc-steering-committee mailing list
| > ghc-steering-committee at haskell.org<mailto: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<mailto:ghc-steering-committee at haskell.org>
| https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20171115/89cc3b99/attachment-0001.html>
More information about the ghc-steering-committee
mailing list