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 {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE PatternSynonyms #-} import Prelude hiding (pred) leZero :: Int -> Maybe Int leZero n | n <= 0 = Just 0 | otherwise = Nothing pred :: Int -> Maybe Int pred n | n > 0 = Just (n - 1) | otherwise = Nothing pattern O <- (leZero -> Just n) where O = 0 pattern S n <- (pred -> Just n) where S n = n + 1 fib :: Int -> Int fib O = 1 fib (S n) = (S n) * fib n On Sun, Apr 28, 2019 at 10:41 AM Artem Pelenitsyn wrote:

succ' in Li-yao's message is meant to be pred, I guess.

-- Best, Artem

On Sun, 28 Apr 2019, 8:01 am Li-yao Xia, wrote:

...

Hi Georgi,

That sounds like a use case for pattern synonyms. As its name suggests, it allows you to give constructor names to patterns. This is quite powerful when combined with view patterns, which allow patterns to use arbitrary logic.

User Guide on pattern synonyms:

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...

pattern Z :: Integer pattern Z = 0

pattern S :: Integer -> Integer pattern S n <- (succ' -> Just n) where S n = n + 1

succ' :: Integer -> Maybe Integer succ' n | n > 0 = Just (n - 1) | otherwise = Nothing

Cheers, Li-yao

...

Hey,

Is there any way to do something similar to what Agda does with natural numbers via BUILTIN pragmas? More precisely I want to have correct-by-construction natural numbers,

On 4/28/19 5:38 AM, Georgi Lyubenov wrote: that

...

at runtime are treated as `Integer`s. My initial idea was to abuse rewrite rules to turn `data N = Z | S N` into `Integer` terms somehow, but I'm not sure if this is possible.

======= Georgi

_______________________________________________ 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.

_______________________________________________ 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.

_______________________________________________ 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.