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

Hi, Richard roughly says what is my sentiment too… I’d phrase it like this: It seems that #281 would be rather straight forward, if it were not for the fact that this is the first (of many?) extensions that allow types and terms to occur in the same syntactic spot. So far, when mentally parsing a program, I know where to look for types, and where to look for terms. #281 breaks that, and has to come up with lots of subtle rules, that make me uneasy. But that's not really #281’s fault – assuming we want to head towards Dependent Haskell with a unified namespace, it’s a problem that needs to be solved! But better have that discussion with a focus on that problem, and have a plan that works in general. Maybe #270 is the right place to have that discussion. My impression is that all (most?) of those working towards a Dependent Haskell world assume that we get a unified namespace with no punning, and all complexity (`type` sigils, `type`-qualified imports) is around compatibility with modules that use punning, with the hope that this is rare. Few are proposing to stick to a world of two namespaces and punning and make _that_ ergonomic. Is that impression correct? Do local modules (#283) alleviate the punning problem a bit? Given `data T = T`, could we make it so that T is the type and T.T the constructor? But this really isn't the right place to throw out shower ideas. I wonder if it would help if someone could maintain a wiki page with an overview of all the numerous proposals and ideas thrown around to tackle the problem about how we get from a world of two name spaces and punning to one with one namespaces and no punning. As for #281, unless I misjudge the urgency of that change, I’d be in favor to park it until we have a good, generally applicable plan for mixing terms and types. Cheers, Joachim Am Montag, den 23.11.2020, 03:35 +0000 schrieb 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-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 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/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 https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ 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 https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/