arithmetic operations of Cubical.Data.Rationals is super slow

[onestruggler]

The stdlib Data.Rational is fast. The follwing code compute instanrtly.

{-# OPTIONS --safe --cubical --two-level #-}
module Scalar where
open import Data.Rational as ℚ hiding (_+_ ; _*_)
open import Data.Integer as ℤ hiding (_+_ ; _*_)

data ℚ[ω] : Set where
  _ω³+_ω²+_ω+_ : ℚ -> ℚ -> ℚ -> ℚ -> ℚ[ω]

infixl 6 _+_
infixl 7 _*_
infix 7 _s*_

_+_ :  ℚ[ω] ->  ℚ[ω] ->  ℚ[ω]
(a ω³+ b ω²+ c ω+ d) + (a' ω³+ b' ω²+ c' ω+ d') = (a ℚ.+ a') ω³+ (b ℚ.+ b') ω²+ (c ℚ.+ c') ω+ (d ℚ.+ d') 


_*_ :  ℚ[ω] ->  ℚ[ω] ->  ℚ[ω]
(a ω³+ b ω²+ c ω+ d) * (a' ω³+ b' ω²+ c' ω+ d') = a'' ω³+ b'' ω²+ c'' ω+ d'' where
  a'' = a ℚ.* d'  ℚ.+  b ℚ.* c'  ℚ.+  c ℚ.* b'  ℚ.+  d ℚ.* a'
  b'' = b ℚ.* d'  ℚ.+  c ℚ.* c'  ℚ.+  d ℚ.* b' ℚ.- a ℚ.* a'
  c'' = c ℚ.* d'  ℚ.+  d ℚ.* c' ℚ.- a ℚ.* b' ℚ.- b ℚ.* a'
  d'' = d ℚ.* d'  ℚ.-  a ℚ.* c'  ℚ.-  b ℚ.* b'  ℚ.-  c ℚ.* a'

_s*_ : ℚ -> ℚ[ω] -> ℚ[ω]
q s* (a ω³+ b ω²+ c ω+ d) = (q ℚ.* a) ω³+ (q ℚ.* b) ω²+ (q ℚ.* c) ω+ (q ℚ.* d)

Q0 = 0ℚ
P0 = (Q0 ω³+ Q0 ω²+ Q0 ω+ Q0) -- 0

P1 = (0ℚ ω³+ 0ℚ ω²+ 0ℚ ω+ 1ℚ) -- 1
M1 = (0ℚ ω³+ 0ℚ ω²+ 0ℚ ω+ (ℚ.- 1ℚ)) -- -1
Pi = (0ℚ ω³+ 1ℚ ω²+ 0ℚ ω+ 0ℚ) -- i
Mi = (0ℚ ω³+ (ℚ.- 1ℚ) ω²+ 0ℚ ω+ 0ℚ) -- -i
Pw = (0ℚ ω³+ 0ℚ ω²+ 1ℚ ω+ 0ℚ) -- ω
Mw = (0ℚ ω³+ 0ℚ ω²+ (ℚ.- 1ℚ) ω+ 0ℚ) -- -ω
-- ½ = [ 1 / 2 ]
---½ = ℚ.- ½



1/√2 = ½ s* ((ℚ.- 1ℚ) ω³+ 0ℚ ω²+ 1ℚ ω+ 0ℚ) -- 1/√2
-1/√2 = -½ s* ((ℚ.- 1ℚ) ω³+ 0ℚ ω²+ 1ℚ ω+ 0ℚ) -- -1/√2

t : {!!}
t = {!-1/√2 * 1/√2 * 1/√2 * 1/√2!}

But the same code using Cubical's rational lib falis to compute. Even multiplication of two numbers -1/√2 * 1/√2 is slow. See the following code.

{-# OPTIONS --safe --cubical --two-level #-}
module Scalar where
open import Cubical.Data.Rationals as ℚ hiding (_+_)
open import Cubical.Data.Int as ℤ hiding (_+_)
open import Cubical.Data.NatPlusOne

data ℚ[ω] : Set where
  _ω³+_ω²+_ω+_ : ℚ -> ℚ -> ℚ -> ℚ -> ℚ[ω]

infixl 6 _+_
infixl 7 _*_
infix 7 _scalar-mult_

_+_ :  ℚ[ω] ->  ℚ[ω] ->  ℚ[ω]
(a ω³+ b ω²+ c ω+ d) + (a' ω³+ b' ω²+ c' ω+ d') = (a ℚ.+ a') ω³+ (b ℚ.+ b') ω²+ (c ℚ.+ c') ω+ (d ℚ.+ d') 


_*_ :  ℚ[ω] ->  ℚ[ω] ->  ℚ[ω]
(a ω³+ b ω²+ c ω+ d) * (a' ω³+ b' ω²+ c' ω+ d') = a'' ω³+ b'' ω²+ c'' ω+ d'' where
  a'' = (a ℚ.· d')  ℚ.+  (b ℚ.· c')  ℚ.+  (c ℚ.· b')  ℚ.+  (d ℚ.· a')
  b'' = ((b ℚ.· d')  ℚ.+  (c ℚ.· c')  ℚ.+  (d ℚ.· b'))  ℚ.-  (a ℚ.· a')
  c'' = (((c ℚ.· d')  ℚ.+  (d ℚ.· c'))  ℚ.-  (a ℚ.· b'))  ℚ.-  (b ℚ.· a')
  d'' = (((d ℚ.· d')  ℚ.-  (a ℚ.· c'))  ℚ.-  (b ℚ.· b'))  ℚ.-  (c ℚ.· a')

_scalar-mult_ : ℚ -> ℚ[ω] -> ℚ[ω]
q scalar-mult (a ω³+ b ω²+ c ω+ d) = (q ℚ.· a) ω³+ (q ℚ.· b) ω²+ (q ℚ.· c) ω+ (q ℚ.· d)

P0 = (0 ω³+ 0 ω²+ 0 ω+ 0) -- 0
Q0 = [ 0 / 1 ]
P1 = (0 ω³+ 0 ω²+ 0 ω+ 1) -- 1
M1 = (0 ω³+ 0 ω²+ 0 ω+ (ℚ.- 1)) -- -1
Pi = (0 ω³+ 1 ω²+ 0 ω+ 0) -- i
Mi = (0 ω³+ (ℚ.- 1) ω²+ 0 ω+ 0) -- -i
Pw = (0 ω³+ 0 ω²+ 1 ω+ 0) -- ω
Mw = (0 ω³+ 0 ω²+ (ℚ.- 1) ω+ 0) -- -ω
½ = [ 1 / 2 ]
-½ = [ ℤ.- 1 / 2 ]



1/√2 = ½ scalar-mult (-1 ω³+ 0 ω²+ 1 ω+ 0) -- 1/√2
-1/√2 = -½ scalar-mult (-1 ω³+ 0 ω²+ 1 ω+ 0) -- -1/√2

t : {!!}
t = {!-1/√2 * 1/√2 * 1/√2 * 1/√2!}

For cubical, I use Agda version 2.6.4.3 + cubical-0.7 ;
for std lib, I use Agda version 2.6.5-422b932 + Version 2.0.

Also, the infixity of ℚ.- in cubical is problematic, I have to put extra parenthes to get the correct result.

Thanks.

[LuuBluum]

This might be due to overeager normalization of arithmetic in Agda? The standard library has a fix with some record prefixes and no-eta-equality, but this isn't the case for Cubical.

Also Cubical's rationals-as-a-set-quotient representation has arithmetic defined in a way that has some undesired usage of recursors that make computation clunky. The details are abstracted to try and reduce the problem, but it's still there until the implementation is updated to avoid calling the recursor entirely. Better to pattern-match so that the associativity proof doesn't get dragged around with every computational step, abstracted or otherwise.