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

[Anthony Clayden]

[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

*>* >.*


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

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).  "
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Typing of Pattern Synonyms: Required vs Provided constraints

[Anthony Clayden]

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.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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Fwd: Typing of Pattern Synonyms: Required vs Provided constraints

[Anthony Clayden]

Thanks Gergö, I do find Richard's tendency to use ViewPattern examples
distracts me from understanding the point. That arrow-to-nowhere or
arrow-to-the-wrong-value syntax is nausea-inducing.

Your "instructive" example is really nothing to do with PatSyns, just
ordinary Haskell numeric patterns: the Language Report (section 3.17.2
point 7., same wording in 2010 and '98) says a numeric literal in a pattern
gets desugared to an `(==)` test against `fromInteger  `. So
that explains where the constraints come from. (Annoyingly, the 
you can't express in legit Haskell source.)

Avoiding distractions is why my o.p. used an `Ord` constraint, also to
follow SPJ's 1999 example. And the canonical example in those old
discussions (like Hughes' 1999 paper) is an `Ord` constraint for elements
of a `Set` structured as a BST.

With your "polymorphic literal" how do I follow the Language Report to
desugar? I'd rather be able to write Richard's example using an as-Pattern
like one of these:

>pattern x@Is3 | x == fromInteger (#3#) = x   -- where #3# is the
inexpressible 
>pattern x@3@Is3 = x

(It's not that I'm "new to patsyn typing"; it's more that patsyn typing and
design keeps falling short of what I hope from such a promising feature. So
I always want to check I'm not mis-understanding. Specifically, the design
for Pattern Synonyms was a lost opportunity to expunge ViewPatterns
entirely.)

AntC

On Fri, 7 Jan 2022 at 09:43, Gergő Érdi  wrote:

> 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:
>
>>
>>
>> ...
>>
>>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Typing of Pattern Synonyms: Required vs Provided constraints

[Gergő Érdi]

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.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, 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-bidir-constr-sigs.rst
>
> Richard
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Typing of Pattern Synonyms: Required vs Provided constraints

[Richard Eisenberg]

> 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.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, 
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-bidir-constr-sigs.rst

Richard

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

Typing of Pattern Synonyms: Required vs Provided constraints

[Anthony Clayden]

There was an interesting exchange between the authors of Haskell compilers
back in 1999 (i.e. when there were multiple compilers)
http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html

I was trying to simulate SPJ's point of view, using PatternSynonyms.

>
>{-#  LANGUAGE DatatypeContexts, PatternSynonyms  #-}
>
>data Ord a => TSPJ a = MkTSPJ a a
>
>pattern PatTSPJ :: (Ord a) => () => a -> a -> TSPJ a-- empty
Provided
>pattern PatTSPJ x y = MkTSPJ x y
>
>unPatTSPJ :: TSPJ a -> (a, a)-- no
constraints
>unPatTSPJ (PatTSPJ x y) = (x, y)
>

`unPatSPJ`'s binding rejected `No instance for (Ord a) arising from a
pattern`. If I don't give a signature, inferred `unPatTSPJ :: Ord b => TSPJ
b -> (b, b)`.

Taking the DatatypeContext off the `data` decl doesn't make a difference.

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

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

Or ... is there some way to simulate the up-to-1999 GHC behaviour? (I
happen to agree with SPJ; Wadler wasn't thinking it through; consider for
example constructor classes over type constructors with constraints:
there's nothing in the instance head for the constraint to attach to. Now
that we have GADTs -- which are appropriate for a different job -- that DT
Contexts perhaps were being (ab-)used for -- I agree more strongly with
SPJ.)

With GADTs I could get a `unGSPJ` that doesn't expose/provide the
constraint, but it does that by packing the constraint/dictionary
(polluting) inside the data constructor. Not  what I want. As SPJ says
down-thread

 "when you take a constructor *apart*, the invariant must hold
by construction: you couldn't have built the thing you are taking
apart unless invariant held.  So enforcing the invariant again is
redundant; and in addition it pollutes the type of selectors."


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