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

Mon Nov 23 08:10:16 UTC 2020

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