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

[Eric Seidel]

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 <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> 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
> >> 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
> 
> _______________________________________________
> 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
>