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 <ekmett at gmail.com> wrote:

>
>
> On Tue, Oct 5, 2021 at 12:39 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.
>>
>
> 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 <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
>>>
>> _______________________________________________
>> 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/20211005/e51c8668/attachment.html>