[Agda] Re: Implicit arguments

[Andreas Abel]

On 13.04.2015 07:32, N. Raghavendra wrote:
> 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!

The reason is that n + m is defined by cases on n.  If n is a variable, 
for instance, then n + ?1 can only be equal to n + ?2 in the 
definitional equality of Agda.  However ?3 + m might reduce depending on 
what ?3 is, so there is often no unique solution.  In particular, Agda 
never tries different values for ?3 to make an equation match, a 
constraint like

   ?3 + (n + m) == n + m

never makes progress, even if there is only one solution: ?3 = zero.

>> 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?

Boring, "obvious" type information tires the human reader out quickly. 
So it is necessary to omit it.  Ideally, Agda would exactly infer what 
we consider obvious...

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/