[Agda] Data.Rational

[Mateusz Kowalczyk]

On 23/03/14 15:42, Mateusz Kowalczyk wrote:
> On 23/03/14 15:29, Amr Sabry wrote:
>> Thank you all for your responses. My take is that there are probably
>> many many ways of implementing rationals and some might be significantly
>> better than others. There is however not even a baseline implementation
>> in the current library for simple operations on the rationals. Using the
>> always-normalized approach that was started in the library, I
>> implemented the basic operations on rationals (unary negation,
>> reciprocal, addition, multiplication, and hence trivially subtraction
>> and division). It's not much but it's start. I am attaching the code in
>> case someone spots obvious improvements and/or problems. If everything
>> looks reasonable, I'd be happy to push to the library. Thanks. --Amr
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> 
> Hi,
> 
> On Agda 2.3.2.1 I get the following type error
> 
> /tmp/Rat.agda:25,1-51,16
> Left hand side gives too many arguments to a function of type
> {m n g : ℕ} →
> {False (n ℕ≟ 0)} →
> {False (g ℕ≟ 0)} →
> GCD m n g →
> Σ-syntax ℕ (λ p → Σ-syntax ℕ (λ q → Coprime p q × False (q ℕ≟ 0)))
> when checking that the clause
> normalize {m} {n} {ℕ.suc g} {_} {_} G with Bézout.identity G
> normalize {m} {.0} {ℕ.suc g} {()} {_}
>   (GCD.is (divides p m≡pg' , divides 0 refl) _)
>   | _
> normalize {m} {n} {ℕ.suc g} {_} {_}
>   (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _)
>   | Bézout.+- x y eq
>   = p ,
>     ℕ.suc q ,
>     Bézout-coprime {p} {ℕ.suc q} {g}
>     (Bézout.+- x y
>      (begin
>       ℕ.suc g ℕ+ y ℕ* (ℕ.suc q ℕ* ℕ.suc g) ≡⟨
>       cong (λ h → ℕ.suc g ℕ+ y ℕ* h) (sym n≡qg') ⟩
>       ℕ.suc g ℕ+ y ℕ* n ≡⟨ eq ⟩
>       x ℕ* m ≡⟨ cong (λ h → x ℕ* h) m≡pg' ⟩ (x ℕ* (p ℕ* ℕ.suc g) ∎)))
>     , tt
> normalize {m} {n} {ℕ.suc g} {_} {_}
>   (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _)
>   | Bézout.-+ x y eq
>   = p ,
>     ℕ.suc q ,
>     Bézout-coprime {p} {ℕ.suc q} {g}
>     (Bézout.-+ x y
>      (begin
>       ℕ.suc g ℕ+ x ℕ* (p ℕ* ℕ.suc g) ≡⟨
>       cong (λ h → ℕ.suc g ℕ+ x ℕ* h) (sym m≡pg') ⟩
>       ℕ.suc g ℕ+ x ℕ* m ≡⟨ eq ⟩
>       y ℕ* n ≡⟨ cong (λ h → y ℕ* h) n≡qg' ⟩
>       (y ℕ* (ℕ.suc q ℕ* ℕ.suc g) ∎)))
>     , tt
> has type
> {m n g : ℕ} →
> {False (n ℕ≟ 0)} →
> {False (g ℕ≟ 0)} →
> GCD m n g →
> Σ-syntax ℕ (λ p → Σ-syntax ℕ (λ q → Coprime p q × False (q ℕ≟ 0)))
> 
> 
> I also advise against leaving trailing whitespace in the file like you
> seem to have done. Lastly, I think the function names don't really fit
> in with the rest of the standard lib, maybe they should be though about
> more?
> 
> Thanks
> 

Forgot to mention that the error can simply be fixed by adding an extra
argument (calling it _ is fine) on line 24.

-- 
Mateusz K.