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

Thu May 20 02:21:46 UTC 2021

I've read through the whole proposal again. 

Thanks, Richard, for all the work you've put in to revising it. It's a much better proposal than when this started.

After reading through it again, I find myself feeling about the same as I did originally: open to the idea of dependent types in Haskell, but concerned about some of the details.

Interestingly, I found myself largely nodding along with much of the actual design in section 4, but am still unconvinced by the proposals referenced in section 1 that motivated this whole thing.

I'll reply here to a few pieces of the proposal, since my comments are more about viewpoints than technical details.

> Rejecting #291 amounts to prioritizing criterion 1; accepting it amounts to prioritizing criterion 2.

I still disagree that this proposal has much of anything to do with dependent types. Repeat occurrences of the same binder asserting type equality is a useful feature (the same would be true for term binders, I think I mentioned that in an earlier thread).

> On the other hand, #281 could be simplified considerably if it did not need to deal with the possibility of type/term ambiguity: that is, if there were no puns. For example, we could declare that the use of any punned identifier in a type argument is an error.

This doesn't seem at all compatible with the reality that Haskell has two namespaces, unless the point is that punned identifiers will need to be manually disambiguated with the `type/data` heralds mentioned later. If that's the case (I suspect so), the proposal should be more explicit about the expected resolution.

> The Opt-In Principle (OIP): Users who do not opt into dependent types will not be affected by them. By "opt into", we mean that users would have to enable -XDependentTypes or import a module that exposes functions with dependently-typed interfaces. These modules would not be standard modules that are routinely imported today, such as Data.List or Prelude.

This is a good principle, but I think you may be trying to have your cake and eat it too. I spent much of the past few years working in C++, which is a cautionary tale for complex language features. In particular, they end up everywhere, especially in core libraries, because generic, core libraries are precisely where you need all that extra power and expressiveness. Recently, I've been working in Scala, where I've observed the same thing. This is not to say that dependent types are bound to appear everywhere, they're a different feature, and C++ and Scala are infamous for their complexity, but I think it will be harder than you admit to keep core libraries free of dependent types. I'm also very glad to see in the following paragraph that you're thinking about ways to hide the complexity from users that don't need to worry about it, please keep that up!

> 4.4   Quantifiers

I'm pretty concerned about adding 3 more quantifiers to keep track of. The breakdown makes sense, but it's a lot of extra cognitive burden. I'm sure you would argue that these only become relevant in advanced use cases, but see above about the OIP.

---

On balance, I think you've done a commendable job of designing these features and principles to minimize disruption to existing code and users. What remains to be seen is how the community adopts and uses these features, and whether that creates a fork in the ecosystem. I will support this proposal, but will hold you to your promise to keep at least a veneer of simplicity over these features (like with $ and levity-polymorphism).

Thanks!
Eric

On Thu, May 13, 2021, at 11:09, 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 <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 <mailto:ghc-steering-committee%40haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 