[Agda] Identifying inefficiency

[Andrea Vezzosi]

I have found that efficiency problems with algebraic structures can be
mitigated by disabling (definitional) eta rules for such record types
and defining instances by copatterns. (Ulf gave a talk partly on this
at the AIM in Leuven).

I have just now pushed such a change for the isEquiv record used by
the cubical primitives:

https://github.com/agda/agda/commit/13d516f20d5cdf88e35349a2d8ddc52e1c5c2dde

This will make it so an element of isEquiv defined by copatterns will
only be definitionally equal to itself, so things get compared by name
and arguments.
This is similar to what happens with functions defined by standard
pattern matching, when they cannot reduce.

This led to a 16x speedup in one particularly bad example:

https://github.com/agda/agda/commit/13d516f20d5cdf88e35349a2d8ddc52e1c5c2dde

pathToEquiv is defined by copatterns, but now without eta for isEquiv
the typechecker will not try to observe what happens at each
projection.

Then eta can still be proven propositionally by pattern matching on
the record constructor.
(Or in cubical one can define the corresponding path also by copatterns).

Cheers,
Andrea


On Tue, Mar 26, 2019 at 5:50 PM Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
> To be precise, I am not abstracting equivalence composition. I am
> abstracting the proof that the composition of equivalences is an
> equivalence. Martin
>
> On 26/03/2019 16:48, Martin Escardo wrote:
> > It seems that indeed I am.
> >
> > Instead of functors, like you, I am composing equivalences. And I have
> > the composition of three equivalences, twice, with the two possible
> > associations.
> >
> > For the moment, I have solved this by making "abstract" the function
> > that composes two equivalences. This brings down the time from 31s to 3s
> > for the module under discussion.
> >
> > But I will look at the link you gave, as it does seem to be the same
> > kind of situation.
> >
> > Thanks!
> >
> > Martin
> >
> > On 26/03/2019 16:42, kahl at cas.mcmaster.ca wrote:
> >> On Tue, Mar 26, 2019 at 03:33:11PM +0000, Martin Escardo wrote:
> >>> (I tried supplying all the implicit arguments to the RHS's, but the 30s
> >>> time remains the same.  At the holes, the types of the subterms of the
> >>> terms that I want to fill the holes with is known, so I am not sure what
> >>> is going on. But I guess this is a different question from the one in
> >>> this thread.)
> >>
> >> Perhaps you are in the kind of situation that I frequently encounter,
> >> see https://github.com/agda/agda/issues/1625 .
> >>
> >> I haven't tried Andrea's patch at
> >>
> >>    https://github.com/agda/agda/issues/1625#issuecomment-132196576
> >>
> >> in a while, but it worked wonders for some developments that would
> >> otherwise have been impossible to typecheck.
> >>
> >>
> >> Wolfram
> >>
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda