Dear GHC steering committee
OK Richard has now revised the "Design for Dependent Types" proposal, and has resubmitted it. As we asked, it now includes the design sketch that constitutes the direction of travel advocated in the proposal, rather than merely referring to it.
Here it is once morehttps://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0...
I propose acceptance.
Remember:
* We would not be accepting every detail of the design in Section 4 - rather, we expect further specific proposals as we move in the direction described in the proposal. So we should not debate the fine print of Section 4.
* We would be accepting that the proposal describes a direction of travel that we are happy with. That in turn gives people the confidence to invest efforts in those more detailed proposals. As the "Proposed change specification" says: "When evaluating new proposals, the GHC committee would consider compatibility with the design sketch below. Generally speaking, new proposals should be forward-compatible with the design sketch; that is, the new features proposed would continue to be at home when surrounded by other dependent-type features."
Any views? Questions of clarification or technical questions belong on the comment stream.
Thanks
Simon
From: ghc-steering-committee On Behalf Of Simon Peyton Jones via ghc-steering-committee
Sent: 06 April 2021 13:58
To: ghc-steering-committee@haskell.org
Subject: Re: [ghc-steering-committee] Recommendation for #378: support the design for dependent types
Richard and I have discussed this.
We concluded that we'd put it back into "Needs revision" status. He's going to expand it (substantially) to include the proposed design sketch of dependent types on the GHC wikihttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fdependent-haskell&data=04%7C01%7Csimonpj%40microsoft.com%7C1b7abe0682c0408df2f708d8f8fbeb5f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533108900934303%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=nucS4608uGvDJd6ki1pJCMfwCP1jlbxVls4IaoJmu84%3D&reserved=0. Then he'll resubmit in the hope of getting approval of the design in principle, subject to subsequent discussion of the fine detail.
Simon
From: Simon Peyton Jones mailto:simonpj@microsoft.com>
Sent: 29 March 2021 13:17
To: ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org
Cc: Simon Peyton Jones mailto:simonpj@microsoft.com>
Subject: Recommendation for #378: support the design for dependent types
Dear GHC Steering Committee
I'm recommending acceptance of Proposal #378: Support the design for dependent typeshttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F378&data=04%7C01%7Csimonpj%40microsoft.com%7C1b7abe0682c0408df2f708d8f8fbeb5f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533108900944303%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=zmz9Iywt1EuiJdFKzuGaxLI5Zeu3ZnqNYwG7MoZTmpA%3D&reserved=0
As you'll see, there is a lot of useful context, but the payload is pretty simple
When evaluating new proposals, the GHC committee would consider compatibility with the proposed design sketch of dependent types on the GHC wikihttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fdependent-haskell&data=04%7C01%7Csimonpj%40microsoft.com%7C1b7abe0682c0408df2f708d8f8fbeb5f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533108900954303%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=nPnYN%2BIZYLORpnhxp6MDygTa83E25HhvzoLxlE3uc0s%3D&reserved=0. Generally speaking, new proposals should be forward-compatible with the design sketch; that is, the new features proposed would continue to be at home when surrounded by other dependent-type features.
Of course, the committee remains free to revise the design sketch or to accept proposals that encroach upon it (i.e. contradicting this guidance), but such choices should be made explicitly.
See also the committee's Review Criteriahttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2F%23review-criteria&data=04%7C01%7Csimonpj%40microsoft.com%7C1b7abe0682c0408df2f708d8f8fbeb5f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533108900954303%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=jSLVnZCggbNtM8QkU26f2WaulvymUb%2BEaGIO6E5%2B8%2FU%3D&reserved=0: put another way, this proposal says that we consider the design sketch alongside other features of today's Haskell when assessing a new proposal's fit with the language.
Note that compatibility with dependent types is far from the only criterion the committee would use to evaluate a proposal. Other review criteria, such as learnability, clarity of error messages, performance, etc., remain just as ever.
Any views? Let's try to converge rapidly.... the proposal has been substantially refined by a lot of debate.
Simon
