[ghc-steering-committee] Scoping of types

Joachim Breitner mail at joachim-breitner.de
Sun Aug 15 20:58:57 UTC 2021


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 <simonpj at microsoft.com> 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 <ghc-steering-committee-bounces at haskell.org> On
> > >  Behalf Of Joachim Breitner
> > >  Sent: 09 August 2021 10:55
> > >  To: ghc-steering-committee at 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 at 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 at 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 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/




More information about the ghc-steering-committee mailing list