<div dir="ltr"><div>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).</div><div><br></div><div>The computation of pattern's complements omits guards and operates only at pattern level. The same can be applied to</div><div><br></div><div>f [10] = 11 -- that is f [x] | x == 10 = 11 or, in Miranda's terms, f [x] = 11, x == 10</div><div>f z = 12</div><div><br></div><div>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.</div><div><br></div><div>In the case of ghc, this is not true:<br><br>ghci> let {f [10] = 11; f _ = 12}<br>ghci> :t f<br>f :: (Eq a1, Num a1, Num a2) => [a1] -> a2<br>ghci> f [10,undefined]<br>12<br>ghci> f [11,undefined]<br>12<br>ghci> f [11]<br>12<br>ghci> f [10]<br>11<br></div><div><br></div><div>Thus, I believe that reasoning from Miranda's paper is not directly applicable here.</div></div><br><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">вт, 6 мая 2025 г. в 11:11, Simon Thompson <<a href="mailto:S.J.Thompson@kent.ac.uk">S.J.Thompson@kent.ac.uk</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">



<div>
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 
<div><br>
</div>
<div>
<div style="display:block">
<div style="display:inline-block" role="link">
<a style="border-radius:10px;font-family:-apple-system,Helvetica,Arial,sans-serif;display:block;width:228px;overflow:hidden;text-decoration:none" rel="nofollow" href="https://dl.acm.org/doi/pdf/10.1007/BF01887213" dir="ltr" role="button" width="228" target="_blank">
<table style="table-layout:fixed;border-collapse:collapse;width:228px;background-color:rgb(229,230,233);font-family:-apple-system,Helvetica,Arial,sans-serif" cellpadding="0" cellspacing="0" border="0" width="228">
<tbody>
<tr>
<td align="center"><img style="width: 228px; height: 295px;" width="228" height="295" alt="preview.png" src="cid:ii_196a4bd8b7bb2f85b031"></td>
</tr>
<tr>
<td>
<table bgcolor="#E5E6E9" cellpadding="0" cellspacing="0" width="228" style="table-layout:fixed;font-family:-apple-system,Helvetica,Arial,sans-serif;background-color:rgb(229,230,233)">
<tbody>
<tr>
<td style="padding:8px 0px">
<div style="max-width:100%;margin:0px 16px;overflow:hidden">
<div style="font-weight:500;font-size:12px;overflow:hidden;text-overflow:ellipsis;text-align:left">
<a rel="nofollow" href="https://dl.acm.org/doi/pdf/10.1007/BF01887213" style="text-decoration:none" target="_blank"><font color="#272727" style="color:rgba(0,0,0,0.847)">BF01887213</font></a></div>
<div style="font-weight:400;font-size:11px;overflow:hidden;text-overflow:ellipsis;text-align:left">
<a rel="nofollow" href="https://dl.acm.org/doi/pdf/10.1007/BF01887213" style="text-decoration:none" target="_blank"><font color="#808080" style="color:rgba(0,0,0,0.498)">PDF Document · 1.5 MB</font></a></div>
</div>
</td>
</tr>
</tbody>
</table>
</td>
</tr>
</tbody>
</table>
</a></div>
</div>
</div>
<div><br>
</div>
<div>section 6.2 explains how these two definitions differ in meaning</div>
<div><br>
</div>
<div>g [x,x] = 37</div>
<div>g z = 42</div>
<div><br>
</div>
<div>h [x,y] = 37 , x=y</div>
<div>h z = 42</div>
<div><br>
</div>
<div>Simon<br id="m_5562759290839151637lineBreakAtBeginningOfMessage">
<div><br>
<blockquote type="cite">
<div>On 6 May 2025, at 10:01, Serguey Zefirov <<a href="mailto:sergueyz@gmail.com" target="_blank">sergueyz@gmail.com</a>> wrote:</div>
<br>
<div>
<div dir="ltr">
<div>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).</div>
<div><br>
</div>
<div>Both are interesting in requiring a class over type to match.</div>
<div><br>
</div>
<div>f 10 = 11 has type f :: (Eq a1, Num a1, Num a2) => a1 -> a2</div>
<div><br>
</div>
<div>f (n+1) = f n has type f :: Integral t1 => t1 -> t2</div>
<div><br>
</div>
<div>In that vein it is possible to add non-linear patterns by adding an equality constraint on the non-linear matches.</div>
<div><br>
</div>
<div>E.g., f x x = x would have type f :: Eq a => a -> a -> a</div>
<div><br>
</div>
<div>For example:</div>
<div><br>
</div>
<div>data Logic = True | False | Not Logic | Or Logic Logic | And Logic Logic deriving Eq</div>
<div><br>
</div>
<div>simplify (And x x) = simplify x</div>
<div>simplify (Or x x) = simplify x</div>
<div>simplify (Not (Not x)) = simplify x</div>
<div>simplify x = x</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>What would you say?</div>
</div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</div>
</blockquote>
</div>
<br>
<div>
<div dir="auto" style="color:rgb(0,0,0);letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none">
<div dir="auto" style="color:rgb(0,0,0);letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none">
<div dir="auto" style="color:rgb(0,0,0);letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none">
<div>Simon Thompson | Professor of Logic and Computation <br>
School of Computing | University of Kent | Canterbury, CT2 7NF, UK<br>
<a href="mailto:s.j.thompson@kent.ac.uk" target="_blank">s.j.thompson@kent.ac.uk</a> | M +44 7986 085754 | W <a href="http://www.cs.kent.ac.uk/~sjt" target="_blank">www.cs.kent.ac.uk/~sjt</a></div>
</div>
</div>
</div>
</div>
<br>
</div>
</div>

</blockquote></div>