[Haskell-cafe] Agda's BUILTIN Naturals in Haskell
a.pelenitsyn at gmail.com
Sun Apr 28 14:41:11 UTC 2019
succ' in Li-yao's message is meant to be pred, I guess.
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:
> 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
> 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,
> > at runtime are treated as `Integer`s. My initial idea was to abuse
> > rules to turn `data N = Z | S N` into `Integer` terms somehow, but I'm
> > 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:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe