Re: [ghc-steering-committee] Recommendation for #378: support the design for dependent types

Sorry, it's a long read. I'd read previous iterations of the proposal, and the wiki page previously. But the current proposal is yet a different text, I didn't want to opine without a proper reading. The proposal is long, but doesn't really make a lot of concrete design choices. - Extend the name lookup in type syntax to lookup in the term namespace when the name is absent in the type namespace - A syntactic form `type …` to switch to the type namespace in terms - Extend the term syntax to be a superset of the type syntax. - Dependent Haskell is to be (mostly) backward compatible I think that's about it. The rest establishes terminology and serves mostly as documentation. And it does a pretty good job at it, I think. The proposed changes seem reasonable. The language, though, is sometimes interesting:

By accepting this proposal, the committee reaffirms Haskell's status as an evolving, forward-thinking language, excited to adopt new ideas.

There remain a few individuals who appear to remain deeply unconvinced. However, these seem to be a small minority. The reasons they are not convinced appear to be around lack of understanding of the proposal/design and general worry about unintended consequences. I have tried to address both of these, but I do not believe my efforts have been fully successful.

Many industrial Haskellers came out of the woodwork to support this

This is really not helpful, I don't think that we want to merge the proposal with this sort of language in it. I'd add that the following: proposal. is rather misleading, since there seem to have been just as many industrial Haskellers which came out opposed to the proposal. --- In summary: I'm in favour of the proposal, as long as Section 5 (Effect and Interaction) and below, are cleaned of the politically charged language. On Thu, May 13, 2021 at 5:09 PM Simon Peyton Jones via ghc-steering-committee wrote:

Friends

You have now had a month to review my recommendation below, to accept #378: support for dependent types. Here it is once more https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362468484%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=K1JBnklN2ztnUyibLJ%2Bv9q8%2BK%2Bg1Sf%2FHDGjwVmj25Mw%3D&reserved=0

I have heard

- Support: Joachim, Vitaly, Alejandro, Vlad (plus Richard and myself) - Against: no one

But that leaves *Tom, Eric, Arnaud, Cale, Simon M, and Iavor* who have not expressed an opinion. Please do!

Failing further feedback, I’ll accept on Tuesday next week.

There has been some further discussion on the pull request https://github.com/ghc-proposals/ghc-proposals/pull/378, but I don’t think any fundamentally new points have come up. This is clearly a judgement call, but one I think we should make. Haskell has always been a research lab – that’s part of what makes it distinctive. I think we can continue to celebrate that innovation. But see my email immediately below for what we are and are not accepting.

Simon

*From:* Simon Peyton Jones *Sent:* 15 April 2021 10:39 *To:* ghc-steering-committee@haskell.org *Cc:* Simon Peyton Jones *Subject:* Recommendation for #378: support the design for dependent types

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 more https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362468484%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=K1JBnklN2ztnUyibLJ%2Bv9q8%2BK%2Bg1Sf%2FHDGjwVmj25Mw%3D&reserved=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 wiki https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fdependent-haskell&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362478476%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C5Ywef9f5MK4jEc2XfmXeZ26YIdJeP0%2F%2BKfGdIhfkYA%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 *Sent:* 29 March 2021 13:17 *To:* ghc-steering-committee@haskell.org *Cc:* Simon Peyton Jones *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 types https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F378&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362478476%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=%2Bf32VqzdL6HgiF436%2FGWPwBl09c1qo%2BAMbgPY6tJfSI%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 wiki https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fdependent-haskell&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362488470%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1xOofIrHU3rP91mxYwvKnefFqCA5RBHCUUuKHqtdZlo%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 Criteria https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2F%23review-criteria&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0e29b49960a43b4d7ee08d8fff24512%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637540763362488470%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C%2B6VLghDD03q1Qwqwytrp75eAHQtPF%2FB1SveNIKrymA%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 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee