Agda's BUILTIN Naturals in Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Agda's BUILTIN Naturals in Haskell

Georgi Lyubenov
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.
Reply | Threaded
Open this post in threaded view
|

Re: Agda's BUILTIN Naturals in Haskell

Li-yao Xia-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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, <[hidden email]> 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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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, <[hidden email]> 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.

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