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

[Simon Peyton Jones via Glasgow-haskell-users]

Perhaps I'm just stupid, and should be disqualified from using such features.
Only as a result of this thread (not from the User Guide nor from the paper) do 
I discover "use" means match-on.

You are not stupid.  And since you misunderstood despite effort, the 
presentation is - by definition - not as good as it should be.

The paper focuses pretty much entirely on matching, and takes building for 
granted.  But I can now see that it is not explicit on this point, and that 
leaves it open to misinterpretation.   I think the paper is reasonably careful 
to say "match on" rather than "use", but I wouldn't bet on it.

I suggest the User Guide needs an example where a constraint needed for 
matching (presumably via a View pattern) is not amongst the constraints carried 
inside the data constructor, nor amongst those needed for building. Then the 
limitations in the current design would be more apparent for users.

The user 
manual
 does already speak about the type of a builder, here:

*  For a bidirectional pattern synonym, a use of the pattern synonym as an 
expression has the type

(CReq, CProv) => t1 -> t2 -> ... -> tN -> t

So in the previous example, when used in an expression, ExNumPat has type

ExNumPat :: (Num a, Eq a, Show b) => b -> T t

Notice that this is a tiny bit more restrictive than the expression MkT 42 x 
which would not require (Eq a).
That does seem to directly address the use of a pattern synonym in an 
expression, and means that both CReq and Cprov are required at use sites in 
expressions.   It even includes an example of the sort you wanted.   How could 
we make that clearer?

Thanks

Simon


PS: I am leaving Microsoft at the end of November 2021, at which point 
simo...@microsoft.com will cease to work.  Use 
simon.peytonjo...@gmail.com instead.  (For 
now, it just forwards to simo...@microsoft.com.)

From: Glasgow-haskell-users  On 
Behalf Of Anthony Clayden
Sent: 06 October 2021 06:25
To: Gergő Érdi 
Cc: GHC users 
Subject: Re: Pattern synonym constraints :: Ord a => () => ...


Thanks Gergö, I've read that paper many times (and the User Guide). Nowhere 
does it make the distinction between required-for-building vs 
required-for-matching. And since most of the syntax for PatSyns (the `where` 
equations) is taken up with building, I'd taken it that "required" means 
required-for-building.

There is one paragraph towards the end of section 6 that kinda hints at the 
issue here. It's so cryptic it's no help. "An alternative would be to carry two 
types for each pattern synonym: ...". But already PatSyns carry two sets of 
_constraints_. The matrix type after the constraints is determined by the 
mapping to/from the data constructor. Why would there be two of those? What 
this paragraph might mean (?) is 'carry three sets of constraints', but put one 
set in a completely different signature. As per the proposal.

>  they [Required constraints] are "required" to be able to use the pattern 
> synonym.

Is highly misleading. Only as a result of this thread (not from the User Guide 
nor from the paper) do I discover "use" means match-on. The paper really does 
not address typing for "use" for building. I agree with SPJ's comment (quoted 
in the proposal) "This turns out to be wrong in both directions."

I suggest the User Guide needs an example where a constraint needed for 
matching (presumably via a View pattern) is not amongst the constraints carried 
inside the data constructor, nor amongst those needed for building. Then the 
limitations in the current design would be more apparent for users.

Perhaps I'm just stupid, and should be disqualified from using such features. 
(I keep away from GADTs for those reasons.) So I'm not going to volunteer to 
revise the User Guide further.


On Wed, 6 Oct 2021 at 15:26, Gergő Érdi mailto:ge...@erdi.hu>> 
wrote:
If you haven't yet, it is probably a good idea to read section 6 of
https://gergo.erdi.hu/papers/patsyns/2016-hs-patsyns-ext.pdf

On Wed, Oct 6, 2021 at 10:23 AM Gergő Érdi 
mailto:ge...@erdi.hu>> wrote:
>
> > I'm afraid none of this is apparent from the User Guide -- and I even 
> > contributed some material to the Guide, without ever understanding that. 
> > Before this thread, I took it that 'Required' means for building -- as in 
> > for smart constructors.
>
> No, that's not what the required/provided distinction means at

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

[Anthony Clayden]

On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones 
wrote:

>
>
> I suggest the User Guide needs an example where a constraint needed for
> matching (presumably via a View pattern) is not amongst the
> constraints carried inside the data constructor, nor amongst those needed
> for building. Then the limitations in the current design would be more
> apparent for users.
>
>
>
> The user manual
> 
> does already speak about the type of a builder, here:
>
...
   How could we make that clearer?


This point in that section of the Guide is wrong/misleading:




   - ⟨CReq⟩ are the constraints *required* to match the pattern.

 must be the union of the constraints required to match the pattern,
_plus_ required to build with the pattern -- if it is bidirectional.


Then thank you Simon, but it's the type of the _matcher_ that's
problematic. The only mechanism for getting the constraints needed for
building is by polluting the constraints needed for matching. Here's a
(crude, daft) example, using guards to 'raise' a
required-for-failing-to-build that isn't required-for-successful-building
nor for-matching

>pattern TwoNode :: (Show a, Ord a) => () => a -> a -> Tree a
   -- GHC insists on both constraints as Req'd
>
>pattern TwoNode x y  <- Node Empty x (Leaf y)   where
>  TwoNode x y | x > y = Node Empty x (Leaf y)
>  | otherwise = error (show x ++ " not greater " ++ show y)

To quote you from May 1999

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


`Show a` must have "held by construction" of the `Node`. But the PatSyn's
constraints are requiring more than that was true in some distant line of
code:  it wants *evidence*  in the form of a dictionary at the point of
deconstructing; since the build was successful, I ipso facto don't want to
`show` anything in consuming it. An `instance Foldable Tree` has no
mechanism to pass in any such dictionaries (which'll anyway be redundant,
as you say).
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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

[Simon Peyton Jones via Glasgow-haskell-users]

 must be the union of the constraints required to match the pattern, 
_plus_ required to build with the pattern -- if it is bidirectional.
I think that is confusing too!  How about this:

  *   ⟨CReq⟩ are the constraints required to match the pattern, in a pattern 
match.
  *   ⟨CProv⟩ are the constraints made available (provided) by a successful 
pattern match.
  *and  are both required when P is used as a constructor in 
an expression.
That makes the constructor form explicit.
The only mechanism for getting the constraints needed for building is by 
polluting the constraints needed for matching.
Yes I agree that’s bad. It is acknowledge as such in the paper, and is the 
subject of accepted proposal #42.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point 
simo...@microsoft.com will cease to work.  Use 
simon.peytonjo...@gmail.com instead.  (For 
now, it just forwards to simo...@microsoft.com.)

From: Anthony Clayden 
Sent: 06 October 2021 11:42
To: Simon Peyton Jones 
Cc: Gergő Érdi ; GHC users 
Subject: Re: Pattern synonym constraints :: Ord a => () => ...



On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:

I suggest the User Guide needs an example where a constraint needed for 
matching (presumably via a View pattern) is not amongst the constraints carried 
inside the data constructor, nor amongst those needed for building. Then the 
limitations in the current design would be more apparent for users.

The user 
manual
 does already speak about the type of a builder, here:

...
   How could we make that clearer?

This point in that section of the Guide is wrong/misleading:


· ⟨CReq⟩ are the constraints required to match the pattern.
 must be the union of the constraints required to match the pattern, 
_plus_ required to build with the pattern -- if it is bidirectional.


Then thank you Simon, but it's the type of the _matcher_ that's problematic. 
The only mechanism for getting the constraints needed for building is by 
polluting the constraints needed for matching. Here's a (crude, daft) example, 
using guards to 'raise' a required-for-failing-to-build that isn't 
required-for-successful-building nor for-matching

>pattern TwoNode :: (Show a, Ord a) => () => a -> a -> Tree a 
> -- GHC insists on both constraints as Req'd
>
>pattern TwoNode x y  <- Node Empty x (Leaf y)   where
>  TwoNode x y | x > y = Node Empty x (Leaf y)
>  | otherwise = error (show x ++ " not greater " ++ show y)
To quote you from May 1999


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


`Show a` must have "held by construction" of the `Node`. But the PatSyn's 
constraints are requiring more than that was true in some distant line of code: 
 it wants evidence  in the form of a dictionary at the point of deconstructing; 
since the build was successful, I ipso facto don't want to `show` anything in 
consuming it. An `instance Foldable Tree` has no mechanism to pass in any such 
dictionaries (which'll anyway be redundant, as you say).


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

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

[ÉRDI Gergő]

On Tue, 5 Oct 2021, David Feuer wrote:


To be clear, the proposal to allow different constraints was accepted, but 
integrating
it into the current, incredibly complex, code was well beyond the limited 
abilities of
the one person who made an attempt. Totally severing pattern synonyms from 
constructor
synonyms (giving them separate namespaces) would be a much simpler design.


The backend side of it shouldn't be too difficult -- after all, we are 
already storing a full `Id` (with type and all) for the builder in 
`PatSyn`, it might as well have a completely different type from the 
matcher `Id`. So in GHC/Tc/TyCl/PatSyn.hs, we can just fiddle with 
`mkPatSynBuilder`.


And so we get to the UX side of this, which is the hairy part and the 
reason I'm not too keen on working on this. As you can see in this 
very thread, pattern types are already quite complex for users.

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