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

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-fo...; 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 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 mailto:mail@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/000... https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000...

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@haskell.org mailto:ghc-steering-committee@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@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee