Pattern synonym constraints :: Ord a => () => ...

[Anthony Clayden]

Thank you to Richard for the Tweag tutorials on Pattern Synonyms. That
third one on Matchers was heavy going. I didn't find an answer (or did I
miss it?) to something that's bugging me:

>    pattern  SmartConstr :: Ord a => () => ...

Seems to mean:

* Required constraint is Ord a  -- fine, for building
* Provided constraint is Ord a  -- why? for matching/consuming

I'm using `SmartConstr` with some logic inside it to validate/build a
well-behaved data structure. But this is an ordinary H98 datatype, not a
GADT.

I don't want to expose the datatype's underlying constructor, because
client code could break the abstraction/build an ill-formed data structure.

If I pattern-match on `SmartConstr`, the consuming function wants `Ord a`.
But I can't always provide `Ord a`, because this isn't a GADT. And the
client's function could be doing something that doesn't need `Ord a` --
like counting elements, or showing them or streaming to a List, etc.

This feels a lot like one of the things that's wrong with 'stupid theta'
datatype contexts.

My work-round seems to be to define a second `ReadOnlyConstr` without
constraints, that's unidirectional/ can't be used for building.

For definiteness, the use case is a underlying non-GADT constructor for a
BST

>      Node :: Tree a -> a -> Tree a -> Tree a
>
>    pattern SmartNode :: Ord a => () => Tree a -> a -> Tree a -> Tree a

with the usual semantics that the left Tree holds elements less than this
node. Note it's the same `a` with the same `Ord a` 'all the way down' the
Tree.

If some function is consuming the Tree, it can provide constraints for its
own purposes:

>    member   :: Ord a => a -> Tree a -> Bool
>    dumbElem :: Eq a  => a -> Tree a -> Bool
>    max      :: Ord a => Tree a -> a

(That again is the same thinking behind deprecating datatype contexts.)

>    countT (SmartNode l x r) = countT l + 1 + countT r               --
why infer Ord a => ?
>
>    class FancyShow t  where
>      fancyShow :: Show a => Int -> t a -> String
>    instance FancyShow Tree  where
>      fancyShow indent (SmartNode l x r) = ...         -- rejected: Could
not deduce Ord a
>

(Ref the parallel thread on Foldable: client code can't declare an instance
for a Constructor class using SmartConstr.)

I can see commonly your Provided would be at least the constraints inside
the GADT constructor. But why presume I have a GADT?  (And yes I get that a
devlishly smart pattern might be building different GADT constrs/various
constraints, so this is difficult to infer.)

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