<div dir="ltr">Hi,<div><br></div><div>I'm trying to write a commutative function over some type, and not repeat the code in the process.</div><div><br></div><div>The toy example is as follows:</div><div>```</div><div>module _ where<br><br>open import Data.Nat<br><br>data Int : {i : Size} -> Set where<br>  Pos : (x : ℕ) -> Int<br>  Neg : (x : ℕ) -> Int<br><br>_⊕_ : Int -> Int -> Int<br>Pos x ⊕ Pos y = Pos (x + y)<br>Neg x ⊕ Neg y = Neg (x + y)<br>Pos x ⊕ Neg zero = Pos x<br>Pos zero ⊕ Neg y = Neg y<br>Pos (suc x) ⊕ Neg (suc y) = (Pos x) ⊕ (Neg y)<br>--- problematic call<br>Neg x ⊕ Pos y = (Pos y) ⊕ (Neg x)<br><div>```</div><div>In the example above, termination checker complains about the last call, since it is not a structural recursion.</div><div><div><br></div><div>(Of course, real types can (and do) have more than two constructors, the constructors are recursive, etc.)</div></div><div><br></div><div>The naive, manual way I see would be to introduce an explicit order on the constructors by some external function, and then call ⊕ passing this parameter over:</div><div><br></div><div>```</div><div>ord : Int -> ℕ<br>ord (Pos _) = 0<br>ord (Neg _) = 1<br><br>_⊕_ : {s : ℕ} -> (x : Int) -> {s ≡ ord x} -> Int -> Int<br>Pos x ⊕ Pos y = Pos (x + y)<br>Neg x ⊕ Neg y = Neg (x + y)<br>Pos x ⊕ Neg zero = Pos x<br>Pos zero ⊕ Neg y = Neg y<br>Pos (suc x) ⊕ Neg (suc y) = _⊕_ {zero} (Pos x) {refl} (Neg y)<br>--- problematic call<br>_⊕_ {suc zero} (Neg x) (Pos y) = _⊕_ {zero} (Pos y) {refl} (Neg x)<br></div><div>```</div><div>but this ends up being very ugly and hard to read.</div><div><div><br></div><div>What is the idiomatic way of handling these types of situations, introducing as little code overhead as possible?</div><div></div></div><div><br></div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><span style="font-size:12.8px">Thanks,</span></div><div><span style="font-size:12.8000001907349px">Jacek</span></div></div></div></div></div></div></div></div></div>