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

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<mailto:simo...@microsoft.com> will cease to work.  Use 
simon.peytonjo...@gmail.com<mailto: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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fghc.gitlab.haskell.org%2Fghc%2Fdoc%2Fusers_guide%2Fexts%2Fpattern_synonyms.html%3Fhighlight%3Dpattern%2520syn%23typing-of-pattern-synonyms=04%7C01%7Csimonpj%40microsoft.com%7C941ec01fb46743eefb4d08d988b5e64a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637691137569565464%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000=B7ZHX1fB5hRZkVuvId1OhnC6j5oYoqeSaD2hByBAPRM%3D=0>
 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 => () => ...

[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]

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<https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html?highlight=pattern%20syn#typing-of-pattern-synonyms>
 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<mailto:simo...@microsoft.com> will cease to work.  Use 
simon.peytonjo...@gmail.com<mailto: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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgergo.erdi.hu%2Fpapers%2Fpatsyns%2F2016-hs-patsyns-ext.pdf=04%7C01%7Csimonpj%40microsoft.com%7Cf208f3e0240646a9829f08d98889d751%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637690948080937568%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000=YhqSQ%2BWSfz5Ycmt8aynh9jJaUVNiiK3kkPrLj1pILx4%3D=0>

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

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

[Anthony Clayden]

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  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  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 all!
> >
> > You should think of both Provided and Required in the context of
> > matching, not in the context of building. To be able to use a pattern
> > synonym to match on a scrutinee of type T, not only does T have to
> > match the scrutinee type of the pattern synonym, but you also must
> > satisfy the constraints of the Required constraints -- they are
> > "required" to be able to use the pattern synonym. On the flipside,
> > once you do use the pattern synonym, on the right-hand side of your
> > matched clause you now get to assume the Provided constraints -- in
> > other words, those constraints are "provided" to you by the pattern
> > synonym.
> >
> > It is true that the builder could have entirely unrelated constraints
> > to either (as in the proposal). The current implementation basically
> > assumes that the Provided constraints can be provided because the
> > builder put them in.
> >
> > Does this make it clearer?
> >
> > On Wed, Oct 6, 2021 at 10:13 AM Anthony Clayden
> >  wrote:
> > >
> > >
> > > Thank you. Yes that proposal seems in 'the same ball park'. As
> Richard's already noted, a H98 data constructor can't _Provide_ any
> constraints, because it has no dictionaries wrapped up inside. But I'm not
> asking it to!
> > >
> > > The current PatSyn signatures don't distinguish between
> Required-for-building vs Required-for-matching (i.e.
> deconstructing/reformatting to the PatSyn). This seems no better than
> 'stupid theta': I'm not asking for any reformatting to pattern-match, just
> give me the darn components, they are what they are where they are.
> > >
> > > 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. So PatSyns aren't really aimed to be for smart
> constructors? I should take that material out of the User Guide?
> > >
> > >
> > > AntC
> > >
> > >
> > > On Wed, 6 Oct 2021 at 10:53, Richard Eisenberg 
> wrote:
> > >>
> > >> You're right -- my apologies. Here is the accepted proposal:
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst
> > >>
> > >> Richard
> > >>
> > >> On Oct 5, 2021, at 12:38 PM, 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.
> > >>
> > >> On Tue, Oct 5, 2021, 

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

[Gergő Érdi]

> 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 all!

You should think of both Provided and Required in the context of
matching, not in the context of building. To be able to use a pattern
synonym to match on a scrutinee of type T, not only does T have to
match the scrutinee type of the pattern synonym, but you also must
satisfy the constraints of the Required constraints -- they are
"required" to be able to use the pattern synonym. On the flipside,
once you do use the pattern synonym, on the right-hand side of your
matched clause you now get to assume the Provided constraints -- in
other words, those constraints are "provided" to you by the pattern
synonym.

It is true that the builder could have entirely unrelated constraints
to either (as in the proposal). The current implementation basically
assumes that the Provided constraints can be provided because the
builder put them in.

Does this make it clearer?

On Wed, Oct 6, 2021 at 10:13 AM Anthony Clayden
 wrote:
>
>
> Thank you. Yes that proposal seems in 'the same ball park'. As Richard's 
> already noted, a H98 data constructor can't _Provide_ any constraints, 
> because it has no dictionaries wrapped up inside. But I'm not asking it to!
>
> The current PatSyn signatures don't distinguish between Required-for-building 
> vs Required-for-matching (i.e. deconstructing/reformatting to the PatSyn). 
> This seems no better than 'stupid theta': I'm not asking for any reformatting 
> to pattern-match, just give me the darn components, they are what they are 
> where they are.
>
> 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. So PatSyns aren't really aimed to be for smart 
> constructors? I should take that material out of the User Guide?
>
>
> AntC
>
>
> On Wed, 6 Oct 2021 at 10:53, Richard Eisenberg  wrote:
>>
>> You're right -- my apologies. Here is the accepted proposal: 
>> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst
>>
>> Richard
>>
>> On Oct 5, 2021, at 12:38 PM, 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.
>>
>> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg  wrote:
>>>
>>>
>>>
>>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden  
>>> wrote:
>>>
>>> >pattern  SmartConstr :: Ord a => () => ...
>>>
>>> Seems to mean:
>>>
>>> * Required constraint is Ord a  -- fine, for building
>>>
>>>
>>> Yes.
>>>
>>> * Provided constraint is Ord a  -- why? for matching/consuming
>>>
>>>
>>> No. Your signature specified that there are no provided constraints: that's 
>>> your ().
>>>
>>>
>>> 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 believe there is no way to have provided constraints in Haskell98. You 
>>> would need either GADTs or higher-rank types.
>>>
>>>
>>> This feels a lot like one of the things that's wrong with 'stupid theta' 
>>> datatype contexts.
>>>
>>>
>>> You're onto something here. Required constraints are very much like the 
>>> stupid theta datatype contexts. But, unlike the stupid thetas, required 
>>> constraints are sometimes useful: they might be needed in order to, say, 
>>> call a function in a view pattern.
>>>
>>> For example:
>>>
>>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>>> checkLT5AndReturn x = (x < 5, x)
>>>
>>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>>>
>>>
>>> My view pattern requires (Ord a, Num a), and so I must declare these as 
>>> required constraints in the pattern synonym type. Because vanilla data 
>>> constructors never do computation, any required constraints for data 
>>> constructors are always useless.
>>>
>>>
>>> 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.
>>>
>>>
>>> Does SmartNode need Ord a to match? Or just to produce a 

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

[Gergő Érdi]

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  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 all!
>
> You should think of both Provided and Required in the context of
> matching, not in the context of building. To be able to use a pattern
> synonym to match on a scrutinee of type T, not only does T have to
> match the scrutinee type of the pattern synonym, but you also must
> satisfy the constraints of the Required constraints -- they are
> "required" to be able to use the pattern synonym. On the flipside,
> once you do use the pattern synonym, on the right-hand side of your
> matched clause you now get to assume the Provided constraints -- in
> other words, those constraints are "provided" to you by the pattern
> synonym.
>
> It is true that the builder could have entirely unrelated constraints
> to either (as in the proposal). The current implementation basically
> assumes that the Provided constraints can be provided because the
> builder put them in.
>
> Does this make it clearer?
>
> On Wed, Oct 6, 2021 at 10:13 AM Anthony Clayden
>  wrote:
> >
> >
> > Thank you. Yes that proposal seems in 'the same ball park'. As Richard's 
> > already noted, a H98 data constructor can't _Provide_ any constraints, 
> > because it has no dictionaries wrapped up inside. But I'm not asking it to!
> >
> > The current PatSyn signatures don't distinguish between 
> > Required-for-building vs Required-for-matching (i.e. 
> > deconstructing/reformatting to the PatSyn). This seems no better than 
> > 'stupid theta': I'm not asking for any reformatting to pattern-match, just 
> > give me the darn components, they are what they are where they are.
> >
> > 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. So PatSyns aren't really aimed to be for smart 
> > constructors? I should take that material out of the User Guide?
> >
> >
> > AntC
> >
> >
> > On Wed, 6 Oct 2021 at 10:53, Richard Eisenberg  wrote:
> >>
> >> You're right -- my apologies. Here is the accepted proposal: 
> >> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst
> >>
> >> Richard
> >>
> >> On Oct 5, 2021, at 12:38 PM, 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.
> >>
> >> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg  wrote:
> >>>
> >>>
> >>>
> >>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden  
> >>> wrote:
> >>>
> >>> >pattern  SmartConstr :: Ord a => () => ...
> >>>
> >>> Seems to mean:
> >>>
> >>> * Required constraint is Ord a  -- fine, for building
> >>>
> >>>
> >>> Yes.
> >>>
> >>> * Provided constraint is Ord a  -- why? for matching/consuming
> >>>
> >>>
> >>> No. Your signature specified that there are no provided constraints: 
> >>> that's your ().
> >>>
> >>>
> >>> 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 believe there is no way to have provided constraints in Haskell98. You 
> >>> would need either GADTs or higher-rank types.
> >>>
> >>>
> >>> This feels a lot like one of the things that's wrong with 'stupid theta' 
> >>> datatype contexts.
> >>>
> >>>
> >>> You're onto something here. Required constraints are very much like the 
> >>> stupid theta datatype contexts. But, unlike the stupid thetas, required 
> >>> constraints are sometimes useful: they might be needed in order to, say, 
> >>> call a function in a view pattern.
> >>>
> >>> For example:
> >>>
> >>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
> >>> checkLT5AndReturn x = (x < 5, x)
> >>>
> >>> pattern LessThan5 :: (Ord a, Num a) => a -> a
> >>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
> >>>
> >>>
> >>> My view pattern requires (Ord a, Num a), and so I must declare these as 
> >>> required constraints in the pattern synonym type. Because vanilla data 
> >>> constructors never do computation, any required constraints for data 
> >>> constructors are always useless.
> >>>
> >>>
> >>> For definiteness, the use case is a 

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

[Anthony Clayden]

Thank you. Yes that proposal seems in 'the same ball park'. As Richard's
already noted, a H98 data constructor can't _Provide_ any constraints,
because it has no dictionaries wrapped up inside. But I'm not asking it to!

The current PatSyn signatures don't distinguish between
Required-for-building vs Required-for-matching (i.e.
deconstructing/reformatting to the PatSyn). This seems no better than
'stupid theta': I'm not asking for any reformatting to pattern-match, just
give me the darn components, they are what they are where they are.

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. So PatSyns aren't really aimed to be for smart
constructors? I should take that material out of the User Guide?


AntC


On Wed, 6 Oct 2021 at 10:53, Richard Eisenberg  wrote:

> You're right -- my apologies. Here is the accepted proposal:
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst
>
> Richard
>
> On Oct 5, 2021, at 12:38 PM, 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.
>
> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg 
> wrote:
>
>>
>>
>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
>> wrote:
>>
>> >pattern  SmartConstr :: Ord a => () => ...
>>
>> Seems to mean:
>>
>> * Required constraint is Ord a  -- fine, for building
>>
>>
>> Yes.
>>
>> * Provided constraint is Ord a  -- why? for matching/consuming
>>
>>
>> No. Your signature specified that there are no provided constraints:
>> that's your ().
>>
>>
>> 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 believe there is no way to have provided constraints in Haskell98. You
>> would need either GADTs or higher-rank types.
>>
>>
>> This feels a lot like one of the things that's wrong with 'stupid theta'
>> datatype contexts.
>>
>>
>> You're onto something here. Required constraints are very much like the
>> stupid theta datatype contexts. But, unlike the stupid thetas, required
>> constraints are sometimes useful: they might be needed in order to, say,
>> call a function in a view pattern.
>>
>> For example:
>>
>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>> checkLT5AndReturn x = (x < 5, x)
>>
>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>>
>>
>> My view pattern requires (Ord a, Num a), and so I must declare these as
>> required constraints in the pattern synonym type. Because vanilla data
>> constructors never do computation, any required constraints for data
>> constructors are always useless.
>>
>>
>> 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.
>>
>>
>> Does SmartNode need Ord a to match? Or just to produce a node? It seems
>> that Ord a is used only for production, not for matching. This suggests
>> that you want a separate smartNode function (not a pattern synonym) and to
>> have no constraints on the pattern synonym, which can be unidirectional
>> (that is, work only as a pattern, not as an expression).
>>
>> It has been mooted to allow pattern synonyms to have two types: one when
>> used as a pattern and a different one when used as an expression. That
>> might work for you here: you want SmartNode to have no constraints as a
>> pattern, but an Ord a constraint as an expression. At the time, the design
>> with two types was considered too complicated and abandoned.
>>
>> Does this help?
>>
>> 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: Pattern synonym constraints :: Ord a => () => ...

[Anthony Clayden]

Thank you Richard (and for the reply to a similar topic on the cafe).

What I meant by the comparison to 'stupid theta' is that GHC's
implementation of datatype contexts used to be mildly useful and moderately
sensible. Then it went stupid, following this 'Contexts on datatype
declarations' thread:
http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062

With the benefit of a great deal of hindsight, and noting that
PatternSynonyms makes explicit there's a builder vs a matcher, I'd say SPJ
was right and Wadler was wrong.

In particular consider trying to implement a Foldable instance (or for any
constructor class): the instance head doesn't reveal the 'content type'
`a`, so there's no way to provide `Ord a`. _But we don't need_ `Ord a`,
because the fold is consuming the content, not building a Foldable
structure. As SPJ says:

> *pattern-matching* on MkT as *eliminating* a constraint. But since the
dictionary isn't stored in the constructor we can't eliminate it.

So at first sight, I was hoping that a PatternSyn

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

would give the pre-May 1999 GHC behaviour for matching -- that is, Provide
nothing, and therefore ask for nothing if the constructor/PatSyn appears
only in a matcher position.

I'm afraid that I don't get your answer wrt PatternSyns that wrap H98
datatypes: how do I demonstrate a difference between the above sig vs:

>pattern SmartConstr :: Ord a => Ord a => blah

It seems to me the shorthand form (with a single `=>`) should be equiv to
the latter, allowing the former nothing-Provided `Ord a => () => blah` to
mean something different.

You say "the design was too complicated". And yet SPJ on that thread says "This
is the simpler choice".

>  you want a separate smartNode function (not a pattern synonym)

I might as well have a SmartNode PatSyn and (unidirectional)
MatcherOnlyNode PatSyn -- which was my work-round in the O.P. Can't you see
that's dysergonomic?

AntC

On Wed, 6 Oct 2021 at 05:32, Richard Eisenberg  wrote:

>
>
> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
> wrote:
>
> >pattern  SmartConstr :: Ord a => () => ...
>
> Seems to mean:
>
> * Required constraint is Ord a  -- fine, for building
>
>
> Yes.
>
> * Provided constraint is Ord a  -- why? for matching/consuming
>
>
> No. Your signature specified that there are no provided constraints:
> that's your ().
>
>
> 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 believe there is no way to have provided constraints in Haskell98. You
> would need either GADTs or higher-rank types.
>
>
> This feels a lot like one of the things that's wrong with 'stupid theta'
> datatype contexts.
>
>
> You're onto something here. Required constraints are very much like the
> stupid theta datatype contexts. But, unlike the stupid thetas, required
> constraints are sometimes useful: they might be needed in order to, say,
> call a function in a view pattern.
>
> For example:
>
> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
> checkLT5AndReturn x = (x < 5, x)
>
> pattern LessThan5 :: (Ord a, Num a) => a -> a
> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>
>
> My view pattern requires (Ord a, Num a), and so I must declare these as
> required constraints in the pattern synonym type. Because vanilla data
> constructors never do computation, any required constraints for data
> constructors are always useless.
>
>
> 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.
>
>
> Does SmartNode need Ord a to match? Or just to produce a node? It seems
> that Ord a is used only for production, not for matching. This suggests
> that you want a separate smartNode function (not a pattern synonym) and to
> have no constraints on the pattern synonym, which can be unidirectional
> (that is, work only as a pattern, not as an expression).
>
> It has been mooted to allow pattern synonyms to have two types: one when
> used as a pattern and a different one when used as an expression. That
> might work for you here: you want SmartNode to have no constraints as a
> pattern, but an Ord a constraint as an expression. At the time, the design
> with two types was considered too complicated and abandoned.
>
> Does this help?
>
> Richard
>
___
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 => () => ...

[Richard Eisenberg]

You're right -- my apologies. Here is the accepted proposal: 
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst

Richard

> On Oct 5, 2021, at 12:38 PM, 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.
> 
> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg  > wrote:
> 
> 
>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden > > wrote:
>> 
>> >pattern  SmartConstr :: Ord a => () => ...
>> 
>> Seems to mean:
>> 
>> * Required constraint is Ord a  -- fine, for building
> 
> Yes.
> 
>> * Provided constraint is Ord a  -- why? for matching/consuming
> 
> No. Your signature specified that there are no provided constraints: that's 
> your ().
> 
>> 
>> 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 believe there is no way to have provided constraints in Haskell98. You 
> would need either GADTs or higher-rank types.
> 
>> 
>> This feels a lot like one of the things that's wrong with 'stupid theta' 
>> datatype contexts.
> 
> You're onto something here. Required constraints are very much like the 
> stupid theta datatype contexts. But, unlike the stupid thetas, required 
> constraints are sometimes useful: they might be needed in order to, say, call 
> a function in a view pattern.
> 
> For example:
> 
>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>> checkLT5AndReturn x = (x < 5, x)
>> 
>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
> 
> My view pattern requires (Ord a, Num a), and so I must declare these as 
> required constraints in the pattern synonym type. Because vanilla data 
> constructors never do computation, any required constraints for data 
> constructors are always useless.
> 
>> 
>> 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.
> 
> Does SmartNode need Ord a to match? Or just to produce a node? It seems that 
> Ord a is used only for production, not for matching. This suggests that you 
> want a separate smartNode function (not a pattern synonym) and to have no 
> constraints on the pattern synonym, which can be unidirectional (that is, 
> work only as a pattern, not as an expression).
> 
> It has been mooted to allow pattern synonyms to have two types: one when used 
> as a pattern and a different one when used as an expression. That might work 
> for you here: you want SmartNode to have no constraints as a pattern, but an 
> Ord a constraint as an expression. At the time, the design with two types was 
> considered too complicated and abandoned.
> 
> Does this help?
> 
> 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: Pattern synonym constraints :: Ord a => () => ...

[David Feuer]

I meant my own brief attempt. Severing them absolutely wouldn't make them
less useful.

pattern Foo :: ...
pattern Foo x <- 

constructor Foo :: ...
constructor Foo x = ...

Separate namespaces, so you can have both, and both can be bundled with a
type.

On Tue, Oct 5, 2021, 1:11 PM Edward Kmett  wrote:

>
>
> On Tue, Oct 5, 2021 at 12:39 PM 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.
>>
>
> It might be simpler in some ways, despite needing yet another syntactic
> marker, etc. but also would make them a lot less useful for a lot of places
> where they are used today, e.g. to provide backwards compatibility for old
> constructors as an API changes, and the like.
>
> Before I left MIRI, Cale had started work on these for us. Is that the
> work you are thinking of, or are you thinking of an earlier effort?
>
> -Edward
>
>
>
>
>> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg 
>> wrote:
>>
>>>
>>>
>>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
>>> wrote:
>>>
>>> >pattern  SmartConstr :: Ord a => () => ...
>>>
>>> Seems to mean:
>>>
>>> * Required constraint is Ord a  -- fine, for building
>>>
>>>
>>> Yes.
>>>
>>> * Provided constraint is Ord a  -- why? for matching/consuming
>>>
>>>
>>> No. Your signature specified that there are no provided constraints:
>>> that's your ().
>>>
>>>
>>> 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 believe there is no way to have provided constraints in Haskell98. You
>>> would need either GADTs or higher-rank types.
>>>
>>>
>>> This feels a lot like one of the things that's wrong with 'stupid theta'
>>> datatype contexts.
>>>
>>>
>>> You're onto something here. Required constraints are very much like the
>>> stupid theta datatype contexts. But, unlike the stupid thetas, required
>>> constraints are sometimes useful: they might be needed in order to, say,
>>> call a function in a view pattern.
>>>
>>> For example:
>>>
>>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>>> checkLT5AndReturn x = (x < 5, x)
>>>
>>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>>>
>>>
>>> My view pattern requires (Ord a, Num a), and so I must declare these as
>>> required constraints in the pattern synonym type. Because vanilla data
>>> constructors never do computation, any required constraints for data
>>> constructors are always useless.
>>>
>>>
>>> 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.
>>>
>>>
>>> Does SmartNode need Ord a to match? Or just to produce a node? It seems
>>> that Ord a is used only for production, not for matching. This suggests
>>> that you want a separate smartNode function (not a pattern synonym) and to
>>> have no constraints on the pattern synonym, which can be unidirectional
>>> (that is, work only as a pattern, not as an expression).
>>>
>>> It has been mooted to allow pattern synonyms to have two types: one when
>>> used as a pattern and a different one when used as an expression. That
>>> might work for you here: you want SmartNode to have no constraints as a
>>> pattern, but an Ord a constraint as an expression. At the time, the design
>>> with two types was considered too complicated and abandoned.
>>>
>>> Does this help?
>>>
>>> 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
>>
>
___
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 => () => ...

[Edward Kmett]

On Tue, Oct 5, 2021 at 12:39 PM 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.
>

It might be simpler in some ways, despite needing yet another syntactic
marker, etc. but also would make them a lot less useful for a lot of places
where they are used today, e.g. to provide backwards compatibility for old
constructors as an API changes, and the like.

Before I left MIRI, Cale had started work on these for us. Is that the work
you are thinking of, or are you thinking of an earlier effort?

-Edward




> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg 
> wrote:
>
>>
>>
>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
>> wrote:
>>
>> >pattern  SmartConstr :: Ord a => () => ...
>>
>> Seems to mean:
>>
>> * Required constraint is Ord a  -- fine, for building
>>
>>
>> Yes.
>>
>> * Provided constraint is Ord a  -- why? for matching/consuming
>>
>>
>> No. Your signature specified that there are no provided constraints:
>> that's your ().
>>
>>
>> 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 believe there is no way to have provided constraints in Haskell98. You
>> would need either GADTs or higher-rank types.
>>
>>
>> This feels a lot like one of the things that's wrong with 'stupid theta'
>> datatype contexts.
>>
>>
>> You're onto something here. Required constraints are very much like the
>> stupid theta datatype contexts. But, unlike the stupid thetas, required
>> constraints are sometimes useful: they might be needed in order to, say,
>> call a function in a view pattern.
>>
>> For example:
>>
>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>> checkLT5AndReturn x = (x < 5, x)
>>
>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>>
>>
>> My view pattern requires (Ord a, Num a), and so I must declare these as
>> required constraints in the pattern synonym type. Because vanilla data
>> constructors never do computation, any required constraints for data
>> constructors are always useless.
>>
>>
>> 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.
>>
>>
>> Does SmartNode need Ord a to match? Or just to produce a node? It seems
>> that Ord a is used only for production, not for matching. This suggests
>> that you want a separate smartNode function (not a pattern synonym) and to
>> have no constraints on the pattern synonym, which can be unidirectional
>> (that is, work only as a pattern, not as an expression).
>>
>> It has been mooted to allow pattern synonyms to have two types: one when
>> used as a pattern and a different one when used as an expression. That
>> might work for you here: you want SmartNode to have no constraints as a
>> pattern, but an Ord a constraint as an expression. At the time, the design
>> with two types was considered too complicated and abandoned.
>>
>> Does this help?
>>
>> 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
>
___
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 => () => ...

[David Feuer]

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.

On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg  wrote:

>
>
> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
> wrote:
>
> >pattern  SmartConstr :: Ord a => () => ...
>
> Seems to mean:
>
> * Required constraint is Ord a  -- fine, for building
>
>
> Yes.
>
> * Provided constraint is Ord a  -- why? for matching/consuming
>
>
> No. Your signature specified that there are no provided constraints:
> that's your ().
>
>
> 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 believe there is no way to have provided constraints in Haskell98. You
> would need either GADTs or higher-rank types.
>
>
> This feels a lot like one of the things that's wrong with 'stupid theta'
> datatype contexts.
>
>
> You're onto something here. Required constraints are very much like the
> stupid theta datatype contexts. But, unlike the stupid thetas, required
> constraints are sometimes useful: they might be needed in order to, say,
> call a function in a view pattern.
>
> For example:
>
> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
> checkLT5AndReturn x = (x < 5, x)
>
> pattern LessThan5 :: (Ord a, Num a) => a -> a
> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>
>
> My view pattern requires (Ord a, Num a), and so I must declare these as
> required constraints in the pattern synonym type. Because vanilla data
> constructors never do computation, any required constraints for data
> constructors are always useless.
>
>
> 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.
>
>
> Does SmartNode need Ord a to match? Or just to produce a node? It seems
> that Ord a is used only for production, not for matching. This suggests
> that you want a separate smartNode function (not a pattern synonym) and to
> have no constraints on the pattern synonym, which can be unidirectional
> (that is, work only as a pattern, not as an expression).
>
> It has been mooted to allow pattern synonyms to have two types: one when
> used as a pattern and a different one when used as an expression. That
> might work for you here: you want SmartNode to have no constraints as a
> pattern, but an Ord a constraint as an expression. At the time, the design
> with two types was considered too complicated and abandoned.
>
> Does this help?
>
> 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: Pattern synonym constraints :: Ord a => () => ...

[Richard Eisenberg]

> On Oct 3, 2021, at 5:38 AM, Anthony Clayden  
> wrote:
> 
> >pattern  SmartConstr :: Ord a => () => ...
> 
> Seems to mean:
> 
> * Required constraint is Ord a  -- fine, for building

Yes.

> * Provided constraint is Ord a  -- why? for matching/consuming

No. Your signature specified that there are no provided constraints: that's 
your ().

> 
> 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 believe there is no way to have provided constraints in Haskell98. You would 
need either GADTs or higher-rank types.

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

You're onto something here. Required constraints are very much like the stupid 
theta datatype contexts. But, unlike the stupid thetas, required constraints 
are sometimes useful: they might be needed in order to, say, call a function in 
a view pattern.

For example:

> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
> checkLT5AndReturn x = (x < 5, x)
> 
> pattern LessThan5 :: (Ord a, Num a) => a -> a
> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )

My view pattern requires (Ord a, Num a), and so I must declare these as 
required constraints in the pattern synonym type. Because vanilla data 
constructors never do computation, any required constraints for data 
constructors are always useless.

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

Does SmartNode need Ord a to match? Or just to produce a node? It seems that 
Ord a is used only for production, not for matching. This suggests that you 
want a separate smartNode function (not a pattern synonym) and to have no 
constraints on the pattern synonym, which can be unidirectional (that is, work 
only as a pattern, not as an expression).

It has been mooted to allow pattern synonyms to have two types: one when used 
as a pattern and a different one when used as an expression. That might work 
for you here: you want SmartNode to have no constraints as a pattern, but an 
Ord a constraint as an expression. At the time, the design with two types was 
considered too complicated and abandoned.

Does this help?

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

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