Re: Concrete syntax for pattern synonym type signatures
Let me restate the proposals more concretely. Correct me if I'm wrong! Suppose we have the following declarations: data T a b where MkT :: (Eq a, Ord b, Show c) = a - (b, b) - c - T a b pattern P x y = MkT 5 (y, True) x What is the type of P? Simon's proposal: pattern P :: (Eq a, Ord Bool, Show c) = (Num a) = c - Bool - T a Bool Or, more generally: pattern pat :: provided constraints = required constraints = matched args - result type My proposal: pattern P :: (Num a) = (Eq a, Ord Bool, Show c) = c - Bool - T a Bool Or, more generally: pattern pat :: required constraints = provided constraints = matched args - result type The only difference is the order of required vs. provided constraints. My previous comment about bizarre scoping is that the universal variables -- which (in my opinion) go with the required constraints -- scope over both sets of constraints. The existential variables go with the provided constraints and scope over only the provided constraints. So, Simon's ordering means that the scope of the second (lexically) listed constraints have a *smaller* scope than the first listed constraints. With my ordering, the size of the scope increases as you read to the right, as it normally does. On Nov 10, 2014, at 4:07 PM, Simon Peyton Jones simo...@microsoft.com wrote: | Whatever syntax we choose, I would highly recommend putting in a helpful | link to more information in error messages. In principle I like this very much, but I have always stumbled on - writing links that will remain stable for ever (and are hence release-specific) - keeping them up to date when the version changes - making them easy to test e.g. in my build tree Separate question really, but would need some systematic attention to make it work properly in general. Is there a way of pulling the version from DynFlags? If so, it would be easy to include the version number in an SDoc. Then, we could make the link go to the user manual. It would be easy to write a function `userManualLink :: String - SDoc` that takes the last bit of the link and produces a link to the manual for the version at hand. (It wouldn't work for non-released versions, but I'm OK with that.) Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
| I should note that I can say this in 7.8.3: | | foo :: Show a = Eq a = a - String | foo x = show x ++ show (x == x) Yes, that's right. SO using two arrows for pattern synonyms would be an abuse of notation. But (a) the 'pattern' keyword signals that something different is coming up, (b) used in an expression, the type does have the same meaning (i.e. both contexts are required), (c) the alternatives seem worse! Simon | -Original Message- | From: Richard Eisenberg [mailto:e...@cis.upenn.edu] | Sent: 10 November 2014 03:03 | To: Simon Peyton Jones | Cc: Dr. ERDI Gergo; GHC Devs | Subject: Re: Concrete syntax for pattern synonym type signatures | | | On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones simo...@microsoft.com | wrote: | | * One other possibility would be two = thus | pattern P :: (Eq b) = (Num a, Eq a) = ...blha... | | | I should note that I can say this in 7.8.3: | | foo :: Show a = Eq a = a - String | foo x = show x ++ show (x == x) | | Note that I've separated the two constraints with a =, not a comma. | This syntax does what you might expect. (I actually believe that this | is an improvement over the conventional syntax, but that's a story for | another day.) For better or worse, this trick does not work for GADT | constructors (which is a weird incongruence with function type | signatures), so adding the extra arrow does not really steal syntax | from GADT pattern synonyms. | | Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
Note though, it doesn't mean the same thing to say (Foo a, Bar a b) = ... as it does to say Foo a = Bar a b = ... The latter can use Foo a when working on Bar a b, but not Bar a b to discharge Foo a, which makes a difference when you have functional dependencies. So in some sense the 'pattern requires/supplies' split is just that. That said, Richard's other option pattern Foo a = P :: Bar a = a has the benefit that it looks a bit like the old datatype contexts (but here applied to the constructor/pattern). If we expect the left hand side or the right hand side to be most often trivial then that may be worth considering. You'd occasionally have things like pattern (Num a, Eq a) = Foo :: a for pattern Foo = 8 but most of the time they'd wind up just looking like a GADT constructor. -Edward On Sun, Nov 9, 2014 at 10:02 PM, Richard Eisenberg e...@cis.upenn.edu wrote: On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones simo...@microsoft.com wrote: * One other possibility would be two = thus pattern P :: (Eq b) = (Num a, Eq a) = ...blha... I should note that I can say this in 7.8.3: foo :: Show a = Eq a = a - String foo x = show x ++ show (x == x) Note that I've separated the two constraints with a =, not a comma. This syntax does what you might expect. (I actually believe that this is an improvement over the conventional syntax, but that's a story for another day.) For better or worse, this trick does not work for GADT constructors (which is a weird incongruence with function type signatures), so adding the extra arrow does not really steal syntax from GADT pattern synonyms. Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
While I'll admit I still like my bikeshed color choice over Simon's, I'm happy to go with the fact that there seems to be more momentum behind Simon's. Instead, let me propose a slight change of shade: put the required constraints *first* and the provided ones *second*. Of course, we could leave out the required constraints. So, continuing the examples from earlier, we have pattern P :: forall a. Num a = forall c. (Eq a, Ord Bool, Show c) = c - Bool - T a Bool pattern C :: (Eq b, Num b) = () = b - c - X Maybe (Maybe b) Of course, you can drop the `forall`s in `P`'s type. This has, I believe, several advantages over the other order: - If you write the `forall`s in, the scope builds left to right. In the other order, the scoping is very bizarre. - I think of the provided bits + arguments of the constraint as what is matched against. The order I propose keeps these pieces together. Consider a synonym for a GADT constructor, but with some of the arguments filled in. With the order I propose, you can straightforwardly do substitution over the original GADT constructor type, and perhaps prepend some new required constraints. In the other order, the original GADT constructor type must be broken up. Whatever syntax we choose, I would highly recommend putting in a helpful link to more information in error messages. This will remain a tripping point, not because of poor syntax, but because this is tricky. I would love to see us start the habit of putting links to web pages (possibly from the manual) in error messages to give users a place to look when they need more information. Richard On Nov 10, 2014, at 9:09 AM, Dr. ERDI Gergo ge...@erdi.hu wrote: Good news, I've made the necessary parser breakthrough and I've now got pattern P :: pretty much anything after this point to parse as a pattern synonym type signature on a local sub-branch of my branch. So no more annoying 'pattern type' nonsense. As for the 'pretty much anything' part, I have SPJ's original proposal implemented as a proof-of-concept: pattern C :: forall b c. (; Eq b, Num b) = b - c - X Maybe (Maybe b) But I see that the popular opinion now seems to be moving to pattern C :: () = (Eq b, Num b) = b - c - X Maybe (Maybe b) which should be even easier to implement now, so I hope to finish the branch in a couple days (it probably doesn't need more than an evening's work now). Thanks go out to everyone who contributed in this little syntax bikeshedding exercise. Bye, Gergo -- .--= ULLA! =-. \ http://gergo.erdi.hu \ `---= ge...@erdi.hu =---' Define (n.) De ting you get for breaking de law. ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Mon, 10 Nov 2014, Richard Eisenberg wrote: pattern P :: forall a. Num a = forall c. (Eq a, Ord Bool, Show c) = c - Bool - T a Bool pattern C :: (Eq b, Num b) = () = b - c - X Maybe (Maybe b) Of course, you can drop the `forall`s in `P`'s type. This has, I believe, several advantages over the other order: - If you write the `forall`s in, the scope builds left to right. In the other order, the scoping is very bizarre. I am by now convinced that allowing two separate sets of `forall`s is overkill, we don't need the extra specificity. One `forall` with a mixed bag of type variables should be enough. ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
| Instead, let me propose a slight change of shade: put the required | constraints *first* and the provided ones *second*. Of course, we could | leave out the required constraints. I'm agnostic about this choice at the moment, but I don't understand your points. | So, continuing the examples from earlier, we have | | pattern P :: forall a. Num a = forall c. (Eq a, Ord Bool, Show c) = c | - Bool - T a Bool | pattern C :: (Eq b, Num b) = () = b - c - X Maybe (Maybe b) In these examples, can you just remind us of which are match-required and which are match-provided? | - If you write the `forall`s in, the scope builds left to right. In the | other order, the scoping is very bizarre. Can you be more explicit? I don't understand. | - I think of the provided bits + arguments of the constraint as what is | matched against. The order I propose keeps these pieces together. Can you give a concrete example? I don't understand. | Whatever syntax we choose, I would highly recommend putting in a helpful | link to more information in error messages. In principle I like this very much, but I have always stumbled on - writing links that will remain stable for ever (and are hence release-specific) - keeping them up to date when the version changes - making them easy to test e.g. in my build tree Separate question really, but would need some systematic attention to make it work properly in general. Simon ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
Note though, it doesn't mean the same thing to say (Foo a, Bar a b) = ... as it does to say Foo a = Bar a b = ... The latter can use Foo a when working on Bar a b, but not Bar a b to discharge Foo a, which makes a difference when you have functional dependencies. I disagree. Can you offer a concrete example, and show that one typechecks when the other does not? Simon From: Edward Kmett [mailto:ekm...@gmail.com] Sent: 10 November 2014 15:46 To: Richard Eisenberg Cc: Simon Peyton Jones; GHC Devs Subject: Re: Concrete syntax for pattern synonym type signatures Note though, it doesn't mean the same thing to say (Foo a, Bar a b) = ... as it does to say Foo a = Bar a b = ... The latter can use Foo a when working on Bar a b, but not Bar a b to discharge Foo a, which makes a difference when you have functional dependencies. So in some sense the 'pattern requires/supplies' split is just that. That said, Richard's other option pattern Foo a = P :: Bar a = a has the benefit that it looks a bit like the old datatype contexts (but here applied to the constructor/pattern). If we expect the left hand side or the right hand side to be most often trivial then that may be worth considering. You'd occasionally have things like pattern (Num a, Eq a) = Foo :: a for pattern Foo = 8 but most of the time they'd wind up just looking like a GADT constructor. -Edward On Sun, Nov 9, 2014 at 10:02 PM, Richard Eisenberg e...@cis.upenn.edumailto:e...@cis.upenn.edu wrote: On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones simo...@microsoft.commailto:simo...@microsoft.com wrote: * One other possibility would be two = thus pattern P :: (Eq b) = (Num a, Eq a) = ...blha... I should note that I can say this in 7.8.3: foo :: Show a = Eq a = a - String foo x = show x ++ show (x == x) Note that I've separated the two constraints with a =, not a comma. This syntax does what you might expect. (I actually believe that this is an improvement over the conventional syntax, but that's a story for another day.) For better or worse, this trick does not work for GADT constructors (which is a weird incongruence with function type signatures), so adding the extra arrow does not really steal syntax from GADT pattern synonyms. Richard ___ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
Well done! Thanks Gergo. | -Original Message- | From: Dr. ERDI Gergo [mailto:ge...@erdi.hu] | Sent: 10 November 2014 14:09 | To: Simon Peyton Jones | Cc: Richard Eisenberg; GHC Devs | Subject: RE: Concrete syntax for pattern synonym type signatures | | Good news, I've made the necessary parser breakthrough and I've now got | | pattern P :: pretty much anything after this point | | to parse as a pattern synonym type signature on a local sub-branch of my | branch. So no more annoying 'pattern type' nonsense. | | As for the 'pretty much anything' part, I have SPJ's original proposal | implemented as a proof-of-concept: | | pattern C :: forall b c. (; Eq b, Num b) = b - c - X Maybe (Maybe | b) | | But I see that the popular opinion now seems to be moving to | | pattern C :: () = (Eq b, Num b) = b - c - X Maybe (Maybe b) | | which should be even easier to implement now, so I hope to finish the | branch in a couple days (it probably doesn't need more than an evening's | work now). | | Thanks go out to everyone who contributed in this little syntax | bikeshedding exercise. | | Bye, | Gergo | | | -- | |.--= ULLA! =-. | \ http://gergo.erdi.hu \ | `---= ge...@erdi.hu =---' | Define (n.) De ting you get for breaking de law. ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Sun, Nov 9, 2014 at 2:11 PM, Simon Peyton Jones simo...@microsoft.com wrote: On this thread: * I'm strongly of the opinion that pattern signatures should start pattern P :: ...blah... Just like value signatures, the pattern name comes first, then a double colon. This has the benefit that it lets users logically continue exporting 'pattern Foo', which is a very nice syntax. The only downside is that the error message when users forget to turn on pattern synonyms is somewhat more baroque than it can be with the extra keyword shoehorned in, but the keyword is pretty awful looking. * One other possibility would be two = thus pattern P :: (Eq b) = (Num a, Eq a) = ...blha... If you wanted something which had a match-required part but no match-provided part, you'd end up with patter P :: () = (Num a, Eq a) = ...blah... which is a little odd, but perhaps no odder than pattern P :: ( | Num a, Eq a ) = ...blah... The nested (=) version has a certain appeal to it. It already parses. The trick is just in properly interpreting it, but users already interpret (Foo a, Bar b) = .. differently in different contexts, e.g. in class and instance declarations. They can adapt. -Edward | -Original Message- | From: Dr. ERDI Gergo [mailto:ge...@erdi.hu] | Sent: 09 November 2014 07:56 | To: Simon Peyton Jones | Cc: GHC Devs | Subject: RE: Concrete syntax for pattern synonym type signatures | | On Tue, 4 Nov 2014, Simon Peyton Jones wrote: | | pattern P :: forall tvs. (match-provided ; match-required) = tau | | The ; match-required part is optional, and the match-provided part | might be empty. So P1 and P2 would look like this: | | pattern P1 :: forall a. (; Num a) = b - (a,b) | pattern P2 :: forall a. (; Num a, Ord a) = a - a | | Doesn't the ';' look a bit like something that could be incidentially | introduced by some layout-aware syntax rule? Wouldn't, e.g., '|' be more | explicit as a separator? | | example: | | pattern P :: forall tvs. (Eq b | Num a, Eq a) = b - T a ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones simo...@microsoft.com wrote: * One other possibility would be two = thus pattern P :: (Eq b) = (Num a, Eq a) = ...blha... I should note that I can say this in 7.8.3: foo :: Show a = Eq a = a - String foo x = show x ++ show (x == x) Note that I've separated the two constraints with a =, not a comma. This syntax does what you might expect. (I actually believe that this is an improvement over the conventional syntax, but that's a story for another day.) For better or worse, this trick does not work for GADT constructors (which is a weird incongruence with function type signatures), so adding the extra arrow does not really steal syntax from GADT pattern synonyms. Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
Just a small note about parsing: On Tue, 4 Nov 2014, Simon Peyton Jones wrote: The more I think about this, the more I think we'll just have to bite the bullet and adapt the syntax for constraints in pattern types, to distinguish the match-required and match-provided parts. Suppose we let pattern signatures look like this: pattern P :: forall tvs. (match-provided ; match-required) = tau The ; match-required part is optional, and the match-provided part might be empty. So P1 and P2 would look like this: pattern P1 :: forall a. (; Num a) = b - (a,b) pattern P2 :: forall a. (; Num a, Ord a) = a - a Because the match-required part is optional (and relatively rare) the common case looks just like an ordinary data constructor. One thing worth noting is that implementing a parser for this would be far from straightforward, because currently contexts are parsed as types and then fixed up into contexts: -- We parse a context as a btype so that we don't get reduce/reduce -- errors in ctype. The basic problem is that -- (Eq a, Ord a) -- looks so much like a tuple type. We can't tell until we find the = So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ..., Um) into a type, which would then require rejecting everywhere else where we really do mean a type... Sounds painful. Also painful: rewriting the whole context parsing code :/ Richard's suggestion: pattern type forall a. Num a = P :: forall c. (Eq a, Ord Bool, Show c) = c - Bool - T a Bool has the nice property (unlike the current horrible syntax) that the foralls close left-to-right; also, it is very easy to parse :) I'm hoping to see some more suggestions or general comments! Bye, Gergo ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Nov 8, 2014, at 11:23 AM, Dr. ERDI Gergo ge...@erdi.hu wrote: So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ..., Um) into a type, which would then require rejecting everywhere else where we really do mean a type... Sounds painful. Also painful: rewriting the whole context parsing code :/ I actually think this wouldn't be all that hard. The same parse-as-wrong-AST-node-and-then-fix-it-up-later trick happens in plenty of places, patterns (parsed as expressions) being one of the biggest. Harder than my proposal, probably, but I don't think it's terrible. Richard's suggestion: pattern type forall a. Num a = P :: forall c. (Eq a, Ord Bool, Show c) = c - Bool - T a Bool has the nice property (unlike the current horrible syntax) that the foralls close left-to-right; also, it is very easy to parse :) One slight infelicity of my syntax is that the `P` is buried. I should also note that I intended the `forall`s to be optional. The universally-quantified variables would be those that appear in the result type. (I conjecture without proof that the free variables of the required constraints must be a subset of the free variables of the result type. I further conjecture that said proof is easy, but the neurons capable of producing said proof have the night off.) The existentially-quantified variables are the other ones. Given that the `forall`s are optional and that required constraints are likely rare (I agree there), then the P does not get buried often. My syntax has the felicity that, like Simon's, if we make a pattern synonym for a GADT constructor, without any funny business, the pattern type is the same as the GADT type. It also supports a reading that says, for the example P, As long as we have Num a, then P has the type (...), which is a correct reading of the type. Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Sat, 8 Nov 2014, Richard Eisenberg wrote: On Nov 8, 2014, at 11:23 AM, Dr. ERDI Gergo ge...@erdi.hu wrote: So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ..., Um) into a type, which would then require rejecting everywhere else where we really do mean a type... Sounds painful. Also painful: rewriting the whole context parsing code :/ I actually think this wouldn't be all that hard. The same parse-as-wrong-AST-node-and-then-fix-it-up-later trick happens in plenty of places, patterns (parsed as expressions) being one of the biggest. Harder than my proposal, probably, but I don't think it's terrible. Right, but the issue in this case is if we add this artifical constructor to HsType just so we can fix it up into a pair of contexts, this constructor would permeate everything else that has to do with HsTypes; if nothing else, it'd need a `panic foo: HsContextPair` branch for all type-related renamer/typechecker functions. Unless I'm missing some shortcut. I hope I do! Bye, Gergo ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Nov 8, 2014, at 10:42 PM, Dr. ERDI Gergo ge...@erdi.hu wrote: Right, but the issue in this case is if we add this artifical constructor to HsType just so we can fix it up into a pair of contexts, this constructor would permeate everything else that has to do with HsTypes; if nothing else, it'd need a `panic foo: HsContextPair` branch for all type-related renamer/typechecker functions. Unless I'm missing some shortcut. I hope I do! No, you're right that you would have to do this, but this turns out to be the least of your worries -- takes 5 minutes. :) Now, if I could only predict what would be the *most* of your worries, I'd be a much more efficient programmer! Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Sat, 8 Nov 2014, Richard Eisenberg wrote: I should also note that I intended the `forall`s to be optional. Of course, the forall binders are optional in all proposals. ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On 11/04/2014 05:32 AM, Simon Peyton Jones wrote: The ; match-required part is optional, and the match-provided part might be empty. So P1 and P2 would look like this: pattern P1 :: forall a. (; Num a) = b - (a,b) pattern P2 :: forall a. (; Num a, Ord a) = a - a How about marking the match-provided parts with a keyword, as so: pattern P2 :: (match_required Num a, match_required Ord a) = a - a Except with a better keyword. if might do in a pinch: pattern P2 :: forall a. (if Num a, if Ord a) = a - a or pattern needed (pattern being a keyword) or pattern forall pattern P2 :: (pattern needed Num a, pattern needed Ord a) = a - a ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
On Tue, 4 Nov 2014, Simon Peyton Jones wrote: pattern P :: forall tvs. (match-provided ; match-required) = tau The ; match-required part is optional, and the match-provided part might be empty. So P1 and P2 would look like this: pattern P1 :: forall a. (; Num a) = b - (a,b) pattern P2 :: forall a. (; Num a, Ord a) = a - a Doesn't the ';' look a bit like something that could be incidentially introduced by some layout-aware syntax rule? Wouldn't, e.g., '|' be more explicit as a separator? example: pattern P :: forall tvs. (Eq b | Num a, Eq a) = b - T a ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Re: Concrete syntax for pattern synonym type signatures
On Wed, 5 Nov 2014, Edward Kmett wrote: One note on the syntax front, 'pattern type' was mentioned as annoyingly trying to shoehorn the word 'type' in to lean on an existing keyword, even though its about a term level construction rather than a type level one. We do have some perfectly serviceable keywords available to us that indicate a more 'term/pattern' orientation, e.g. 'case' and 'of' come to mind as things that are viable candidates for similar abuse here. careful there, or someone might suggest type of pattern P :: ... :P ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
RE: Concrete syntax for pattern synonym type signatures
Here is one principle: for GADTs, the pattern type signature should look like the GADT data constructor. So if we have data S a where S1 :: p - q - S (p,q) S2 :: ...blah... pattern P x y = S1 x y then surely the signature for P should be P :: p - q - S (p,q) The same goes for constraints in the constructor's type. Thus, using your example: | data T a b where | MkT :: (Eq a, Ord b, Show c) = a - (b, b) - c - T a b If I say pattern P x y z = MkT x y z then the signature for P should be identical to that of MkT. --- It gets a bit more interesting when you have nested patterns that instantiate the type. For example, with the same type T, consider pattern P x y z = MkT (x,y) (False,True) [z] the right signature for P must presumably be P :: (Eq (p,q), Show [r]) = p - q - r - T (p,q) Bool We don't need to distinguish 'r' as existential, any more than we do in the original signature for MkT. Note that we must retain the instantiated but un-simplified constraints (Eq (p,b), Show [r]), because when pattern-matching against P, those are the constraints brought into scope. - The general story, for both data constructors and pattern synonyms, is that if the type is D :: forall abc. (C1, C2...) = blah then the constraints (C1, C2...) are - *required* when using D in an expression, - *provided* (i.e. brought into scope) pattern matching against D. The tricky case comes when the pattern synonym involves some constraints that are *required* during *pattern-matching*. A simple example is pattern P1 x = (8, x) Here we *require* a (Num a) dictionary *both* when using P1 in an expression (to build the value 8), *and* when using P in pattern matching (to build a value 8 to compare with the value being matched). I'll call the constraints that are *required* when matching the match-required constraints. The same happens for view patterns: gr :: Ord a = a - a - Maybe a gr v x | x v = Just v | otherwise = Nothing pattern P2 x = (gr 8 - Just x) Here, (Ord a, Num a) are match-required. (P2 is uni-directional, so we can't use P2 in expressions.) We can't give a signature to P1 like this P1 :: forall a. Num a = b - (a,b) because that looks as if (Num a) would be *provided* when pattern matching (see general story above), whereas actually it is required. This is the nub of the problem Gergo is presenting us with. Notice that P1 is bidirectional, and can be used in expressions, where again we *require* (Num a), so P1's term type really is something like (Num a) = b - (a,b). The more I think about this, the more I think we'll just have to bite the bullet and adapt the syntax for constraints in pattern types, to distinguish the match-required and match-provided parts. Suppose we let pattern signatures look like this: pattern P :: forall tvs. (match-provided ; match-required) = tau The ; match-required part is optional, and the match-provided part might be empty. So P1 and P2 would look like this: pattern P1 :: forall a. (; Num a) = b - (a,b) pattern P2 :: forall a. (; Num a, Ord a) = a - a Because the match-required part is optional (and relatively rare) the common case looks just like an ordinary data constructor. None of this addresses the bidirectional/unidirectional question, but that's a pretty separate matter. Simon | -Original Message- | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Dr. | ERDI Gergo | Sent: 03 November 2014 10:13 | To: GHC Devs | Subject: RFC: Concrete syntax for pattern synonym type signatures | | Background | -- | | As explained on | https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Staticsemantics | the type of a pattern synonym can be fully described with the | following pieces of information: | | * If the pattern synonym is bidirectional | * Universially-bound type variables, and required constraints on them | * The type of the pattern itself, closed over the universially-bound | type variables | * Existentially-bound type variables, and the constraints provided by | them | * The types of the arguments, closed over the universially and | existentially bound type variables | | Here's an example showing all of these axes in action: | | data T a b where | MkT :: (Eq a, Ord b, Show c) = a - (b, b) - c - T a b | | pattern P x y = MkT 5 (y, True) x | | In this case: | | * The name of the pattern synonym is `P` | * The pattern synonym is bidirectional | * The universially-bound tyvars/required constraints are `forall a. | Num a` | * The type of the pattern is `T a Bool` | * The existentially-bound tyvars/provided constraints are | `forall c. (Eq a, Ord Bool, Show c)` | * The type of the arguments are `c` and `Bool`. | | The problem, then, is finding a concrete syntax that captures
Re: Concrete syntax for pattern synonym type signatures
One note on the syntax front, 'pattern type' was mentioned as annoyingly trying to shoehorn the word 'type' in to lean on an existing keyword, even though its about a term level construction rather than a type level one. We do have some perfectly serviceable keywords available to us that indicate a more 'term/pattern' orientation, e.g. 'case' and 'of' come to mind as things that are viable candidates for similar abuse here. I'm just digging through the lexical lego bin for parts. I don't quite know how to put them together to make a nice syntax though. -Edward On Tue, Nov 4, 2014 at 5:32 AM, Simon Peyton Jones simo...@microsoft.com wrote: Here is one principle: for GADTs, the pattern type signature should look like the GADT data constructor. So if we have data S a where S1 :: p - q - S (p,q) S2 :: ...blah... pattern P x y = S1 x y then surely the signature for P should be P :: p - q - S (p,q) The same goes for constraints in the constructor's type. Thus, using your example: | data T a b where | MkT :: (Eq a, Ord b, Show c) = a - (b, b) - c - T a b If I say pattern P x y z = MkT x y z then the signature for P should be identical to that of MkT. --- It gets a bit more interesting when you have nested patterns that instantiate the type. For example, with the same type T, consider pattern P x y z = MkT (x,y) (False,True) [z] the right signature for P must presumably be P :: (Eq (p,q), Show [r]) = p - q - r - T (p,q) Bool We don't need to distinguish 'r' as existential, any more than we do in the original signature for MkT. Note that we must retain the instantiated but un-simplified constraints (Eq (p,b), Show [r]), because when pattern-matching against P, those are the constraints brought into scope. - The general story, for both data constructors and pattern synonyms, is that if the type is D :: forall abc. (C1, C2...) = blah then the constraints (C1, C2...) are - *required* when using D in an expression, - *provided* (i.e. brought into scope) pattern matching against D. The tricky case comes when the pattern synonym involves some constraints that are *required* during *pattern-matching*. A simple example is pattern P1 x = (8, x) Here we *require* a (Num a) dictionary *both* when using P1 in an expression (to build the value 8), *and* when using P in pattern matching (to build a value 8 to compare with the value being matched). I'll call the constraints that are *required* when matching the match-required constraints. The same happens for view patterns: gr :: Ord a = a - a - Maybe a gr v x | x v = Just v | otherwise = Nothing pattern P2 x = (gr 8 - Just x) Here, (Ord a, Num a) are match-required. (P2 is uni-directional, so we can't use P2 in expressions.) We can't give a signature to P1 like this P1 :: forall a. Num a = b - (a,b) because that looks as if (Num a) would be *provided* when pattern matching (see general story above), whereas actually it is required. This is the nub of the problem Gergo is presenting us with. Notice that P1 is bidirectional, and can be used in expressions, where again we *require* (Num a), so P1's term type really is something like (Num a) = b - (a,b). The more I think about this, the more I think we'll just have to bite the bullet and adapt the syntax for constraints in pattern types, to distinguish the match-required and match-provided parts. Suppose we let pattern signatures look like this: pattern P :: forall tvs. (match-provided ; match-required) = tau The ; match-required part is optional, and the match-provided part might be empty. So P1 and P2 would look like this: pattern P1 :: forall a. (; Num a) = b - (a,b) pattern P2 :: forall a. (; Num a, Ord a) = a - a Because the match-required part is optional (and relatively rare) the common case looks just like an ordinary data constructor. None of this addresses the bidirectional/unidirectional question, but that's a pretty separate matter. Simon | -Original Message- | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Dr. | ERDI Gergo | Sent: 03 November 2014 10:13 | To: GHC Devs | Subject: RFC: Concrete syntax for pattern synonym type signatures | | Background | -- | | As explained on | https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Staticsemantics | the type of a pattern synonym can be fully described with the | following pieces of information: | | * If the pattern synonym is bidirectional | * Universially-bound type variables, and required constraints on them | * The type of the pattern itself, closed over the universially-bound | type variables | * Existentially-bound type variables, and the constraints provided by | them | * The types of the arguments, closed over the
