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

[Edward Kmett]

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/a473505d/attachment.html>