Re: Typing of Pattern Synonyms: Required vs Provided constraints

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). " And yet he's somehow forgotten his own design for constraints: the _only_ way to enforce a constraint is by providing evidence in the form of a dictionary. (This is especially impossible for a constructor class where it's the (invisible) argument type to the constructor that wants the constraint.) That's why I agree with SPJ 1999 here: on a pattern match there's no mechanism to pass in a constraint (dictionary-as-evidence); and you're not doing computation in merely matching -- it doesn't even need `Eq`. In a pattern

baz (MkT 3 3) = "Three" -- desugars to baz (MkT x y) | x == fromInteger #3#, y == fromInteger #3# = "Three"

It's the appearance of the `==` and `fromInteger` that Require `(Eq a, Num a)`; I don't expect them Provided by `T`'s nor `MkT`'s Datatype context. And in general, guards can induce arbitrary computation; it's not the responsibility of the datatype declarer to anticipate that. (A Separation of Concerns argument.) So I want constraints 'Required' for building -- that is constraints 'sighted' whether or not any computation involved; but not 'Provided' by matching -- because they're already sighted by the very fact of having built the pattern (to paraphrase SPJ1999). Thanks for pointing out that proposal. I guess it'll achieve what I want for a BST or Wadler's assoc list; would be nice to see an explicit example. I don't want to use a GADT here, because it's the same constraint on every data constructor; and a BST recurses with the same constraint; holding identical dictionaries inside each node is just clutter. Something accessing the BST (probably) needs to bring its `Ord` dictionary with it (`elem` for example); but not necessarily (`count`, `toList` or `show`).

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,

I disagree. To "be available" requires a dictionary. A pattern synonym gets desugarred, it doesn't hold a dictionary itself. The dictionary *was* "already available" at the time of building; but it's no longer available unless the PatSyn got desugarred to a GADT with that dictionary inside. I want these PatSyns desugarred to ordinary H98 data constructors. And I want an empty Provided `:: (Ord a) => () => a -> a -> T a` to mean nothing is Provided, not even what was Required.

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...

AntC