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

[Artem Pelenitsyn]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190428/a61626b8/attachment.html>