Add predecessor for natural numbers

[jespercockx]

For reasons (TM) I wanted to implement a recursor for natural numbers in agda2hs. Since pattern matching on Natural is not allowed in Haskell, I thought I'd use ifDec instead. However, in the non-zero branch I need to take the predecessor in order to make the recursive call:

recNat : (a : @0 Nat → Set)
       → (z : a 0)
       → (s : (m : Nat) → a m → a (suc m))
       → (n : Nat) → a n
recNat a z s n = ifDec (n ≟ 0)
  (λ where {{refl}} → z)
  (λ {{n≠0}} →
    case predNat n n≠0 of λ where
      (m ⟨ refl ⟩) → s m (recNat a z s m))

{-# COMPILE AGDA2HS recNat #-}

predNat needs a somewhat complicated (but sensible) type:

predNat : (n : Nat) → @0 (n ≡ 0 → ⊥) → ∃ Nat λ m → n ≡ suc m

Since it doesn't seem possible to implement predNat with the primitives that agda2hs currently provides, I thought it could be nice to add it as a primitive, so more complex functions like recNat can be implemented on top. WDYT?

(The definition of _≟_ is currently missing from the agda2hs prelude, but it can readily be defined:

_≟_ : {{_ : Eq a}} {{_ : IsLawfulEq a}} → (x y : a) → Dec (x ≡ y)
x ≟ y = (x == y) ⟨ isEquality x y ⟩

{-# COMPILE AGDA2HS _≟_ inline #-}

)

[jwaldmann]

Since pattern matching on Natural is not allowed in Haskell,

that depends on the exact definition of "Haskell":

ghci> import Numeric.Natural 
ghci> :set -XNPlusKPatterns 
ghci> f :: Natural -> Natural ; f 0 = 5; f (x+1)= x
ghci> f 8
7

How does MAlonzo solve this?

[jespercockx]

Oh right, I forgot about NPlusKPatterns. I thought it was deprecated, but I guess it is still usable so we could indeed target it.

I believe MAlonzo just compiles the patterns to guards: a zero pattern becomes a guard n == 0 and a suc m pattern becomes a guard n > 0 and a let-binding m = n-1. We could do the same in agda2hs but it would break with our goal of just representing Haskell features using Agda syntax.

[jwaldmann]

SPJ says (2017) "n+k patterns were removed in later versions of Haskell (Haskell 2010 I think) but GHC still supports them." https://gitlab.haskell.org/ghc/ghc/-/issues/14100#note_141172

(MAlonzo) ... becomes a guard

I am looking at a random example in my project,

du_Nat'45'sws_16 ::
  Integer ->
  Integer ->
  ...
du_Nat'45'sws_16 v0 v1 v2 v3
  = case coe v0 of
      0 -> coe v2
      _ -> let v4 = subInt (coe v0) (coe (1 :: Integer)) in
...

This matches on 0, avoids NPlusK, and takes non-negativity for granted?

[jespercockx]

That's exactly what I was talking about. Even though it would go somewhat against the philosophy of agda2hs, it might still be the easiest way to just add support for pattern matching on Nats in this way, which would also let me implement the predNat function from the OP.

[jespercockx]

I experimented a bit with using a view pattern for this, and I got

myPred : Nat → Nat
myPred zero = zero
myPred (suc n) = n

to compile to

myPred :: Natural -> Natural
myPred 0 = 0
myPred (pred -> n) = n

which looks pretty nice to me. However, it doesn't work correctly when the clauses are swapped. Unlike MAlonzo, agda2hs compiles each clause in isolation and preserves the ordering of the clauses, so the strategy of matching on 0/_ wouldn't work either.

One rather ugly solution would be to generate the following instead:

myPred :: Natural -> Natural
myPred 0 = 0
myPred (`minusNaturalMaybe` 1 -> Just n) = n

which makes the clauses order-independent but does not even remotely resemble hand-written Haskell code.

The other solution would be to generate a guard anyway, which we would have to propagate to the top level of the clause.

EDIT: generating a guard has the rather ugly side-effect that we need to name the input itself rather than just its predecessor, which adds more syntactic noise. Generating readable code is really a lot harder than it looks...

My proposal in the OP has the nice property that it is trivial to compile to readable code, we can just compile predNat straight to pred. Maybe we should just accept the extra syntax noise on the Agda side as the price we have to pay for readable Haskell code.