[Agda] Identifying inefficiency
Martin Escardo
m.escardo at cs.bham.ac.uk
Tue Mar 26 17:50:32 CET 2019
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
More information about the Agda
mailing list