Can you, maybe, summarize what the various options are? And their conflicts? On Fri, Jul 30, 2021 at 11:53 AM Alejandro Serrano Mena wrote:

Sorry, I was not clear about the goal of the message. This all stems from the fact that Joachim asked me to shepherd #238. However, when trying to do so, I found that this was not the only proposal changing some of the scoping of types, but that there’s a lot going on with regards to that field.

My question to the Committee is: should we continue shepherding the proposals independently, or should we take some time to make a general judgment about how we want scoping to work on types, in the same way that we had a general Dependent Haskell proposal?

Regards, Alejandro

El 29 jul 2021 16:38:07, Spiwack, Arnaud escribió:

...

I'm not sure what way forward you are suggesting (and judging from the lack of response, it's probably not clear for the other committee members either).

Philosophically, there is a balance to strike between backward compatibility and consistency. I'd note however that all of the existing behaviour is gated behind `ScopedTypeVariables`, which is fairly stable, but not necessarily unmovable. I don't think breaking backward compatibility would be unsurmountable.

On Fri, Jul 23, 2021 at 11:50 AM Alejandro Serrano Mena < trupill@gmail.com> wrote:

...

Dear Committee,

There’s a lot happening right now in the GHC proposals repo about scoping of types in different elements in the language. Richard asked for our decision in #238, but following a very good suggestion from Joachim, I think it’s better to give an overview on what’s going on. In my opinion, this should lead to a consolidation of the different proposals into a unified design.

*Current status*

In Haskell 2010 there’s no way to refer to type variables introduced in a type signature. For a long time, GHC has shipped with -XScopedTypeVariables, which introduced scoping for types by prepending them with `forall`. We could then use it in other types, or as part of a type application if -XTypeApplications is on.

...

id :: forall a. a -> a id x = f @a x where f y = y

In the past 3 years we’ve accepted two proposals which extend this ability: - First to patterns https://github.com/ghc-proposals/ghc-proposals/pull/126, so we can write `id @a x = …` - Then to lambdas https://github.com/ghc-proposals/ghc-proposals/pull/155, so we can write `id = \@a x -> …`

*What is going on*

It seems that the accepted proposals were not quite right. We have two on-going proposals to *amend* the current ones: - https://github.com/ghc-proposals/ghc-proposals/pull/291 proposes simplifications to type variable patterns. As I understand this would make type variables in patterns behave like term variables (cannot be repeated, occurrences in inner scopes shadow the outer one, and so on). - https://github.com/ghc-proposals/ghc-proposals/pull/238 introduces -XTypeAbstractions, which make the combination of `forall` and `\@a` behave “as it should be”. But to be honest, I do not fully grasp the problems before, so neither how this amendment solves the problem; there’s a pointer to the GHC issue tracker where some incompatibility is discussed https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412 - https://github.com/ghc-proposals/ghc-proposals/pull/420 amends the current behaviour of signatures in patterns (what happens if I write `id (x :: a)` ).

So we have different ways to introduce new type variables: `f :: forall a. …`, `f @a = …`, `f = \@a -> …`, `f (x :: a) = …`; and it’s very unclear what the scoping mechanism for each one should be. I think the problem is characterised very well in the following comment by Simon PJ https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-7267159...

Note that this problem is arising in other places, too. For example #281, which adds visible `forall a -> ` ( https://github.com/ghc-proposals/ghc-proposals/pull/281) is also talking about name resolution (see https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-8848100... for an example).

*How should we proceed*

Personally, I am a bit worried about having divergent designs on this matter, and the fact that no fewer than 2 amendments are being proposed (!) For me, the best would be to come up with a unified design of how scoping works for types, covering all possible ways to introduce and resolve them. I am happy to help with this.

Another important point seems to be how far we want to get from the current status quo (-XScopedTypeVariables make a type variable in a signature scope in its body, type variables in pattern signatures are always fresh), and how that fits with the overall -XDependentHaskell initiative.

Kind regards, Alejandro _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I spoke to Richard about this. He is planning to respond to your call | What do you think, how should we proceed? Does anyone feel a calling to | guide this process to a conclusion? Maybe his shepherding of #425 (invisible binders in type declarations) is a good fit with that enterprise. Thank you Richard! Simon | -----Original Message----- | From: ghc-steering-committee On | Behalf Of Joachim Breitner | Sent: 09 August 2021 10:55 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Scoping of types | | Hi, | | I wasn't technically asking you to shepherd it, merely to assign a shephard | and write the necessary mails and other red tape that I wasn't keen on doing | on the phone while traveling. But now I have a proper keyboard again, so I | can do this. Or I can try. | | There are three proposals in the air that are somewhat related, and might be | worth being shepherded together. We have done that before, and it makes | great sense. In fact, I would consider it within the powers of a shepherd to | take two related proposal and work them into one. | | We have these proposals that related to "type variables and patterns": | (summaries are mine and might be wrong) | | #291: Simplify scoping for type applications in patterns | | This makes the "a" in a (Just @a _) pattern to always bind a new | type variable, it is never an occurrence (as it would be under | the accepted "#126 Type Varialbes in TPatterns" | | #238: Introduce -XTypeAbstractions, limiting -XScopedTypeVariables | | This refines/fixes "#155 Binding type variables in λ exprs", | splits up ScopedTypeVariables, introduces a @(..) short-hand | (the dots are syntax, not metasyntax). | | #420: no-implicit-binds: Adjust defaulting of -XPatternSignatureBinds | | This modifies "#285 -XNoImplicitForAll, - | XNoPatternSignatureBinds", which itself partly breaks out | existing behavior into two new extensions (ImplicitForAll, | PatternSignatureBinds) | | Fun fact: #285 includes wording like "or, if #238 is accepted:" | | | So, if I see it correctly, we have _three_ accepted proposals related to | type variables (#126, #155, #285), which are all unimplemented. On top of | that, we have three open proposals modifying these. This is all very | confusing and doesn't feel quite effective to me. It's not unusual that | proposals are accepted but don't get implemented for a while, but it can be | a sign that they are not quite right yet. | | So I am almost of a mind to un-accept #126, #155, #285, and, together with, | #291, #238, #420 mark then at "needs unifiying revision", and asking the | authors and all interested parties to come up with one (1) unifying proposal | that covers it all. | | Well, maybe this is a bit too harsh, but in principle it seems more | productive to juggle this set of unimplemented proposals, proposal modifying | proposals and conditional proposals. | | Or maybe all it needs is a single shepherd who is motivated to clear this | jungle for us. | | What do you think, how should we proceed? Does anyone feel a calling to | guide this process to a conclusion? | | | Cheers, | Joachim | | -- | Joachim Breitner | mail@joachim-breitner.de | | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim | - | breitner.de%2F&data=04%7C01%7Csimonpj%40microsoft.com%7Cc73b2d6cfc814077 | 015d08d95b1bc947%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63764099718817 | 7261%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1 | haWwiLCJXVCI6Mn0%3D%7C1000&sdata=nUxjVT1dUp8eizt7faWgnuF%2BWWPHj6e2Rug3K | d5usGU%3D&reserved=0 | | | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haske | ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cc73b2d6cfc814077015d0 | 8d95b1bc947%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637640997188177261% | 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi | LCJXVCI6Mn0%3D%7C1000&sdata=BkvvfLPKEqhO24Q%2FLVJXnW2i%2F5YiesjTMcA6FXC2 | zNI%3D&reserved=0

Hi, thanks! At the risk of sounding like a broken record: One thing that I found missing in the proposals so far (but maybe I just didn’t see it) is a good idea of very obviously (convenient and easy to spot syntax) and in a unifying way (types and terms the same way – of course!) distinguishing between occurrences and binders of variables in a pattern. Binders? Of course the main thing on a pattern. Occurrences in types? Also not unheard of; was a big part of #126. Occurrences in terms? Sounds odd, but I believe that not having a good syntax for that is one of the main reasons we currently can’t abstract pattern synonyms over terms, but that such abstraction is useful and will eventually come, and it would be great to already now use a syntax on the type level that we can use on the terms level as well. (After all, we want to get rid of the syntactic levels.) Given that ocurrences are the rarer case (both in terms and types), maybe a simple “marker” would work? But I have no obviously compelling solution to offer. With that wish list item voiced, I am looking forward to your proposal :-) Cheers, Joachim Am Sonntag, dem 15.08.2021 um 14:38 +0000 schrieb Richard Eisenberg:

Yes, indeed. Time is remarkably squeezed for me right now (which is why I'm working on a Sunday morning). Don't expect any action here before September. But I plan to synthesize this little bundle of proposals into something coherent soon. I don't expect any real changes over what's currently proposed -- just a more coherent & unified presentation, accompanied by typing rules.

Richard

...

On Aug 14, 2021, at 11:40 AM, Simon Peyton Jones wrote:

I spoke to Richard about this. He is planning to respond to your call

...

What do you think, how should we proceed? Does anyone feel a calling to guide this process to a conclusion?

Maybe his shepherding of #425 (invisible binders in type declarations) is a good fit with that enterprise.

Thank you Richard!

Simon

...

-----Original Message----- From: ghc-steering-committee On Behalf Of Joachim Breitner Sent: 09 August 2021 10:55 To: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Scoping of types

Hi,

I wasn't technically asking you to shepherd it, merely to assign a shephard and write the necessary mails and other red tape that I wasn't keen on doing on the phone while traveling. But now I have a proper keyboard again, so I can do this. Or I can try.

There are three proposals in the air that are somewhat related, and might be worth being shepherded together. We have done that before, and it makes great sense. In fact, I would consider it within the powers of a shepherd to take two related proposal and work them into one.

We have these proposals that related to "type variables and patterns": (summaries are mine and might be wrong)

#291: Simplify scoping for type applications in patterns

This makes the "a" in a (Just @a _) pattern to always bind a new type variable, it is never an occurrence (as it would be under the accepted "#126 Type Varialbes in TPatterns"

#238: Introduce -XTypeAbstractions, limiting -XScopedTypeVariables

This refines/fixes "#155 Binding type variables in λ exprs", splits up ScopedTypeVariables, introduces a @(..) short-hand (the dots are syntax, not metasyntax).

#420: no-implicit-binds: Adjust defaulting of -XPatternSignatureBinds

This modifies "#285 -XNoImplicitForAll, - XNoPatternSignatureBinds", which itself partly breaks out existing behavior into two new extensions (ImplicitForAll, PatternSignatureBinds)

Fun fact: #285 includes wording like "or, if #238 is accepted:"

So, if I see it correctly, we have _three_ accepted proposals related to type variables (#126, #155, #285), which are all unimplemented. On top of that, we have three open proposals modifying these. This is all very confusing and doesn't feel quite effective to me. It's not unusual that proposals are accepted but don't get implemented for a while, but it can be a sign that they are not quite right yet.

So I am almost of a mind to un-accept #126, #155, #285, and, together with, #291, #238, #420 mark then at "needs unifiying revision", and asking the authors and all interested parties to come up with one (1) unifying proposal that covers it all.

Well, maybe this is a bit too harsh, but in principle it seems more productive to juggle this set of unimplemented proposals, proposal modifying proposals and conditional proposals.

Or maybe all it needs is a single shepherd who is motivated to clear this jungle for us.

What do you think, how should we proceed? Does anyone feel a calling to guide this process to a conclusion?

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de

https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim - breitner.de%2F&data=04%7C01%7Csimonpj%40microsoft.com%7Cc73b2d6cfc814077 015d08d95b1bc947%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63764099718817 7261%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1 haWwiLCJXVCI6Mn0%3D%7C1000&sdata=nUxjVT1dUp8eizt7faWgnuF%2BWWPHj6e2Rug3K d5usGU%3D&reserved=0

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haske ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cc73b2d6cfc814077015d0 8d95b1bc947%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637640997188177261% 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi LCJXVCI6Mn0%3D%7C1000&sdata=BkvvfLPKEqhO24Q%2FLVJXnW2i%2F5YiesjTMcA6FXC2 zNI%3D&reserved=0

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