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

Tue May 18 07:47:22 UTC 2021

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.

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:

> Many industrial Haskellers came out of the woodwork to support this
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 <ghc-steering-committee at haskell.org> 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 <simonpj at microsoft.com>
> *Sent:* 15 April 2021 10:39
> *To:* ghc-steering-committee at haskell.org
> *Cc:* Simon Peyton Jones <simonpj at microsoft.com>
> *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 <ghc-steering-committee-bounces at haskell.org>
> *On Behalf Of *Simon Peyton Jones via ghc-steering-committee
> *Sent:* 06 April 2021 13:58
> *To:* ghc-steering-committee at 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 <simonpj at microsoft.com>
> *Sent:* 29 March 2021 13:17
> *To:* ghc-steering-committee at haskell.org
> *Cc:* Simon Peyton Jones <simonpj at 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 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 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/20210518/9ec75f11/attachment.html>