2 + 3 is not convertible to 3 + 2

[AndrasKovacs]

Using Church-coded natural numbers, 2 + 3 = 3 + 2 is not provable:

CNat : Type
CNat = (n : Type) -> (n -> n) -> n -> n

CAdd : CNat -> CNat -> CNat
CAdd a b n s z = a n s (b n s z)

N3 : CNat
N3 n s z = s (s (s z))

N2 : CNat
N2 n s z = s (s z)

Fail : CAdd N2 N3 = CAdd N3 N2
Fail = Refl

I get "can't solve constraint between N3 and N2", using Idris2 0.5.1.

[Russoul]

That works xD:

CNat : Type
CNat = (n : Type) -> (n -> n) -> n -> n

CAdd : CNat -> CNat -> CNat
CAdd = \a, b, n, s, z => a n s (b n s z)

N3 : CNat
N3 = \n, s, z => s (s (s z))

N2 : CNat
N2 = \n, s, z => s (s z)

Fail : CAdd N2 N3 = CAdd N3 N2
Fail = Refl

Seemingly, It doesn't unfold the definitions.

[gallais]

You only need CAdd a b = \n, s, z => a n s (b n s z). That'll be because we don't eta-expand in a type-directed manner when comparing stuck neutrals (under-applied definitions are considered stuck).

[AndrasKovacs]

Thanks. I would consider this beta-reduction though, not eta-expansion. It's kind of weird that the arity of a top-level function is a primitive notion on the level of conversion checking.

[gallais]

I think that Agda, Haskell, OCaml, etc. all make a semantic distinction between f xs = \ ys => ... and f xs ys = .... You don't notice it in Agda because things get eta-expanded enough that the definition will reduce.

[ice1000]

I think that Agda, Haskell, OCaml, etc. all make a semantic distinction between f xs = \ ys => ... and f xs ys = .... You don't notice it in Agda because things get eta-expanded enough that the definition will reduce.

Aya and Arend also do this 🤔. What are the benefits? My understanding is that it guarantees the number of arguments supplied for unfold

[cartazio]

in the context of ghc, it has to do with providing an efficient machine calling convention for known arity functions