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 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-bounces@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 all of | this information. This syntax is needed for at least two purposes: | | * Showing pattern synonym type information in Haddock/GHCi | * Pattern synonym type signatures (#8584) | | Current state of things | ----------------------- | | GHCi 7.8.3 shows the type above as: | | pattern (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t Bool) | | Not only does it not show directionality, I think this is very | confusing in every other way as well, especially with explicit | foralls: | | pattern forall c. (Eq t, Ord Bool, Show c) => P c Bool :: forall t. | Num t => (T t Bool) | | I am currently working on implementing #8584, which means I need to | parse these type signatures. I managed to get the above monstrosity to | parse (unambigiously from actual pattern synonym definitions) by | throwing in an extra 'type' keyword: | | pattern type (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t | Bool) | | Request for help | ---------------- | | Surely we can do better than that! So let's come up with a nice syntax | for pattern synonym type signatures. It will be used in the pattern | synonym type signature annotations of GHC 7.10, and we could also | retrofit it into GHC 7.8.4 and its Haddock, so that documentation | generated with today's tools will look consistent with code you will | be able to enter in tomorrow's version. | | Bye, | Gergo | _______________________________________________ | 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

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

On Sat, 8 Nov 2014, Richard Eisenberg wrote:

On Nov 8, 2014, at 11:23 AM, "Dr. ERDI Gergo" 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

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.

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

On Sun, Nov 9, 2014 at 2:11 PM, Simon Peyton Jones 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:gergo@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

| 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:eir@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 | 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

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" 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 \ `---= gergo@erdi.hu =-------' Define (n.) De ting you get for breaking de law.

| 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

| My proposal: | | > pattern P :: (Num a) => (Eq a, Ord Bool, Show c) => c -> Bool -> T a | > Bool | | 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. I _think_ you mean that you _could_ write P's type like this: | > pattern P :: forall a. (Num a) => forall c. (Eq a, Ord Bool, Show c) => c -> Bool -> T a I'm not sure we really would give it that nested structure, but it would be reasonable to do so. Richard's point is that the match-required constraints can *only* mention the universally quantified type variables. So yes, I think Richard is probably right. Incidentally ote that pattern P x = (3,x) would have type pattern P :: Num a => () => b -> (a,b) But since the "match-provided but no match-required" case must look simple, the "match-required but no match-provided" case is bound to look odd. OK, Gergo, I think you are good to go now. Simon | On Nov 10, 2014, at 4:07 PM, Simon Peyton Jones | 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

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

On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones 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

Lamely, I can't seem to reconstruct the problem. GHC seems to be more careful about gathering the constraints up into a tuple even when I give an explicit type signature involving nested contexts nowadays. -Edward On Mon, Nov 10, 2014 at 4:07 PM, Simon Peyton Jones wrote:

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:ekmett@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 wrote:

On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones 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