[Agda] agda slow

[Andrea Vezzosi]

Yes, the problem seems to be defining things inline as a lambda, if
you define a function in a where clause and just fill the record field
with it then typechecking goes pretty fast and not consuming much
memory.

I guess the lambda gets always beta-reduced in the type of the
remaining fields, while a defined function will not be unfolded as
much.

Cheers,
Andrea

On Wed, Jun 3, 2015 at 1:47 PM, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> Thank you for your advice. As usual I have jumped to the conclusion too
> quickly. Switching off eta by declaring records to be coinductive doesn’t
> help. :-(
>
> Maybe it is caused by me using a let inside a lambda inside a record?
>
> m : Methods M
> m = record
>       { .. ; _[_]Tᴹ = λ {Γ} {Γᴹ} {Δ} {Δᴹ} {A} Aᴹ {δ} δᴹ →
>       let
>         p : ((A [ δ ]T) [ Pr Γᴹ ]T) [ π₁ {A = A [ δ ]T [ Pr Γᴹ ]T} id ]T ≡
> (A [ Pr Δᴹ ]T) [ =s δᴹ ∘ π₁ id ]T
>         p = obvious
>       in Aᴹ [ =s δᴹ ∘ (π₁ id) , coe (TmΓ= p) (π₂ id) ]T
>
>
>
> The full code is at https://bitbucket.org/akaposi/tt-in-tt in
> TT/LogPredElim.agda
>
> I am happy to do more experiments as soon as I find the time but I’d just
> like to know wether this is related to a known issue.
>
> Thorsten
>
> On 02/06/2015 17:44, "Andrea Vezzosi" <sanzhiyan at gmail.com> wrote:
>
>>One hacky way would be to declare them coinductive, that would disable
>>eta but also pattern matching.
>>
>>record Foo .. : Set where
>>   coinductive
>>   field
>>      bar : ...
>>
>>
>>Best,
>>Andrea
>>
>>
>>On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch
>><Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>> Hi,
>>>
>>> I know that this is a common experience. I was just starting to use some
>>> records to restructure some code we are working on and the memory goes
>>> through the roof. Is there a way to switch off eta expansion of records
>>>or
>>> would this disable type checking of records altogether.
>>>
>>> Cheers,
>>> Thorsten
>>>
>>> This message and any attachment are intended solely for the addressee
>>> and may contain confidential information. If you have received this
>>> message in error, please send it back to me, and immediately delete it.
>>>
>>> Please do not use, copy or disclose the information contained in this
>>> message or in any attachment.  Any views or opinions expressed by the
>>> author of this email do not necessarily reflect the views of the
>>> University of Nottingham.
>>>
>>> This message has been checked for viruses but the contents of an
>>> attachment may still contain software viruses which could damage your
>>> computer system, you are advised to perform your own checks. Email
>>> communications with the University of Nottingham may be monitored as
>>> permitted by UK legislation.
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>