<div dir="ltr">Hi Jesper,<div><br></div><div>Thanks for your response and your time. This indeed solves the example toy  problem, but it does that by exploiting some structure in this code (this obviously means it wasn't a good example to begin with, sorry about that).</div><div>What I'm looking for, In general, is a fully general solution that treats the constructors as more-or-less black boxes (in particular, under assumption that there's no easy way of defining functions over subsets of them, like you did with substraction).</div><div><br></div><div>Let's say there are three constructors:</div><div>```</div><div>postulate</div><div>  X : Set</div><div>  Y : Set</div><div>  Z : Set</div><div>  T' : Set</div><div><br></div><div>data T : Set where</div><div>  A : X -> T</div><div>  B : Y -> T</div><div>  C : Z -> T</div><div>```</div><div><br></div><div>and I'd now like to define a commutative function over them.</div><div><br></div><div>```</div><div>f : T -> T -> T'</div><div>f (A x) (A x) = (some complicated definition using the specifics of x's)</div><div><div>f (A x) (B y) = (some complicated definition using the specifics of x's and y's)</div><div></div></div><div><div><div>f (A x) (C z) = (some complicated definition using the specifics of x's and z's)</div><div>-- etc for all other required cases</div><div>-- and now I don't want to repeat code from above, but I want to be able to define</div><div>f (B y) (A x) = f (A x) (B y)</div><div>f (C z) (A x) = f (A x) (C z)</div><div>f (C z) (B y) = f (B y) (C z)</div><div>```</div><div><br></div><div>There's no easy way of refactoring out these particular cases, and then just using this refactored-out function with changed order of arguments. So, is there any "idiomatic" way of dealing with these kinds of situations?</div><div><br></div><div>Best</div><div>Jacek</div><div></div></div><div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Oct 31, 2019 at 5:03 AM Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</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"><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" target="_blank">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>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><span style="font-size:12.8px">Best regards</span><br></div><div><span style="font-size:12.8px">Jacek Karwowski</span></div></div></div></div></div></div></div>