<div dir="ltr"><div dir="ltr">I also think it makes sense to allow the O pattern to match any number less than or equal to 0 to make our functions total. So putting it all together, we get something like<div><br></div><div><div>{-# LANGUAGE ViewPatterns #-}</div><div>{-# LANGUAGE PatternSynonyms #-}</div><div><br></div><div>import Prelude hiding (pred)</div><div><br></div><div>leZero :: Int -> Maybe Int</div><div>leZero n | n <= 0 = Just 0</div><div> | otherwise = Nothing</div><div><br></div><div>pred :: Int -> Maybe Int</div><div>pred n | n > 0 = Just (n - 1)</div><div> | otherwise = Nothing</div><div><br></div><div>pattern O <- (leZero -> Just n) where</div><div> O = 0</div><div><br></div><div>pattern S n <- (pred -> Just n) where</div><div> S n = n + 1</div><div><br></div><div>fib :: Int -> Int</div><div>fib O = 1</div><div>fib (S n) = (S n) * fib n</div></div><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Apr 28, 2019 at 10:41 AM Artem Pelenitsyn <<a href="mailto:a.pelenitsyn@gmail.com">a.pelenitsyn@gmail.com</a>> wrote:<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 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" target="_blank">lysxia@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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>
_______________________________________________<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" 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>