Disastrous expansion of operations in `Data.Rational.Base`

[MatthewDaggitt]

The operations such as addition and multiplication in Data.Rational.Base are defined in terms of the numerator and denominator projection operations, e.g.

agda-stdlib/src/Data/Rational/Base.agda

Lines 206 to 207 in 650e05f

	_+_ : ℚ → ℚ → ℚ
	p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

This is beautiful and elegant, and arguably the right way to define them. However, it does mean that Agda unfolds these definitions automatically. By the time you have an expression x + y + z + a + b + c the unfolded expression is over 200 lines long.

This makes the rational numbers almost impossible to work with in large proofs. In recent proofs I've resorted to redefining everything that's needed under the abstract keyword.

[MatthewDaggitt]

See also the recent mailing list issue which was also caused by this problem.

[MatthewDaggitt]

Suggestion from @andreasabel: investigate using --no-eta-equality in record

[andreasabel]

Turn off eta-equality but still allow pattern matching:

module Data.Rational.Base where
...
record ℚ : Set where
  no-eta-equality; pattern
  constructor mkℚ
  ...

As @gallais said, you need to match on some arguments to enable reductions:

>-nonZero : ∀ {p} → p > 0ℚ → NonZero p
>-nonZero {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.>-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)

<-nonZero : ∀ {p} → p < 0ℚ → NonZero p
<-nonZero {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.<-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)

positive : ∀ {p} → p > 0ℚ → Positive p
positive {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.positive {toℚᵘ p} (ℚᵘ.*<* p<q)

negative : ∀ {p} → p < 0ℚ → Negative p
negative {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.negative {toℚᵘ p} (ℚᵘ.*<* p<q)

nonPositive : ∀ {p} → p ≤ 0ℚ → NonPositive p
nonPositive {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} (ℚᵘ.*≤* p≤q)

nonNegative : ∀ {p} → p ≥ 0ℚ → NonNegative p
nonNegative {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q)
...

You can force matching with p@(mkQ _ _ _) to make things reduce more lazily:

-- addition
_+_ : ℚ → ℚ → ℚ
p@(mkℚ _ _ _) + q@(mkℚ _ _ _) = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

-- multiplication
_*_ : ℚ → ℚ → ℚ
p@(mkℚ _ _ _) * q@(mkℚ _ _ _) = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)
...

[andreasabel]

Alternative way to force matching: x@record{} (closer to Haskell, don't need to mention constructor name):

_+_ : ℚ → ℚ → ℚ
p@record{} + q@record{} = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

[MatthewDaggitt]

Ooh that's even nicer. Yup, I'm happy with that solution.

[MatthewDaggitt]

Going to have a hack at this now.

[MatthewDaggitt]

Hmm, we have the same issue with multiplication in Data.Integer but that's appears harder to fix as there's no one constructor to pattern match on....