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

[Richard Eisenberg]

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 <iavor.diatchki at gmail.com> 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 <ghc-steering-committee at haskell.org <mailto:ghc-steering-committee at haskell.org>> 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 at haskell.org <mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee>
> _______________________________________________
> 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/20210330/a1b4c52d/attachment-0001.html>