[Agda] instance arguments proposal and crash

[Paolo Capriotti]

On Tue, Mar 5, 2013 at 8:35 AM, Dominique Devriese
<dominique.devriese at gmail.com> wrote:
> Hi all,
>
> 2013/3/4 Paolo Capriotti <p.capriotti at gmail.com>:
>> I'm currently experimenting with ways to squeeze as much overloading as possible
>> out of Agda's instance arguments. My simplified use case looks something like
>> this:
>>
>>     record IsMonoid (M : Set) : Set where
>>       field
>>         unit : M
>>         _*_ : M → M → M
>>
>>     record IsGroup (M : Set) : Set where
>>       field
>>         is-mon : IsMonoid M
>>         inv : M → M
>>
>>     record Monoid : Set₁ where
>>       field
>>         carrier : Set
>>         is-mon : IsMonoid carrier
>>
>>     record Group : Set₁ where
>>       field
>>         carrier : Set
>>         is-grp : IsGroup carrier
>>
>> Now, I want to be able to define a function like:
>>
>>     f : (M : Monoid)(G : Group)
>>       → Monoid.carrier M × Monoid.carrier G
>>
>> by simply writing
>>
>>     f M G = unit , unit
>>
>> without any qualification on unit. This is particularly important for infix
>> operators, because qualifying them is horrible, and always renaming them is
>> error prone, confusing and unmaintainable.
>
> I agree that this should work.
>
>> So, my idea is to define a record for "supertypes" of Monoid:
>> ...
>
> However, I want to propose an alternative idea to achieve it.  I think
> we can build on the recent eta-expansion of implicit argument patterns
> of records. This eta-expansion is a feature that was recently
> introduced (I think by Andreas); if we write for example
>
>   g : {M : Set} {is-mon: IsMonoid M} -> T -> ...
>   g _ = ...
>
> Then Agda will insert implicit patterns for M and is-mon in the definition:
>
>  g {_M} {_is-mon} _ = ...
>
> Next, because is-mon is a record it will (since recently) eta-expand
> the _is-mon pattern to
>
>  g {_M} {record { unit = _u, _*_=_times }} _ = ...
>
> There are still some problems with this, however:
> * the expansion does not happen if there is no real argument before
> the equals sign (because of the changes made for issue 655?)
> * the record eta-expansion is annoying if we want to use instance
> arguments on the right-hand side, because after the eta-expansion
> there is no value of the record type in scope any more. Issue 777
> contains a patch that solves this by instead translating to an
> (internal) as-pattern like this:
>     g {_M} {_is-mon@(record { unit = _u, _*_ = _times })}
>   but the as-patterns introduce extra let-bindings in the RHS, which
> trigger an unrelated problem if used together with coinduction (see
> discussion for issue 777).
>
> Anyway, my proposal for Paolo's problem would be to introduce a new
> form of record open command that recursively eta-expands the record in
> the same way as the implicit record patterns and brings in scope its
> contents as let-bindings:
>
> f M G = unit , unit
>   where open IsMonoid {{...}}
>              open recursively Monoid M
>              open recursively Group G

This would already be a huge improvement over what is currently
achievable, but it would still require an explicit declaration for
every object we want to be included in the instance search, whereas if
we had the "combined" instance search that I described, opening
MonoidInterface in my example would make every function in IsMonoid
resolve its argument for all groups and monoids in scope.

I think this combined search is actually pretty powerful, and I
suspect you can encode complex type class patterns like functional
dependencies with it. Also, it doesn't seem like a big change from the
current system, at least in principle. I'm not very familiar with
Agda's internals, so I'm not sure how hard it would be to implement
(we would probably also need a syntax to enable it).

> This is very useful, can you please report it as a bug on the Agda
> issue tracker?  It seems at first sight unrelated to the rest of the
> discussion.
>

Sure, http://code.google.com/p/agda/issues/detail?id=814.

BR,
Paolo