Translating "zero" constructor of Nat to "0" literal

[viktorcsimma]

I've found @uncle-betty's workaround for natural pattern matching at #117 quite useful. To be more precise, this one, when we make an equivalent version where we only pattern-match for zero:

module Test where

open import Haskell.Prelude
open import Haskell.Prim using (monusNat)

fac3 : Nat → Nat
fac3 0       = 1
fac3 (suc n) = suc n * fac3 n

{-# TERMINATING #-}
fac3' : Nat → Nat
fac3' 0 = 1
fac3' n = n * fac3' (monusNat n 1)

{-# COMPILE AGDA2HS fac3' #-}

fac3'≡fac3 : ∀ n → fac3' n ≡ fac3 n
fac3'≡fac3 zero = refl
fac3'≡fac3 (suc n) rewrite fac3'≡fac3 n = refl

However, this is not supported anymore per #154. I consider it to be useful; so I've rewritten Function.hs so that it always rewrites Agda.Builtin.Nat.Nat.zero to a 0 literal. Pattern matching to suc would still be rejected.

I don't know whether it would require a broader consensus; but I think we wouldn't lose anything by adding this feature. Thanks in advance for looking at it:)

[jespercockx]

Thanks for the PR, but I am still not convinced that using Agda's builtin Nat type in non-erased parts of Agda2Hs makes any sense. There is no default type in Haskell that corresponds to it, so I don't even know what kind of useful code you'd want to get out of this.

[viktorcsimma]

You are right about the Natural type… but still, recursive functions with a case for 0 and a case for everything else are legal Haskell code, maybe even idiomatic. (The factorial function is something I can imagine as an example – that could be written in Agda with integers and an erased proof that they are nonnegative, but it would look strange.) Maybe the Natural type can be replaced with Integer, but we should think about how to handle the negative cases then… I don’t what the best solution would be for that. But I think that might belong to a separate issue.

[viktorcsimma]

Maybe an idea for a replacement of naturals would be some kind of record, with an integer and an erased proof. And that could be used in the Agda code, and the Haskell code would simply work with Integers. This might be implemented in our Haskell library and imported instead of Agda’s Nat.