[Agda] Identifying inefficiency

[Martin Escardo]

Thanks for sharing this, which should be very useful.

However, I think at some point a more principled solution will be 
needed. I am now struggling with time issues dealing with "Sigma". Very 
often eta for Sigma is really useful to have to get short proofs. But 
also very often I enter a time black hole, and while I think I have 
enough experience to deal with it, I end up spending more time 
"optimizing" the proof than coming up with the mathematical meat of a proof.

I don't have a specific proposal, but here is a remark regarding 
"helping Agda". Very often, mathematicians, when writing papers or 
books, give hints to the reader, and sometimes these hints are not 
needed, but they do help the reader to understand the material more 
quickly.

For example, a mathematician when writing the definition of a 
homomorphism as f(x + y) = f x + f y may quickly add that "addition on 
the left refers to the group A, whereas addition on the right it refers 
to the group B".

Similarly, it should be useful to have all sorts of hints to help Agda 
with (fast) type checking. The idea would be that we write Agda 
definitions just as we do now, but we may add, before or after writing a 
term, annotations indicating what should (not) be attempted when trying 
to type check it, how to resolve ambiguities, how much to (not) expand 
definitional equalities.

It is illuminating to read well written mathematical papers that 
actively help the readers to digest the material. Sometimes we will need 
to help Agda to digest our code, too, if we don't want to wait too long 
until it says "I understand now".

And I bet that hints that help Agda to understand our code will also 
help human readers to understand it

Best,
Martin

On 09/04/2019 15:42, sanzhiyan at gmail.com wrote:
> 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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe