Dear Committee, I still have mixed feeling about this, but they are more about the whole “Dependent Haskell” project as a whole than about this specific proposal, which I find now in really good shape. On the one hand, I fear that by introducing more and more DH features, the language will morph into something difficult to reconcile with “basic Haskell”. After all, if we have dependent features available, why not use it in the Prelude and other libraries? This would make Haskell harder to use in (1) teaching, since newcomers would need more time to understand those features, and (2) research, since to build a tool on top of Haskell (think of LiquidHaskell) you’ll need to buy the whole “dependent + linear paradigm” too. On the other hand, the status of type-level computation in GHC is less than ideal: too many separate extensions, each of them adding a tiny bit of expressiveness, and a handful of folklore tricks. On that regard, having a prospective design of the future is great, because (1) it allows for a more cohesive set of features, and (2) helps on focusing the goals of the broader community. And since GHC already have some of those features, it’s actually possible to stop the boat sailing on the direction of dependent + linear types? Is this the design we want? is yet another question. I am quite confident about the maturity of the design, knowing that the authors have been working on this problem for years (even more a decade?). Regards, Alejandro On 18 Apr 2021 at 11:26:14, Joachim Breitner wrote:

Dear Committee,

Richard has now revised the “Design for Dependent Types” proposal,

and has resubmitted it.

I am in support of this proposal. I expect it will be painful at times to go that route, and it will creak at the edges, but my sense is that this eventual unification of types and terms is something that will become something we’d expect from a “modern language”, a bit like we expect function types and lambdas these days, and I have some hope that eventually, in a relatively far away future, Haskell will nicer and simpler because of this

The alternative, sticking to a non-dependent design (and yes, getting some benefits from that too), could lead to Haskell becoming a “language of the 00s”. Useful, mature, great to get work done, still something that not everybody knows and you can still feel a bit special for knowing it. But no longer the language that is _both_ productively usable and at the same time incorporates new, research-close features. It might become a bit like Perl in that sense. (Ok, that’s a bit too gloomy … take it as hyperbole).

I expect that discouraging punning will be maybe the most painful part of that route, for the wider community. import GHC.Tupe; swap :: Tuple [a,b] -> Tuple [b,a] just isn’t as smooth as `swap :: (a,b) -> (b,a)`. (And we can’t even cargo-cult from the ML family and use `(a * b) -> (b * a)` for the type of types…) I acknowledge that, I wish there was a better solution, but what’s in #378 seems to be the least bad.

I am amused that this proposal rests on a PEP, and happy to see that the LSP gets a more central role in the language design ;-)

Cheers, Joachim

PS: Quick note about #291 (type variables in patterns), just to record my current thinking:

I understand the reasoning, it would be nice to treat a `@(Maybe a)` argument like a `(Just x)` argument in patterns, binding `a`. But I am not convinced we can afford to toss out the ability to use an _occurence_ of a type `a`. My interpretation of #378’s implication on #291 is that we’ll have to find a way to distinguish binders from ocurrences that works independently of types and values (I believe we do need it for types, and I think we should have this for values as well anyways, as PatternSynonyms _should_ be able to abstract over patterns that have _required_ values, not just required constraints.)

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Dear Committee, I support this proposal. I think, that the hardest problem when teaching Haskell is not to get through the basics. Many of us who have teaching experience all know how to get that done. The real problems come with type-level magic and workarounds involving singletons. I often find that it's much easier to explain and solve the very same problems in Idris than in Haskell. If we want to use the corresponding features in Haskell (and many of Haskellers really want that), we must make them clearer. I believe that DH (as sketched in this proposal) is the right way to do that. Every now and then I hear the question if we are going to get dependent types in Haskell. I'm sure, Richard answers this question on a daily basis. I consider accepting this proposal as a clear statement to those who wait for dependent types in Haskell. So, let's do that! Vitaly пн, 19 апр. 2021 г. в 19:04, Richard Eisenberg :

On Apr 19, 2021, at 3:03 AM, Alejandro Serrano Mena wrote:

On the one hand, I fear that by introducing more and more DH features, the language will morph into something difficult to reconcile with “basic Haskell”. After all, if we have dependent features available, why not use it in the Prelude and other libraries? This would make Haskell harder to use in (1) teaching, since newcomers would need more time to understand those features, and (2) research, since to build a tool on top of Haskell (think of LiquidHaskell) you’ll need to buy the whole “dependent + linear paradigm” too.

Both of these are great points to raise. For (1): we will have to continue to use good taste in designing the Prelude/`base` and other libraries. Lots of fancy features have existed in Haskell for decades, but we have been careful in how these are exposed to users. One small blunder happened a few years ago when `:t ($)` became very unwieldy (showing $'s levity polymorphism), and that got fixed before release. Another blunder (in my opinion) is that the type of length now requires understanding Foldable -- but the code around Foldable & Traversable is all Haskell98 anyway. It remains vitally important that error messages and GHCi interactions remain understandable to beginners. I personally would consider it a failure of this project if that were not to be the case. I have added some thoughts around this to the proposal at https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0...

For (2): This is harder. I suppose a researcher could consider Haskell without -XLinearTypes -XDependentTypes, but any GHC-based implementation would be out of reach, then. Regardless, many Haskell-based research papers already choose a slice of GHC/Haskell to study, and I expect that to continue to be the case. However, I acknowledge that research accessibility may decrease with this change.

Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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

On Tue, May 18, 2021 at 8:37 PM Richard Eisenberg wrote:

...

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.

I stand by this claim -- though I can see how the language here might be off-putting. This section is meant to be a summary of the discussion, and this really was a part of the discussion. However, I have replaced this bullet with a narrower one, describing the particular worry about people being forced to use dependent types because of early library adoption.

You are claiming that they don't agree with the proposal because they don't understand. It's a very strong claim to make. But you've changed the sentence already, so I guess no point in arguing further.

...

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.

I disagree here. The GitHub ticket has 412 positive emotions, and 3 negative ones. The 412 might be an overcount, because I believe one individual can put multiple emoji on the same ticket, but there are at least 274 individuals in favor. It's true that I don't know how many of these are industrial users, but there were quite a few people who identified as industrial users in support. I actually don't know that any of the detractors identified themselves as industrial users, though I didn't read through all the comment trail to check this.

We don't -- and shouldn't -- operate solely (or primarily) on the basis of popularity, but I think both the emoji expressed and the comment trail suggests that this feature is desired in industry more widely than it is opposed.

There is no doubt that the idea of Dependent Haskell is popular (Dependent Haskell in general, and this proposal in particular), but I'm not sure that this is what your sentence is claiming (I wouldn't object to this claim!). If it's not misleading, this claim is at least very hard to verify. It does make me uncomfortable (as for industrial contradictors I remember Matt Parsons being one of them). PS: I didn't mean to imply that there being few claims/design choices in the proposal was a bad thing. I suppose, though, that like many such high-level summaries of a thing one comments, it was meant mostly for my own consumption, to ground my reasoning. /Arnaud

Hi, Am Mittwoch, den 19.05.2021, 22:21 -0400 schrieb Eric Seidel:

...

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 am actually not opposed to compromising on the OIP, and would not mind seeing new features of Haskell be used in basic libraries where they make sense. Base has `HasCallStack`. It has Rank2Polymorphism. It has type equalities. It has generics, and thus associated types. I am not opposed to keeping simple things simple, and just along the desire to break no more code than necessary as we change basic libraries will help. But overall I’d rather compromise on OIP than on, say, using the right tool for the right problem. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I have since heard from Tom, Eric, and Arnaud; and Iavor has stepped down from the committee. So we have * Support: Tom, Eric, Arnaud, Joachim, Vitaly, Alejandro, Vlad (plus Richard and myself) * Against: no one That leaves: Cale and Simon M. At this point I think we have enough support to declare the proposal accepted. Joachim, can you merge it? Thanks Simon From: Simon Peyton Jones Sent: 13 May 2021 16:09 To: ghc-steering-committee@haskell.org Cc: Simon Peyton Jones Subject: RE: Recommendation for #378: support the design for dependent types Friends You have now had a month to review my recommendation below, to accept #378: support for dependent types. Here it is once morehttps://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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493133964%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=QjIYtMwzGAKby2bqezO9AmUchHO9zUyGhzSOCJPlTms%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 requesthttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F378&data=04%7C01%7Csimonpj%40microsoft.com%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493143963%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=lOdCJyt61%2B6elYx1npgMG9BBsrHD1FHg%2BFo0IbylndM%3D&reserved=0, 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 mailto:simonpj@microsoft.com> Sent: 15 April 2021 10:39 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 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://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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493143963%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=wTdlzqgSiFRe5hwoaHG2s6ukIv2eAaEY1M%2F%2FbDxrRII%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 mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Simon Peyton Jones via ghc-steering-committee Sent: 06 April 2021 13:58 To: ghc-steering-committee@haskell.orgmailto: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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493153956%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=MxflQbPVLwdC0uGcrJ7P%2FkZzsqIgt1vo%2BPfExxjYkS4%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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493163947%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=VBTZfqvQ8fEISn39rMwYV0zc6uXV8g07l8y4aZ0WcAI%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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493163947%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=qoyKKGDL%2Fz6JMu%2FC3SMBmjnC24KJFic1i57iG7AG8hY%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%7C7e737205b1e3428cc18208d916210e74%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637565153493173941%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=bz9L49gK5qLs5RArmLvfcOS7GfdMY3FyJm5cthB%2BFI8%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

Thanks, all! :) I think the ability to write up (collaboratively with Simon) and discuss a proposal such as this one publicly really shows the virtue of the proposal process. Thanks for all the feedback here! Richard

On May 26, 2021, at 3:38 AM, Joachim Breitner wrote:

Am Mittwoch, den 26.05.2021, 07:20 +0000 schrieb Simon Peyton Jones via ghc-steering-committee:

...

At this point I think we have enough support to declare the proposal accepted. Joachim, can you merge it?

Done! -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee