[ghc-steering-committee] Discussion about "Type Application in Patterns" (#126)

[Simon Peyton Jones]

|  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 at 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 <ghc-steering-committee-bounces at haskell.org> On
|  Behalf Of Joachim Breitner
|  Sent: 04 August 2018 16:27
|  To: ghc-steering-committee at 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 at haskell.org
|  > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ
|  > ee
|  --
|  Joachim Breitner
|    mail at 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