Fwiw, a less contrived, and much more relatable, version of Richard's example would be pattern Is3 :: (Num a, Eq a) => a -- only a Required constraint pattern Is3 = 3 -- a polymorphic literal! I think it can be quite instructive for people new to patsyn typing to work out why this is exactly the same as the one in Richard's email! On Thu, Jan 6, 2022, 21:11 Richard Eisenberg wrote:

On Jan 5, 2022, at 9:19 PM, Anthony Clayden wrote:

So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.

In your example, yes: the Required context is "stupid" in the way that "stupid theta" is. The reason to have a Required context is if your pattern synonym does computation that requires a constraint. For example:

pattern Is3 :: (Num a, Eq a) => a -- only a Required constraint pattern Is3 = ((==) 3 -> True) -- that's a view pattern

In your case, there is no computation (your pattern synonym just stands for a constructor), so the Required context is unhelpful (and does indeed act just like a datatype context).

The User Guide https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts... says

- ⟨CProv⟩ are the constraints *made available (provided)* by a successful pattern match.

But it doesn't mean that. It's more like "⟨CProv⟩ are the constraints made available *in addition to ⟨CReq⟩* (provided union required) by a successful pattern match."

I agree with the user guide here: the Provided constraints are made available. The Required constraint must *already* be available before the pattern match, so they are not made available *by* the match. It is true, though, that in the context of the match, both the Provided and the Required constraints must be satisfiable.

To get the pre-1999 behavior, you would need a different type for a pattern synonym used as a pattern than for one used as an expression. This is the subject of the accepted-but-not-implemented https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bi...

Richard

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

[Picking up a cafe thread from February that fits here https://mail.haskell.org/pipermail/haskell-cafe/2021-February/133459.html.] Am 23.02.21 um 20:07 schrieb Richard Eisenberg:

* You might be interested in my recent paper on exactly this problem: *>* how to make DatatypeContexts actually work the way you want: *>* https://richarde.dev/papers/2020/partialdata/partialdata.pdf https://richarde.dev/papers/2020/partialdata/partialdata.pdf *>* <https://richarde.dev/papers/2020/partialdata/partialdata.pdf https://richarde.dev/papers/2020/partialdata/partialdata.pdf>.*

I think that paper is _not_ how DatatypeContexts should work -- at least for the example in that thread of `fmap` over a data structure wanting to preserve some invariant, such as unique elements. - For the matching/Provided constraints the paper at least does no harm by magically unveiling constraints via a Well-Formed-Type mechanism. It would equally do no harm by just not Providing any constraints at all. - For the building/Required constraints: it would do harm to magically unveil (for example) a computation to squish out duplicates or re-order elements by their `fmap`ed result. The Laws for `Functor.fmap` include "preserving the structure of " the Functor. Squishing out duplicates/reordering/rebalancing breaks that. Instead of `fmap` you should use `Foldable.foldMap :: Monoid https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Monoid.html#t:Mo... m => (a -> m) -> t a -> m`; with `m` instance of the form `Ord b => Monoid (t b)` -- `Ord` induced from the Datatype context of `t`. Then there is a mechanism to pass in the `Ord` dictionary from outside/no need for WFT magic. I get it that Required `Ord b` is a poor stand-in for the invariant: no duplicates; elements in ascending sequence; BST balanced. So the Monoid instance still couldn't expose the underlying data constructors. Forcing to use `foldMap` at least puts it in the programmer's face that trying to use `fmap` is a type error standing in for law-breaking. AntC On Fri, 7 Jan 2022 at 15:00, Anthony Clayden wrote:

On Fri, 7 Jan 2022 at 09:08, Richard Eisenberg wrote:

...

On Jan 5, 2022, at 9:19 PM, Anthony Clayden wrote:

So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.

In your example, yes: the Required context is "stupid" in the way that "stupid theta" is. The reason to have a Required context is if your pattern synonym does computation that requires a constraint. ...

I don't think that's the only (or even the chief) reason. Wadler's response on that 1999 thread is telling

"Often, a type will make no sense without the constraints; e.g., an association list type Alist a b makes no sense unless Eq a holds. The class constraints on data declarations were a simple way for the user to ask the compiler to enforce this invariant. They have compile-time effect only, no effect whatsoever on run-time (in particular, no dictionaries should be passed). "