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

I fail to see why the guarded definition (h [a,b] = 37, a == b; h z = 42) needs to evaluate tail of (a:b:tail). The computation of pattern's complements omits guards and operates only at pattern level. The same can be applied to f [10] = 11 -- that is f [x] | x == 10 = 11 or, in Miranda's terms, f [x] = 11, x == 10 f z = 12 and we can say that complement of pattern in "f [x] | x == 10" is [], (a:b:c) and, thusly, f [11, undefined] should evaluate to undefined. In the case of ghc, this is not true: ghci> let {f [10] = 11; f _ = 12} ghci> :t f f :: (Eq a1, Num a1, Num a2) => [a1] -> a2 ghci> f [10,undefined] 12 ghci> f [11,undefined] 12 ghci> f [11] 12 ghci> f [10] 11 Thus, I believe that reasoning from Miranda's paper is not directly applicable here. вт, 6 мая 2025 г. в 11:11, Simon Thompson :

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 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@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt