[Agda] Avoiding implicit argument proliferation?

[Brandon Moore]

On 2011-03-25 04:14 Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-03-23 08:00, Brandon Moore wrote:
> > Here's some code, extracted  from an attempt at formalizing early excercies
> > in "Categories for the  Working Mathematician". The hidden arguments
> > continue to accumulate as  higher structures are build. They can be 
inferred,
> > so working with these  definitions in expressions is not too bad, but to 
>state
> > any types it  seems I need to quantify over (and manually provide) all these
> > implicit  arguments.
> 
> See the following thread for a previous discussion about this  issue:
> 
>   Why aren't free vars in types automatically  generalized
>   http://thread.gmane.org/gmane.comp.lang.agda/772

Thanks for the reference. Unfortunately, it seems light on suggestions
for working with the present language. I do have some ideas for automatically
quantifying over implicit parameters that might work a bit better than the
ones mentioned in that thread, but there are still some problems to work out.
Anyway, I was hoping for suggestions that work with the current language.

I have found a partial solution. At least, it works on small examples; I haven't
converted the whole program yet. In short, make a module which rewrites
all the record components according to an equality, and use that.

My problem isn't that I mind explicitly quantifying over implicit parameters,
it is the they types of those parameters have parameters, and those parameters
have types with parameters and so on.

Working with records containing types avoids having to pass these parameters,
and works great as long as the types can be independent, but I lacked a good
approach for constraining two records to agree on a type component.

For a simple example, take a record with a function between two sets

record Fun : Set₁ where
  field
    A B : Set
    f : A → B

Defining a commutative square is easy:

record Square : Set₁ where
  field
    F G : Fun
    top : Fun.A F → Fun.A G
    bottom : Fun.B F → Fun.B G
    commute : (x : Fun.A F) → Fun.f G (top x) ≡ bottom (Fun.f F x)

Working with records that are supposed to agree is harder.

compose : (R1 R2 : Fun) → Fun.B R1 ≡ Fun.A R2 → Fun
compose R1 R1 eq = ?

Rewriting by eq has no effect, and I can't match on it:

Cannot pattern match on constructor refl, since the inferred
indices [Fun.B R3] cannot be unified with the expected indices
[Fun.A R4] for some R4, R3
when checking that the expression ? has type Fun

Opening modules in a where clause provides shorter names,
but the values are still not sufficiently in scope to be improved
by a rewrite - this will not refine:

compose2 : (R1 R2 : Fun) → Fun.B R1 ≡ Fun.A R2 → Fun
compose2 R1 R2 eq = record { A = A; B = C; f = fg }
  where
    open Fun R1
    open Fun R2 renaming (A to B1 ; B to C; f to g)
    fg : A → C
    fg rewrite eq = {! g ∘ f !}

It seems the only option is to explicitly repeat every record
field the definition wishes to use in an with-clause to bring it into
the local scope, so it can be refined:

compose3 : (R1 R2 : Fun) → Fun.B R1 ≡ Fun.A R2 → Fun
compose3 R1 R2 eq with Fun.f R1 | Fun.f R2
... | f | g rewrite eq = record { f = g ∘ f }

Overhead scaling with the number of times a field is mentioned
is unacceptable. Fortunately, I realized I can put the casting
in a module (I expect this is where someone is going to point out that
it's already generated automatically, or at least demonstrated a few times
in the standard library):

module CastFun (r : Fun){A' : Set}(cdom : Fun.A r ≡ A')
                        {B' : Set}(ccod : Fun.B r ≡ B') where
  A : Set
  A = A'

  B : Set
  B = B'

  f : A → B
  f with Fun.f r
  f | f' rewrite cdom | ccod = f'

This allows a record to be opened under equalities

compose4 : (R1 R2 : Fun) → Fun.B R1 ≡ Fun.A R2 → Fun
compose4 R1 R2 match = record { f = g ∘ f }
  where
    open CastFun R1 refl match
    open Fun R2 hiding (A) renaming (B to C; f to g)

I'll see how well this works for the full program.

Brandon