[Agda] Re: Implicit arguments

[effectfully]

N. Raghavendra,
> I am
> wondering if it's more efficient to avoid implicit arguments altogether,
> except for truly "background" stuff like universe levels.

This is much like bidirectional type checking: in many cases it's
easier to infer terms than to unify them.

> and it may also be
> easy for other human readers to understand the code

You don't need to understand, how Agda infers implicits, to understand
what the code says.

> Also, it's not at all the case that Agda has to do less work if you make everything
> explicit. The reason for that is that Agda is not very trusting of the user, so if you
> write something explicitly that Agda can figure out for itself it needs to check that
> what you wrote is actually the right thing, i.e. it matches what Agda inferred it ought
> to be.

Also, here is a quote from Edwin Brady's thesis:

"A practical implementation must consider methods for removing
implicit information, whether it be inferable at run-time (like the
length of the Vect) or simply not used (like the element type). Since
implicit information is implicit exactly because it is duplicated in
some other part of the term this amounts to removing subterms whose
values are already known."

> However, whenever we apply bool-ind, we anyway have to provide Agda the
> arguments C and x, that too in unwieldy braces.  It'd be nice if Agda
> rejects the implicit declaration for the arguments C and x in such a
> situation.

Unification is a complex task, and sometimes it's possible to infer
things in a one context and impossible in the another. Even for your
`bool-ind' Agda can sometimes infer `x':

    record Sing {α} {A : Set α} (x : A) : Set α where

    foo : _
    foo = bool-ind {C = Sing} _ _

    bar : Sing true
    bar = foo



I said "Agda usually can't infer `f' from (f x)", but she can in some
useful cases. As an example

    bad-fancy-apply : ∀ {n} -> (List ℕ -> Vec ℕ n) -> List ℕ -> Vec ℕ n
    bad-fancy-apply = id

Here `n' doesn't depend on anything, so if we pass the `fromList'
function, which is defined as

    fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)
    fromList List.[]         = []
    fromList (List._∷_ x xs) = x ∷ fromList xs

to `bad-fancy-apply`, we'll get cannot-instantiate-error, because the
length of the resulting vector does depend. But we can fix this:

    fancy-apply : {k : List ℕ -> ℕ} -> ((xs : List ℕ) -> Vec ℕ (k xs))
-> (xs : List ℕ) -> Vec ℕ (k xs)
    fancy-apply = id

    test-fancy-apply : _
    test-fancy-apply = fancy-apply fromList (1 ∷ 2 ∷ 3 ∷ [])

Now `fancy-apply' reflects the dependency in `fromList'. And Agda is
able to infer that `k'.

Here is an even more fancy example:

    z : (k : Level -> Level) -> Set (suc (k zero))
    z k = Set (k zero)

    s : {j : (Level -> Level) -> Level}
      -> ((k : Level -> Level) -> Set (suc (j k)))
      -> (k : Level -> Level)
      -> Set (suc (k zero ⊔ j (k ∘ suc)))
    s r k = Set (k zero) -> r (k ∘ suc)

    crescendo : {j : (Level -> Level) -> Level}
              -> ((k : Level -> Level) -> Set (j k)) -> Set (j id)
    crescendo r = r id

    test : crescendo (s (s (s z))) ≡ (Set₀ -> Set₁ -> Set₂ -> Set₃)
    test = refl

Still Agda can infer pretty complicated `j' in both `s' and `crescendo'.

I also encoded an ECC, and a bounded dependent quantifier was

    _≥Π_ : ∀ {α}
         -> (A : Type α) {k : ∀ {α'} {A' : Type α'} -> A' ≤ A -> level}
         -> (∀ {α'} {A' : Type α'} {le : A' ≤ A} -> ≤⟦ le ⟧ᵂ -> Type (k le))
         -> Type (α ⊔ᵢ k (≤-refl A))

And inferring `k' still wasn't a problem.

But it's hard to predict, when such an inferring becomes a problem. I
encountered some cases, that look simple to me, but not to Agda.