[Agda] Termination checker on commutative functions

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191031/824e8d66/attachment.html>