[Agda] Avoiding implicit argument proliferation?

[Nils Anders Danielsson]

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.

In order to enable experiments with such features I have implemented
Randy's encoding and added it to the standard library [*]:

   http://www.cse.chalmers.se/~nad/listings/lib/Record.html
   http://www.cse.chalmers.se/~nad/listings/lib/README.Record.html

For instance (taking an example from Randy's paper), we can define a
signature for PERs as follows:

   PER : Signature _
   PER = ∅ , "S"     ∶ (λ _ → Set)
           , "R"     ∶ (λ r → r · "S" → r · "S" → Set)
           , "sym"   ∶ (λ r → Lift (Symmetric (r · "R")))
           , "trans" ∶ (λ r → Lift (Transitive (r · "R")))

We can then state that the converse relation is a PER as follows:

   converse : (P : Record PER) →
              Record (PER With "S" ≔ (λ _ → P · "S")
                          With "R" ≔ (λ _ → flip (P · "R")))

Randy implemented his encoding in Lego, and seemed to encounter some
efficiency problems. Unfortunately it appears as if we get similar
problems in Agda, but at least we have something to play with.

[*] For this piece of code I wanted to allow records in (certain) mutual
blocks.

-- 
/NAD