[Agda] Re: Implicit arguments

[N. Raghavendra]

At 2015-04-13T03:16:38+04:00, effectfully wrote:

> Agda can't infer `n' from (n + m), if `m' is known.

Many thanks for the explanation.

It's indeed surprising that Agda can infer m, but not n, from n + m, but
perhaps it's only my naivete!

> A little more complicated example:
>
>     postulate
>       fancy₄ : ∀ n {m p} -> Vec ℕ (n + m + p) -> Vec ℕ (n + m) -> ⊤
>
>     test-fancy₄ : ⊤
>     test-fancy₄ = fancy₄ 2 (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) (1 ∷ 2 ∷ 3 ∷ [])
>
> (n = 2, n + m + p = 5, n + m = 3) => (n = 2, m = 1, p = 2)

Looks like Agda has to do a lot of work inferring these implicits!  I am
wondering if it's more efficient to avoid implicit arguments altogether,
except for truly "background" stuff like universe levels.  Without
implicits, it looks like Agda has to do less work, and it may also be
easy for other human readers to understand the code.  What do you feel?

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/