Re: Typing of Pattern Synonyms: Required vs Provided constraints [was cafe DatatypeContexts / alternative]

[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). "