<div dir="ltr"><div>Hi Jacek,</div><div><br></div><div>The easiest solution here would be to first define a helper function for subtraction on `Nat`, and then use it to deal with the two symmetric cases:<br></div><div><br></div><div>```</div><div><span style="font-family:monospace">module _ where<br><br>open import Agda.Builtin.Nat<br><br>data Int : Set where<br>  Pos : (x : Nat) → Int<br>  Neg : (x : Nat) → Int<br><br>_⊝Nat_ : Nat → Nat → Int<br>x       ⊝Nat zero    = Pos x<br>zero    ⊝Nat y       = Neg y<br>(suc x) ⊝Nat (suc y) = x ⊝Nat y<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 y = x ⊝Nat y<br>Neg x ⊕ Pos y = y ⊝Nat x<br></span></div><div>```</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Oct 31, 2019 at 2:00 AM Jacek Karwowski <<a href="mailto:jac.karwowski@gmail.com">jac.karwowski@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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"><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.8px">Jacek</span></div></div></div></div></div></div></div></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>