[Agda] Avoiding implicit argument proliferation?

[Brandon Moore]

> From: Nils Anders Danielsson <nad at chalmers.se>

> Sent: Mon, March 28, 2011 9:57:06 AM
> 
> On 2011-03-25 14:34, Brandon Moore wrote:
> > 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.
> 
> In "Dependently Typed Records  in Type Theory" Randy Pollack claims that
> the use of Pebble-style sharing  (sharing by parametrisation) is
> inconvenient in large-scale developments, and  argues for the use of
> something like "with" (not to be confused with Agda's  with).
> Interestingly he also shows how records with "with" can be encoded  in
> Agda, using induction-recursion.

I read (some of) that paper as well, but didn't think to implement it.
I'll have to try it out, sooner if I run into things I can't handle with the
slightly simplified approach I've worked out in the meantime.

I've found I can avoid manually writing the casting modules as in
my previous message, by alternating parametrized and
non-parametrized records.

A structure is introduced as a parameterized record containing all the
interesting fields.

record FunctorP(C D : Category) : Set where ...

Then to hide indices another record contains just the parameters and
an instance of the parametrized record.

record Functor : Set₁ where
  field
    C D : Category
    F : FunctorP C D

Instead of an casting module which retypes all the fields, it's enough to
provide a casting function which takes the unparametrized record and
some equalities to a correctly parametrized instance of the parametrized
record.

castFunctor : (F : Functor){C D : Category} → Functor.C F ≡ C → Functor.D F ≡ D 
→ FunctorP C D
castFunctor F eqC eqD with Functor.F F; ... | F' rewrite eqC | eqD = F'

The result can be opened with the automatically generated module,
as in

open FunctorP (castFunctor F refl equalityFromContext)

Brandon