As a co-author of the paper that came from this: yes, please! :)

On Jul 26, 2018, at 6:17 AM, Simon Peyton Jones via ghc-steering-committee wrote:

I’m a strong supporter. I think the proposal itself (which will have longevity) could be improved significantly, and have commented to that effect.

Simon

From: ghc-steering-committee On Behalf Of Iavor Diatchki Sent: 26 July 2018 09:09 To: ghc-steering-committee@haskell.org Subject: [ghc-steering-committee] Discussion about "Type Application in Patterns" (#126)

Hello,

let's also start the discussion on feature request 126. The idea here is that we allow the @ notation for explicit type applications to also be used on constructors in patterns. Using @ with a constructor in a pattern has the same meaning as it does it an expression: the provided type is used to instantiate the corresponding type parameter of the constructor. If the type contains variables, those are treated in the same way as in #128, where "unbound" variables name the matching types. Here are some examples:

f1 (Just @Int x) = x -- This has type `Maybe Int -> Int`

f2 (Just @[a] x) = x == "c" -- `a` is an alias for `Char`

f3 (SomeException @e ex) = ... -- `e` is a name for the existentially hidden exception type

Overall I think that is a simple and natural extension to the way @ already works, and I propose that we accept it.

Thoughts?

-Iavor

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

Could someone give me a motivating example for what this enables? If there is such in the paper, a link to the paper is fine. On Sat, Aug 4, 2018 at 10:27 AM, Joachim Breitner wrote:

Hi,

can we have an additional nod by someone who is not an author of the corresponding paper?

Also, I updated the proposal to answer the disambiguation with as- patterns: https://github.com/ghc-proposals/ghc-proposals/pull/126/commits/12d64105b097... And I would like a second pair of eyes there, as this choice blocks us from in the future allowing patterns on both sides on @, i.e. something like

Just (_ :_) @ (fun -> True) @ x

because

Nothing @ a

would be ambiguous.

Cheers, Joachim

Am Donnerstag, den 26.07.2018, 11:08 +0300 schrieb Iavor Diatchki:

...

let's also start the discussion on feature request 126. The idea here is that we allow the @ notation for explicit type applications to also be used on constructors in patterns. Using @ with a constructor in a pattern has the same meaning as it does it an expression: the provided type is used to instantiate the corresponding type parameter of the constructor. If the type contains variables, those are treated in the same way as in #128, where "unbound" variables name the matching types. Here are some examples:

f1 (Just @Int x) = x -- This has type `Maybe Int -> Int`

f2 (Just @[a] x) = x == "c" -- `a` is an alias for `Char`

f3 (SomeException @e ex) = ... -- `e` is a name for the existentially hidden exception type

Overall I think that is a simple and natural extension to the way @ already works, and I propose that we accept it.

Thoughts?

-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

-- Chris Allen Currently working on http://haskellbook.com

Seems reasonable to me. There's been a general push to eliminate cases for Proxy as well. On Sat, Aug 4, 2018 at 1:33 PM, Joachim Breitner wrote:

Hi,

Am Samstag, den 04.08.2018, 13:16 -0500 schrieb Christopher Allen:

...

Could someone give me a motivating example for what this enables?

with “this”, do you refer to type applications in patterns? The main fundamental motivation is to bind existential type variables. Currently we often do this using Proxy, but we’d like a more convenient syntax that mirrors type applications in patterns.

or do you refer to allowing complex patterns on both sides of an as- pattern? I don’t have an example for this handy, and maybe we actually never want that, in which case there is no issue.

Cheers, Joachim -- 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

-- Chris Allen Currently working on http://haskellbook.com

I'm in favor of accepting as well. On Mon, Aug 13, 2018, at 04:52, Iavor Diatchki wrote:

We've had this under discussion for just about 2 weeks, and there does not appear to be any objections, so I think we should accept it.

On Sat, Aug 4, 2018 at 10:05 PM Christopher Allen wrote:

...

Seems reasonable to me. There's been a general push to eliminate cases for Proxy as well.

On Sat, Aug 4, 2018 at 1:33 PM, Joachim Breitner wrote:

...

Hi,

Am Samstag, den 04.08.2018, 13:16 -0500 schrieb Christopher Allen:

...

Could someone give me a motivating example for what this enables?

with “this”, do you refer to type applications in patterns? The main fundamental motivation is to bind existential type variables. Currently we often do this using Proxy, but we’d like a more convenient syntax that mirrors type applications in patterns.

or do you refer to allowing complex patterns on both sides of an as- pattern? I don’t have an example for this handy, and maybe we actually never want that, in which case there is no issue.

Cheers, Joachim -- 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

-- Chris Allen Currently working on http://haskellbook.com _______________________________________________ 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

| And I would like a second pair of eyes there, as this choice blocks us from | in the future allowing patterns on both sides on @, i.e. something like | | Just (_ :_) @ (fun -> True) @ x Yes, this is a bit annoying. See the "Alternatives" section of the accepted proposal "As patterns in pattern synonyms", here: https://github.com/ghc-proposals/ghc-proposals/pull/94 The proposal points out that "@" makes sense as an "and-pattern", dual to "or-patterns" (which are, I hope, close to acceptance). However, if I read it aright, the proposed new syntax does NOT include Just (_ : _) @ (fun -> True) because in the proposal the thing to the left of the "@" must be a gcon, or another type application. So even if we added and-patterns, there's no ambiguity here. What would be ambiguous is this and-pattern: Nothing @ pat (i.e. with a nullary contructor as the first of p1@p2). But that's a pretty silly and-pattern so I think we could let this ambiguous case resolve as a pattern type application. You could I suppose write (Nothing)@pat to get the and-pattern. TL;DR: I don't think the current proposal blocks future more compositional use of "@". Simon | -----Original Message----- | From: ghc-steering-committee On | Behalf Of Joachim Breitner | Sent: 04 August 2018 16:27 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Discussion about "Type Application in | Patterns" (#126) | | Hi, | | can we have an additional nod by someone who is not an author of the | corresponding paper? | | Also, I updated the proposal to answer the disambiguation with as- | patterns: | https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com% | 2Fghc-proposals%2Fghc- | proposals%2Fpull%2F126%2Fcommits%2F12d64105b0979c674502c3768118b424d09a572b& | amp;data=02%7C01%7Csimonpj%40microsoft.com%7Cc38b4c2cc1b441aceca108d5fa1ed3b | 2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636689932664304509&sdata= | l2sjKwC3Lq16kzmfKB2dCEHktaDVVjj6IeGFrlCMhXQ%3D&reserved=0 | And I would like a second pair of eyes there, as this choice blocks us from | in the future allowing patterns on both sides on @, i.e. something like | | Just (_ :_) @ (fun -> True) @ x | | because | | Nothing @ a | | would be ambiguous. | | Cheers, | Joachim | | Am Donnerstag, den 26.07.2018, 11:08 +0300 schrieb Iavor Diatchki: | > let's also start the discussion on feature request 126. The idea here is | that we allow the @ notation for explicit type applications to also be used | on constructors in patterns. Using @ with a constructor in a pattern has | the same meaning as it does it an expression: the provided type is used to | instantiate the corresponding type parameter of the constructor. If the | type contains variables, those are treated in the same way as in #128, where | "unbound" variables name the matching types. Here are some examples: | > | > f1 (Just @Int x) = x -- This has type `Maybe Int -> Int` | > | > f2 (Just @[a] x) = x == "c" -- `a` is an alias for `Char` | > | > f3 (SomeException @e ex) = ... -- `e` is a name for the | > existentially hidden exception type | > | > Overall I think that is a simple and natural extension to the way @ | already works, and I propose that we accept it. | > | > Thoughts? | > | > -Iavor | > | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ | > ee | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cc38b4c2cc1b441ac | eca108d5fa1ed3b2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63668993266430 | 4509&sdata=n9ZojGAGBrwWi0CYzr8RVCjlKNFByoEZxvWahxTlAvc%3D&reserved=0

| pattern Ascii :: String | pattern Ascii <- (all isAscii -> True) | | and now | | foo (Ascii @ ('X':rest)) = | | is now longer as silly… That’s a good example. It's easy to work around: pattern And p q = p@q foo (Ascii `And` ('X' : rest)) = .. The proposal draw attention to whether ( (K) @type ) is or is not a legal pattern type application. I think currently it is not. So using "significant" parentheses would be another workaround. Neither workaround is truly satisfactory, but I think the goodness of type applications in patterns (which we know we want) is more important than truly uniform and-patterns (which no one is asking for, yet). Simon | -----Original Message----- | From: ghc-steering-committee | On Behalf Of Joachim Breitner | Sent: 16 August 2018 23:02 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Discussion about "Type Application | in Patterns" (#126) | | Hi, | | Am Donnerstag, den 16.08.2018, 08:46 +0000 schrieb Simon Peyton Jones | via ghc-steering-committee: | > What would be ambiguous is this and-pattern: | > Nothing @ pat | > (i.e. with a nullary contructor as the first of p1@p2). But that's a | > pretty silly and-pattern so I think we could let this ambiguous case | > resolve as a pattern type application. | | nullary constructors can be synonyms! | | pattern Ascii :: String | pattern Ascii <- (all isAscii -> True) | | and now | | foo (Ascii @ ('X':rest)) = | | is now longer as silly… | | > You could I suppose write | > (Nothing)@pat to get the and-pattern. | | Significant parenthesis? Ugh. | | But yeah, maybe it is good enough™ to deal with this particular corner. | | Cheers, | Joachim | | | | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joach | im- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C36168190ebda4 | 2b8bf1408d603c3e1bc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63670053 | 7181819165&sdata=xoZDGIrlYH6AS3Lq7VFSCWu311UV5RMCS0ZsrhhzvwA%3D&r | eserved=0

I hate to throw a wrinkle in, but much of this discussion assumes that type arguments come before other arguments after a constructor. This is true today, and there are no immediate plans to change it, but this assumption won't be valid if we have full dependent types. For example, we might want something like

data T where MkT :: forall k -> Int -> forall (a :: k). TypeRep a -> T

Now, we might get patterns like

foo (MkT k n @a r) = ...

Without whitespace-sensitivity, I don't think we'll be able to disambiguate between type pattern and as-pattern. (I thought for a moment that we could use the constructor arity as a guide, but this fails if we have two @-signs, where only one is meant to be a type pattern. We won't be able to tell which one!) Whitespace-sensitivity is bad, but it's not unprecedented in Haskell. Ignoring the layout rule (which is quite different), this is much more like the treatment of `.` and `$`. Specifically, `T . f` is T composed with f, while `T.f` is the name `f` from the module `T`. And `f $ (g x)` is f applied to (g x) while `f $(g x)` is f applied to a splice. Considering this future of relaxed ordering requirements on data constructors isn't compulsory, but I do think it's better if we don't paint ourselves into a corner around this. Thanks, Richard

On Aug 16, 2018, at 7:27 PM, Joachim Breitner wrote:

Hi,

Am Donnerstag, den 16.08.2018, 23:22 +0000 schrieb Simon Peyton Jones:

...

...

pattern Ascii :: String pattern Ascii <- (all isAscii -> True)

and now

foo (Ascii @ ('X':rest)) =

is now longer as silly…

That’s a good example. It's easy to work around:

pattern And p q = p@q

foo (Ascii `And` ('X' : rest)) = ..

nice. I included this in the proposal under “Costs and Drawbacks”, for future reference.

Cheers, Joachim

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

The rule is this, implemented in the lexer: With -XTypeApplications on, the character immediately before an @ determines how it is lexed. 1. If the character is a legal end-of-identifier character (respecting the state of the -XMagicHash flag), then the @ is an as-pattern. 2. Otherwise, then the @ is the beginning of a type application. I abbreviate the rule as talking about whitespace sensitivity, because if the character preceding the @ is, say, a +, then we lex +@ as a user-defined operator. This rule has been implemented since GHC 8.0 and applies in patterns as well as expressions. I don't think anyone noticed. :) So it works reasonably well. It's a silly rule and I'd be happy to do better, but I don't think it's strictly necessary to aim for better here. It would be reasonable to warn when a user writes an as-pattern that doesn't conform to this rule (with -XNoTypeApplications). Richard

On Aug 17, 2018, at 1:37 AM, Joachim Breitner wrote:

Hi Richard,

Am Donnerstag, den 16.08.2018, 22:28 -0400 schrieb Richard Eisenberg:

...

Considering this future of relaxed ordering requirements on data constructors isn't compulsory, but I do think it's better if we don't paint ourselves into a corner around this.

I agree.

But so what do we do? Already now require that there is no space between @ and the following token when the user wants to use type applications in the pattern?

And would we also require the user to add a space after an at-pattern? In which case we should probably start a deprecation cycle for the currently legal

foo (a @b) = …

Cheers, Joachim

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

Ha. We could tighten this up further to require a non-blank immediately after the @ for a type application. Thus f @Int or g @(Tree Int) but not f @ Int g @ (Tree Int) That would leave (p1@p2) and (p1 @ p2) free for patterns. Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 17 August 2018 17:18 To: Joachim Breitner Cc: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Discussion about "Type Application in Patterns" (#126) Note that this rule is documented, in brief, in the manual:

A visible type application is preceded with an @ sign. (To disambiguate the syntax, the @ must be preceded with a non-identifier letter, usually a space. For example, read@Int 5 would not parse.)

On Aug 17, 2018, at 12:16 PM, Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote: The rule is this, implemented in the lexer: With -XTypeApplications on, the character immediately before an @ determines how it is lexed. 1. If the character is a legal end-of-identifier character (respecting the state of the -XMagicHash flag), then the @ is an as-pattern. 2. Otherwise, then the @ is the beginning of a type application. I abbreviate the rule as talking about whitespace sensitivity, because if the character preceding the @ is, say, a +, then we lex +@ as a user-defined operator. This rule has been implemented since GHC 8.0 and applies in patterns as well as expressions. I don't think anyone noticed. :) So it works reasonably well. It's a silly rule and I'd be happy to do better, but I don't think it's strictly necessary to aim for better here. It would be reasonable to warn when a user writes an as-pattern that doesn't conform to this rule (with -XNoTypeApplications). Richard On Aug 17, 2018, at 1:37 AM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi Richard, Am Donnerstag, den 16.08.2018, 22:28 -0400 schrieb Richard Eisenberg: Considering this future of relaxed ordering requirements on data constructors isn't compulsory, but I do think it's better if we don't paint ourselves into a corner around this. I agree. But so what do we do? Already now require that there is no space between @ and the following token when the user wants to use type applications in the pattern? And would we also require the user to add a space after an at-pattern? In which case we should probably start a deprecation cycle for the currently legal foo (a @b) = … Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C549984ffda524c614d6008d6045cf7bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636701194744752293&sdata=i4KtV3B%2B2YUluqn3Rx7th3sm6%2BDYkinoMQE6n%2FNqdZQ%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto: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.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Freitag, den 17.08.2018, 13:00 -0400 schrieb Eric Seidel:

I've always thought of "@Int" as a single syntactic unit, so I'd be happy to disallow spaces between the @ and the type.

not opposed in principle, but if we go that route, it should also apply to type applications in expressions, for consistency. Are we willing to potentially break code out there? (Well, it’s an extension, the fix is simple and fully backward-compatible, and most people probably got it right in the first place, so maybe breaking is not too bad.) Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I think the goal is to preserve the syntactic space for f ((f -> Just x) @ (g -> Just y)) = ... as an "and-pattern" which matches both patterns and binds both x and y. And also perhaps f ((f -> Just x)@(g -> Just y)) = ... by narrowing the situations in which "@" introduces a type argument to just <space>@<type> with white space before, but not after the "@". And do to his in both terms and patterns. Simon | -----Original Message----- | From: ghc-steering-committee On Behalf Of Richard Eisenberg | Sent: 19 August 2018 02:32 | To: Joachim Breitner | Cc: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Discussion about "Type | Application in Patterns" (#126) | | So what's the new rule? Is it: | | - @ denotes a type application if it is preceded by a non-identifier | character and succeeded by a non-whitespace character | - @ denotes an as-pattern if is preceded by an identifier character or | succeeded by a whitespace character | | This means that `f@ Int` is an as-pattern. | | I think the new rule just adds another twist to an already too- | complicated plot. | | I'm not worried about backward-compat issues here (echoing Joachim's | sentiments) but I don't see the advantage to this new spec. | | Richard | | > On Aug 17, 2018, at 1:27 PM, Joachim Breitner wrote: | > | > Hi, | > | > Am Freitag, den 17.08.2018, 13:00 -0400 schrieb Eric Seidel: | >> I've always thought of "@Int" as a single syntactic unit, so I'd be | happy to disallow spaces between the @ and the type. | > | > not opposed in principle, but if we go that route, it should also | > apply to type applications in expressions, for consistency. Are we | > willing to potentially break code out there? (Well, it’s an | > extension, the fix is simple and fully backward-compatible, and most | > people probably got it right in the first place, so maybe breaking is | > not too bad.) | > | > Cheers, | > Joachim | > | > | > -- | > Joachim Breitner | > mail@joachim-breitner.de | > | > | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.jo | > achim- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca3c9 | > | e99884a34ec6670d08d605739f1f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C | > | 0%7C636702391484409758&sdata=mFolm%2BaXnNO%2FMdniUugnuqcotyGViJbtf | > qK%2FKD1VM0I%3D&reserved=0 | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | committ | > ee | | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | committee