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

6 Oct 2021

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