[Haskell-cafe] Non-linear patterns.

[Serguey Zefirov]

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 <S.J.Thompson at kent.ac.uk>:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250506/8efd88a9/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/8efd88a9/attachment-0001.png>