<div dir="auto"><div>succ' in Li-yao's message is meant to be pred, I guess.</div><div dir="auto"><br></div><div dir="auto">--</div><div dir="auto">Best, Artem</div><div dir="auto"><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Sun, 28 Apr 2019, 8:01 am Li-yao Xia, <<a href="mailto:lysxia@gmail.com">lysxia@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Georgi,<br>
<br>
That sounds like a use case for pattern synonyms. As its name suggests, <br>
it allows you to give constructor names to patterns. This is quite <br>
powerful when combined with view patterns, which allow patterns to use <br>
arbitrary logic.<br>
<br>
User Guide on pattern synonyms: <br>
<a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#pattern-synonyms" rel="noreferrer noreferrer" target="_blank">https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#pattern-synonyms</a><br>
<br>
pattern Z :: Integer<br>
pattern Z = 0<br>
<br>
pattern S :: Integer -> Integer<br>
pattern S n <- (succ' -> Just n) where<br>
   S n = n + 1<br>
<br>
succ' :: Integer -> Maybe Integer<br>
succ' n | n > 0 = Just (n - 1)<br>
         | otherwise = Nothing<br>
<br>
Cheers,<br>
Li-yao<br>
<br>
On 4/28/19 5:38 AM, Georgi Lyubenov wrote:<br>
> Hey,<br>
> <br>
> Is there any way to do something similar to what Agda does with natural<br>
> numbers via BUILTIN pragmas?<br>
> More precisely I want to have correct-by-construction natural numbers, that<br>
> at runtime are treated as `Integer`s. My initial idea was to abuse rewrite<br>
> rules to turn `data N = Z | S N` into `Integer` terms somehow, but I'm not<br>
> sure if this is possible.<br>
> <br>
> =======<br>
> Georgi<br>
> <br>
> <br>
> _______________________________________________<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" rel="noreferrer noreferrer" 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.<br>
> <br>
_______________________________________________<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" rel="noreferrer noreferrer" 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.</blockquote></div></div></div>