[ghc-steering-committee] Please review "Visible 'forall' in types of terms" #281

[Richard Eisenberg]

My silence on this proposal is because I want to accept, but I agree with Iavor that it's become too baroque. My #378 is, in part, an attempt to clarify our stance on these sorts of features so that we can take a stab at simplifying #281 by making it less expressive.

So, I guess my vote is to delay decision on this proposal until we have one for #378 (or #270, which can also help shed light on this one).

Responding directly to Alejandro's concerns here: I actually don't really understand. I think (1) is decided by https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0081-forall-arrow.rst; we use this syntax in standalone kind signatures in GHC 8.10. We *could* change this if there were a compelling reason, but this proposal is just continuing an existing feature. By (2), I think you're referring to all the complications in the proposals at how to deal with names and syntax in arguments -- I wouldn't myself describe this as conflating the two namespaces, but rather as defining a subtle set of rules for interpreting ambiguous names. It's the subtlety of these rules that makes me uncomfortable. For (3), I don't really think there's much there -- and what there is seems to require (2) (and vice versa). Do you have an example of a type-inference interaction you're worried about here?

Richard

> On Nov 22, 2020, at 12:09 PM, Alejandro Serrano Mena <trupill at gmail.com> wrote:
> 
> Hi all,
> For me, there are two main concerns here:
> This could be split on different proposals: (1) using the “forall a ->” syntax, (2) conflating the type and term syntax and namespaces, (3) introducing checking and inference for it;
> I find the claim that you can just take the Quick Look Impredicativity paper, make a couple of adjustments, and get correct checking and inference. This kind of big change is the one for which I would actually expect a peer-reviewed paper.
> 
> Regards,
> Alejandro
> 
> El El sáb, 21 nov 2020 a las 10:10, Joachim Breitner <mail at joachim-breitner.de <mailto:mail at joachim-breitner.de>> escribió:
> Dear Committee,
> 
> Iavor suggested to reject this proposal, but we have not heard a lot
> here yet. Especially before rejecting proposals, we probably owe a
> careful analysis, possibly with suggestions of ways forward (splitting
> the proposal into smaller pieces maybe? Iavor says there are many
> changes there).
> 
> If we have continued silence, we’d reject.
> 
> Cheers,
> Joachim
> 
> 
> Am Mittwoch, den 11.11.2020, 13:41 -0800 schrieb Iavor Diatchki:
> > Hello,
> > 
> > Proposal #281 has been submitted for review by the committee again, please read through it and let's have a discussion.   Here are links to the proposal's discussion section, and the proposal text:
> > 
> > https://github.com/ghc-proposals/ghc-proposals/pull/281 <https://github.com/ghc-proposals/ghc-proposals/pull/281>
> > https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst <https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst>
> > 
> > While I suggested acceptance on the previous version, I am leaning towards rejecting the proposal  now.  My reasoning is that I hadn't fully understood all the aspects of the original proposal, and the new proposal seems to lack a simple modular specification.  There are *many* changes described in the document,  but I found it hard to understand what is the current design, from the point of view of a user of the feature, as opposed to someone trying to implement it.
> > 
> > I'd be curious about what others think.
> > 
> > -Iavor
> > 
> > 
> > _______________________________________________
> > 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>
> -- 
> Joachim Breitner
>   mail at joachim-breitner.de <mailto:mail at joachim-breitner.de>
>   http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
> 
> 
> _______________________________________________
> 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/20201123/3bfbb3f6/attachment.html>