I think I would also prefer to have a more concrete proposal that we would conditionally accept. The only thing to be careful about is to make clear which parts of the design you consider absolutely necessary (eg the unification of type and term syntax) and which you consider more up for debate and refinement. On Mon, Mar 29, 2021, at 23:27, Richard Eisenberg wrote:

Iavor raises an interesting point.

I wrote Proposal #378 in the way I did (somewhat vaguely, about design decisions made by the committee) because I hadn't yet pinned down exactly what DH was in a way that would make for a more proper proposal. I knew we needed the Syntactic Unification Principle and some of the other high-level goals, but I hadn't articulated these to myself or to anyone else.

However, thanks to Simon PJ's patient help and then initiative in starting https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell, we now have something much closer to a proper proposal than I expected to end up with. It's not exactly fully specified in a few places, but I think this page is good enough to consider for some sort of conditional approval. Then, maybe we could get to implementing it (perhaps in pieces) and use that real experience to refine the proposal and revisit the conditional acceptance via modifications to the design.

What do others think? I'm happy to rephrase #378 as a more proper proposal (albeit seeking only conditional acceptance) if we think it's mature enough to.

However, if the current text is not mature enough to form the basis of a more proper proposal, I do not wish to invest lots and lots more time in fleshing out a general direction that the committee is uninterested in. So perhaps the real goal of my writing #378 is to surface the appetite of the committee in pursuing this direction. There is always a chicken-and-egg problem in making a choice about direction, in that it's hard to know the pros and cons of an unexplored avenue of inquiry. But maybe we have enough information now that we can make such a decision without further anticipatory exploration.

Thanks, Richard

...

On Mar 29, 2021, at 12:39 PM, Iavor Diatchki wrote:

Hello,

my preference would be to reject this proposal, and turn the "proposed design for dependent haskell" (the link in Simon's e-mail) into its own proposal so that we can discuss it, and suggest changes. It seems really odd to agree to adhere to a design that we never discussed.

By the way, it's really great to finally see something written down about the actual design of DH. I had a quick read, and I have some questions, which is why I think it makes more sense to have the design as its own proposal. In particular, it seems to me like it might be quite possible to split the DH design into a collection of separate extensions, which might make it easier to understand, although I don't fully understand the whole picture, and might be wrong about that.

-Iavor

On Mon, Mar 29, 2021 at 5:17 AM Simon Peyton Jones via ghc-steering-committee wrote:

...

Dear GHC Steering Committee____

...

...

I’m recommending acceptance of Proposal #378: Support the design for dependent types https://github.com/ghc-proposals/ghc-proposals/pull/378____

...

...

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://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell. 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://github.com/ghc-proposals/ghc-proposals/#review-criteria: 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

---

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

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

I agree with Vitaly on this not being a proper proposal. My main objection is that it indirectly brings all of https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell into the proposal, but in a sort of “we can still be wrong” mode. Personally, I’ll be happier to see the wiki page turned into a sort of “proposal roadmap” or something along those lines. Alejandro On 30 Mar 2021 at 15:08:42, Vitaly Bragilevsky wrote:

I don't see this proposal as a proper GHC proposal. I don't think we should accept or reject it. We don't have a formal check for committee criteria anyway. Am I in support of introducing DH into GHC? Yes, I am. But then I'll be more inclined to support Richard's objections to any other proposals if they contradict the DH design sketch. I don't need to swear to follow these additional criteria.

Vitaly

пн, 29 мар. 2021 г. в 15:17, Simon Peyton Jones via ghc-steering-committee :

...

Dear GHC Steering Committee

I’m recommending acceptance of Proposal #378: Support the design for dependent types https://github.com/ghc-proposals/ghc-proposals/pull/378

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://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell. 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://github.com/ghc-proposals/ghc-proposals/#review-criteria: 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

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