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

newer
Re: Glasgow-haskell-users Digest,...

older
Re: InstanceSigs -- rationale for...

Anthony Clayden

3 Oct 2021 3 Oct '21

9:38 a.m.

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

Attachments:

attachment.html (text/html — 5.2 KB)

Show replies by date

Richard Eisenberg

5 Oct 5 Oct

4:32 p.m.

...

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

David Feuer

4:38 p.m.

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

Edward Kmett

5:11 p.m.

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

David Feuer

5:14 p.m.

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

Richard Eisenberg

9:53 p.m.

You're right -- my apologies. Here is the accepted proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bi... 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 mailto:lists@richarde.dev> wrote:

...
On Oct 3, 2021, at 5:38 AM, Anthony Clayden mailto:anthony.d.clayden@gmail.com> 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 mailto:Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Anthony Clayden

6 Oct 6 Oct

2:07 a.m.

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

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

Gergő Érdi

2:23 a.m.

...

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

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

Gergő Érdi

2:25 a.m.

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

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

Anthony Clayden

5:25 a.m.

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.

...

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

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

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

anthony.d.clayden@gmail.com> 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:

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

...
...
...
...
You're onto something here. Required constraints are very much like

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

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

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! that's your (). theta' datatype contexts. 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. this node. Note it's the same `a` with the same `Ord a` 'all the way down' the Tree. 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

Simon Peyton Jones

8:24 a.m.

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 manualhttps://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.htm... 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 simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@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:gergo@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&data=04%7C01%7Csimonpj%40microsoft.com%7Cf208f3e0240646a9829f08d98889d751%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637690948080937568%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=YhqSQ%2BWSfz5Ycmt8aynh9jJaUVNiiK3kkPrLj1pILx4%3D&reserved=0 On Wed, Oct 6, 2021 at 10:23 AM Gergő Érdi mailto:gergo@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 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 mailto:anthony.d.clayden@gmail.com> 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 mailto:lists@richarde.dev> wrote:

...
You're right -- my apologies. Here is the accepted proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bi...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0042-bidir-constr-sigs.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cf208f3e0240646a9829f08d98889d751%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637690948080947564%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=Cdf7aEeHc8yXFJCn8aX9WdGGJueQsqGK0zY7Ib%2B6FsY%3D&reserved=0

Richard

On Oct 5, 2021, at 12:38 PM, David Feuer mailto:david.feuer@gmail.com> 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 mailto:lists@richarde.dev> wrote:

...
On Oct 3, 2021, at 5:38 AM, Anthony Clayden mailto:anthony.d.clayden@gmail.com> 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.orgmailto:Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7Cf208f3e0240646a9829f08d98889d751%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637690948080957559%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=z1wP8QMlfRhfNmbX0n0HuoYx6MufLQdMjCTgBVZMqcs%3D&reserved=0

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7Cf208f3e0240646a9829f08d98889d751%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637690948080967559%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=dw%2BRrhD1RqrZYMSCjXNRofuuC6PHtgRjVd%2BmlBQQkoI%3D&reserved=0

Anthony Clayden

10:41 a.m.

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 https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.htm... 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. <CReq> 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).

Simon Peyton Jones

11:11 a.m.

<CReq> 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. * <CReq> and <CProv> 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 simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@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:simonpj@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 manualhttps://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&data=04%7C01%7Csimonpj%40microsoft.com%7C941ec01fb46743eefb4d08d988b5e64a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637691137569565464%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=B7ZHX1fB5hRZkVuvId1OhnC6j5oYoqeSaD2hByBAPRM%3D&reserved=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. <CReq> 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).

ÉRDI Gergő

11:14 a.m.

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.

Anthony Clayden

12:55 a.m.

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

1368

Age (days ago)

1371

Last active (days ago)

List overview

Download

14 comments

7 participants

participants (7)

Anthony Clayden
David Feuer
Edward Kmett
Gergő Érdi
Richard Eisenberg
Simon Peyton Jones
ÉRDI Gergő

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

tags

participants (7)