Concrete syntax for pattern synonym type signatures

[Richard Eisenberg]

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