[Agda] instance arguments proposal and crash

[Dominique Devriese]

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 work because the "open recursively" commands would bring in
scope all of the record's (transitive) fields, including their
IsMonoid structures, which are then available to resolve unit's
instance argument.

The "open recursively" commands could perhaps also be used internally
as an alternative to the previously mentioned introduction of record
patterns on the LHS with the same effects.

> Anyway, in one of my earlier attempts at tackling this problem, I stumbled upon
> a crash. Here's the code triggering 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.

Thanks
Dominique