[Agda] making a pair explodes

[Andrea Vezzosi]

I wouldn't be able to say much about why the type signature made
things much better, it's mostly that I was even surprised the
expression fully typechecked, if it did with no unresolved
constraints, considering that it's hard to infer the type of a pair
constructed like that.

What is the type of _,_ exactly?


On Mon, Apr 17, 2017 at 3:17 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Mon, 2017-04-17 at 13:22 +0200, Andrea Vezzosi wrote:
>> A couple of questions:
>>
>> - Does it help if you provide the type signature for "rR∣?"  ?
>> - What about doing putting the local definitions in a "where" clause
>> rather than a "let"?
>
>
> Great!
> Adding the type signature for rR∣? helps.
> Under 3 Gb heap,  it takes 74 seconds to type-check.
>
> The type check cost reduces probably more than 100 times.
>
> Thank you very much.
>
> I could suspect this effect with the type signature, but I have
> forgotten to try it.
>
> This is indeed a relief.
> Because during last four years this is the main example in my project
> for dependent types in computer algebra. This example was tried two
> years earlier; its type check has failed in the same way.
> Now it is time to revisit it. And it occurs that it is sufficient to add
> a single type signature.
>
> Can you, please, give a hint: how does this occur that without this
> signature the checker spends this much computation?
>
> Further: the whole project needs the minimum of 10 Gb to check, and is
> checked in 64 minutes.
> And it is highly desirable to reduce this to 7 Gb, or even better, to
> 3 Gb.
> And there are many places where I skip type signatures (in order to make
> the code looking shorter).
> Suppose that I add some type signatures to the modules that take most of
> the cost to check. Does this worth trying?
>
> Thanks,
>
> ------
> Sergei
>
>
>> On Mon, Apr 17, 2017 at 1:00 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
>> > Dear Agda developers,
>> >
>> > The following fragment shows a certain remarkable detail:
>> >
>> >   f :  (b : C) → IsPrime b → Domain _ _
>> >   f b prime-b =
>> >               let open ForPrime b prime-b using (rFoo; ...)
>> >                   rIR   = proj₁ rFoo
>> >                   _∣r?_ = proj₂ rFoo
>> >                   rR    = Foo.ring rIR
>> >                   rR∣?  = (rR , _∣r?_)    -- **
>> >               in
>> >               anything
>> >
>> > Here  ForPrime  is a paramtric module,  Foo is a record.
>> > All the needed previous .agda files have been checked earlier,
>> > within about  10 Gb heap and 50 minutes.
>> > And checking this  f  explodes:  for  26 Gb  3 hours is not enough, so I
>> > have interrupted it.
>> >
>> > I set `anything' there in order to see which part of let-in makes the
>> > checker explode.
>> >
>> > And it occurs that commenting out the last line in let-in makes f
>> > checked in a small time:
>> >
>> > Finished Foo
>> > Total                      62,991ms
>> > Miscellaneous                 360ms
>> > Deserialization            53,299ms
>> > Serialization               4,772ms (9,012ms)
>> > Serialization.BinaryEncode  4,072ms
>> > Serialization.Sort             88ms
>> > Serialization.Compress         76ms
>> > Import                        156ms
>> > Typing                         84ms    (88ms)
>> > DeadCode                       60ms
>> > Scoping                        12ms
>> > ModuleName                     12ms
>> >
>> >
>> > So:  rR  and  _∣r?_  are checked in a small time,
>> > while composing them into a pair gives explosion.
>> >
>> > I know about the effect of large terms being substituted into a
>> > parametric module - the effect produced by a certain lack of data
>> > sharing in the type representation.
>> >
>> > But: really only composing this pair must lead to this explosion?
>> > Can you guess and tell what may be happening there?
>> >
>> > I can provide the full code.
>> > But it is large, and needs about 10 Gb heap to type-check.
>> >
>> > Thanks,
>> >
>> > -------
>> > Sergei
>> >
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>