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

[Li-yao Xia]

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