[Haskell-cafe] Agda's BUILTIN Naturals in Haskell

[Jake]

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 <a.pelenitsyn at gmail.com>
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, <lysxia at gmail.com> 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.html#pattern-synonyms
>>
>> 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
>>
>> On 4/28/19 5:38 AM, Georgi Lyubenov wrote:
>> > 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,
>> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190430/3dd57559/attachment.html>