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 :

| 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@haskell.org] On Behalf Of Richard Eisenberg | Sent: 13 November 2017 03:25 | To: Manuel M T Chakravarty | Cc: ghc-steering-committee@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 | 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% | 2Fghc-proposals%2Fghc-proposals%2Fpull%2F91%23issuecomment- | 343457821&data=02%7C01%7Csimonpj%40microsoft.com%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% | 2Fghc-proposals%2Fghc-proposals%23ghc- | proposals&data=02%7C01%7Csimonpj%40microsoft.com%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@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