[Agda] making a pair explodes

[Sergei Meshveliani]

On Mon, 2017-04-17 at 16:04 +0200, Andrea Vezzosi wrote:
> 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?
> 

_,_  is of Standard.

But may be your question refers to something else. 
For any occasion, I add:  

_,_  is used here in 
                  rR∣? = (rR , _∣r?_)  

And this pair has type    CommutativeRing-with∣? α (α ⊔ α=).
And the latter defined as 

  CommutativeRing-with∣? :  ∀ (α α= : Level) → Set (suc (α ⊔ α=))
  CommutativeRing-with∣? α α= =
                              ∃ \ (R : CommutativeRing α α=) →
                                  let M = CommutativeRing.*magma R
                                  in  Decidable₂ (Magma._∣_ M)
 
-- commutative ring with a decidable division relation.



> 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
> >>
> >
> >
>