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 <lists at richarde.dev> 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 <david.feuer at 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 <lists at richarde.dev>
> wrote:
>
>>
>>
>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden <anthony.d.clayden at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20211006/06172ca7/attachment-0001.html>