[Agda] Termination checker on commutative functions

[Jacek Karwowski]

Hi Jesper,

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).
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).

Let's say there are three constructors:
```
postulate
  X : Set
  Y : Set
  Z : Set
  T' : Set

data T : Set where
  A : X -> T
  B : Y -> T
  C : Z -> T
```

and I'd now like to define a commutative function over them.

```
f : T -> T -> T'
f (A x) (A x) = (some complicated definition using the specifics of x's)
f (A x) (B y) = (some complicated definition using the specifics of x's and
y's)
f (A x) (C z) = (some complicated definition using the specifics of x's and
z's)
-- etc for all other required cases
-- and now I don't want to repeat code from above, but I want to be able to
define
f (B y) (A x) = f (A x) (B y)
f (C z) (A x) = f (A x) (C z)
f (C z) (B y) = f (B y) (C z)
```

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?

Best
Jacek

On Thu, Oct 31, 2019 at 5:03 AM Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Jacek,
>
> 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:
>
> ```
> module _ where
>
> open import Agda.Builtin.Nat
>
> data Int : Set where
>   Pos : (x : Nat) → Int
>   Neg : (x : Nat) → Int
>
> _⊝Nat_ : Nat → Nat → Int
> x       ⊝Nat zero    = Pos x
> zero    ⊝Nat y       = Neg y
> (suc x) ⊝Nat (suc y) = x ⊝Nat y
>
> _⊕_ : Int → Int → Int
> Pos x ⊕ Pos y = Pos (x + y)
> Neg x ⊕ Neg y = Neg (x + y)
> Pos x ⊕ Neg y = x ⊝Nat y
> Neg x ⊕ Pos y = y ⊝Nat x
> ```
>
> -- Jesper
>
> On Thu, Oct 31, 2019 at 2:00 AM Jacek Karwowski <jac.karwowski at gmail.com>
> wrote:
>
>> Hi,
>>
>> I'm trying to write a commutative function over some type, and not repeat
>> the code in the process.
>>
>> The toy example is as follows:
>> ```
>> module _ where
>>
>> open import Data.Nat
>>
>> data Int : {i : Size} -> Set where
>>   Pos : (x : ℕ) -> Int
>>   Neg : (x : ℕ) -> Int
>>
>> _⊕_ : Int -> Int -> Int
>> Pos x ⊕ Pos y = Pos (x + y)
>> Neg x ⊕ Neg y = Neg (x + y)
>> Pos x ⊕ Neg zero = Pos x
>> Pos zero ⊕ Neg y = Neg y
>> Pos (suc x) ⊕ Neg (suc y) = (Pos x) ⊕ (Neg y)
>> --- problematic call
>> Neg x ⊕ Pos y = (Pos y) ⊕ (Neg x)
>> ```
>> In the example above, termination checker complains about the last call,
>> since it is not a structural recursion.
>>
>> (Of course, real types can (and do) have more than two constructors, the
>> constructors are recursive, etc.)
>>
>> 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:
>>
>> ```
>> ord : Int -> ℕ
>> ord (Pos _) = 0
>> ord (Neg _) = 1
>>
>> _⊕_ : {s : ℕ} -> (x : Int) -> {s ≡ ord x} -> Int -> Int
>> Pos x ⊕ Pos y = Pos (x + y)
>> Neg x ⊕ Neg y = Neg (x + y)
>> Pos x ⊕ Neg zero = Pos x
>> Pos zero ⊕ Neg y = Neg y
>> Pos (suc x) ⊕ Neg (suc y) = _⊕_ {zero} (Pos x) {refl} (Neg y)
>> --- problematic call
>> _⊕_ {suc zero} (Neg x) (Pos y) = _⊕_ {zero} (Pos y) {refl} (Neg x)
>> ```
>> but this ends up being very ugly and hard to read.
>>
>> What is the idiomatic way of handling these types of situations,
>> introducing as little code overhead as possible?
>>
>> Thanks,
>> Jacek
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>

-- 
Best regards
Jacek Karwowski
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191107/5de4612f/attachment.html>