Typing of Pattern Synonyms: Required vs Provided constraints

[Anthony Clayden]

On Fri, 7 Jan 2022 at 09:08, Richard Eisenberg <lists at richarde.dev> wrote:

>
>
> On Jan 5, 2022, at 9:19 PM, Anthony Clayden <anthony.d.clayden at gmail.com>
> 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.html#typing-of-pattern-synonyms
>  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-bidir-constr-sigs.rst
>
>
>


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20220107/59d4c9cd/attachment.html>