[Haskell-cafe] Non-linear patterns.

[Serguey Zefirov]

An "Eq a" equality constraint would be enough. I do not ask for equality of
definitions or references, despite the fact these can be used in DSL's.

вт, 6 мая 2025 г. в 11:22, Noon van der Silk <noonsilk at gmail.com>:

> The `Eq` you request there is not quite enough; right? you don't want
> merely a to have an Eq; you want a to be exactly equal to (the other) a?
>
> On Tue, 6 May 2025 at 09:11, Simon Thompson via Haskell-Cafe <
> haskell-cafe at haskell.org> wrote:
>
>> Repeated variables in patterns were allowed in Miranda, a predecessor of
>> Haskell. In a lazy context there are interesting questions about how
>> pattern matches fail, and in particular the point at which equality tests
>> take place in matching a complex pattern. This paper
>>
>> [image: preview.png]
>>
>> BF01887213 <https://dl.acm.org/doi/pdf/10.1007/BF01887213>
>> PDF Document · 1.5 MB <https://dl.acm.org/doi/pdf/10.1007/BF01887213>
>> <https://dl.acm.org/doi/pdf/10.1007/BF01887213>
>>
>> section 6.2 explains how these two definitions differ in meaning
>>
>> g [x,x] = 37
>> g z = 42
>>
>> h [x,y] = 37 , x=y
>> h z = 42
>>
>> Simon
>>
>> On 6 May 2025, at 10:01, Serguey Zefirov <sergueyz at gmail.com> wrote:
>>
>> There are artifacts of old Haskell standards that are a matching against
>> integer value (2 + 2 = 5) and a matching against arithmetic expression (f
>> (n+1) = f n).
>>
>> Both are interesting in requiring a class over type to match.
>>
>> f 10 = 11 has type f :: (Eq a1, Num a1, Num a2) => a1 -> a2
>>
>> f (n+1) = f n has type f :: Integral t1 => t1 -> t2
>>
>> In that vein it is possible to add non-linear patterns by adding an
>> equality constraint on the non-linear matches.
>>
>> E.g., f x x = x would have type f :: Eq a => a -> a -> a
>>
>> For example:
>>
>> data Logic = True | False | Not Logic | Or Logic Logic | And Logic Logic
>> deriving Eq
>>
>> simplify (And x x) = simplify x
>> simplify (Or x x) = simplify x
>> simplify (Not (Not x)) = simplify x
>> simplify x = x
>>
>> Patterns like that are common in simplification/optimization rules. Also,
>> by making them legal, it would be possible to use them in Template Haskell
>> to make better embedded languages.
>>
>> On the implementation side, it can be implemented much like the (n+k)
>> pattern. I also think that pattern matching completeness checker should not
>> change.
>>
>> What would you say?
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>>
>>
>> Simon Thompson | Professor of Logic and Computation
>> School of Computing | University of Kent | Canterbury, CT2 7NF, UK
>> s.j.thompson at kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
>
>
> --
> Noon van der Silk
>
> http://silky.github.io/
>
> "My programming language is kindness."
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250506/03a41dc3/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: preview.png
Type: image/png
Size: 209182 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250506/03a41dc3/attachment-0001.png>