[Agda] type check performance

[Ulf Norell]

You should also try to print the types with implicit arguments shown. Types
may look simple to a human but Agda has to worry about all the things that
you would leave out of your text book.

You can turns this on with C-c C-x C-h or put {-# OPTIONS --show-implicit
#-} at the top of the file.

/ Ulf

On Thu, Jan 12, 2017 at 7:35 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Wed, 2017-01-11 at 14:21 -0500, Wolfram Kahl wrote:
> > On Wed, Jan 11, 2017 at 09:46:00PM +0300, Sergei Meshveliani wrote:
> > > And my case is different. I define standard classical algebraic
> > > structures: Semigroup, Group, Ring, EuclideanRing, and such, and prove
> > > in Agda certain well-known properties of their operations. There cannot
> > > appear such type expressions like above for  id id ... id.
> > >
> > > And still its type check needs 7Gb RAM and 60 minutes of time (on a 3
> > > GHz computer).
> > >
> > > [...]
> > >
> > > There is something strange in these 60 minutes and 7 Gb minimum.
> > > For example,  EuclideanRing  is far enough in the hierarchy.
> > > And I ask to print the type (C-c C-d)  of the function (lemma)
> > >
> > >   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
> > >
> > > in the module parameterized by an instance of  EuclideanRing.
> > > It shows
> > >
> > > (a b : UpIntegralRing.Carrier upIR) →
> > > (UpIntegralRing.*upMonoid upIR UpMonoid.∣ b) a →
> > > (upIR UpIntegralRing.≈ EuclideanRing.eucRem upIR∣? E a b)
> > > (UpIntegralRing.0# upIR)
> > >
> > > This does not look like a large expression
> > > (though it contains several parts that may need to be replaced with
> > > their expanded definitions, depending on situation).
> >
> > Can you go to the top-level of the file module in which this is defined,
> > and ask for the type  (C-c C-d) of the qualified name of remByDivisor,
> > qualified as necessary to be able to refer to it from the top-level
> > of the file module?
> >
> > And also do that for each of  ∣  ,  eucRem ,  ≈ , and  0# ?
> >
> > If my understanding is correct, then at least in some circumstances
> > and to a certain degree, these are the types that Agda is really dealing
> with.
> >
>
> I have there
>
> --------------------------------------------
> open import Level using (_⊔_)
> ...
> ...
> module OfEuclideanRing {α α=} (upIR∣? : UpIntegralRing-with∣? α α=)
>                  (open OverIntegralRing-0 upIR∣? using (EuclideanRing))
>                  E : EuclideanRing)
>   where
>   upIR = proj₁ upIR∣?
>   _∣?_ = proj₂ upIR∣?
>
>   open UpIntegralRing upIR using
>                            (setoid; ... _≈_;  ... 0#; ... *upMonoid)
>                            renaming (Carrier to C)
>
>   open UpMonoid *upMonoid using (_∣_; _∤_; ∣cong; ... ∣trans)
>                           renaming (∣∙ to ∣*; _~asd_ to _~_)
>   ...
>   open EuclideanRing E using (eucRem; ...)
>   ...
>
>   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
>   ...
> --------------------------------------------
>
> I go to the beginning of this file and command
>
>   C-c C-d
>   remByDivisor
>
> And it prints its type.
> Now, try with the _∣_.
>
> This _∣_ instance is opened from   open UpMonoid *upMonoid,
>
> and  *upMonoid  is opened from  open UpIntegralRing upIR.
>
> What expression need I to put to the   C-c C-d   input window?
> I try
>   let *UM = UpIntegralRing.*upMonoid upIR in UpMonoid._∣_ *UM
>
> It reports
>
> ---------------
> Structures0.DSet.Carrier
> (.Structures0.Magma.dS (Structures0.UpMagma.magma
>   (.Structures0a.UpSemigroup.upMagma
>    (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →
> Structures0.DSet.Carrier
> (.Structures0.Magma.dS (Structures0.UpMagma.magma
>   (.Structures0a.UpSemigroup.upMagma
>    (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →
> Set (α= ⊔ α)
> ------------------
>
> It searches down:
>    UpIntegralRing --> UpMonoid --> UpSemigroup --> UpMagma --> DSet -->
>    Carrier
>
> for each argument in the signature of  _∣_  -- as it was intended.
>
> Further:
>   C-c C-d
>   EuclideanRing.eucRem E
>
> leads to an error:
> ------------------
> (OverIntegralRing-0.EuclideanRing upIR∣?) !=<
> (Data.Product.Σ (UpIntegralRing (_α_0 upIR∣? E) (_α=_1 upIR∣? E))
>  (λ upR → Decidable₂ (Magma._∣_ (UpIntegralRing.*magma upR))))
> of type (Set (α= ⊔ α))
> when checking that the expression E has type
> UpIntegralRing-with∣? (_α_0 upIR∣? E) (_α=_1 upIR∣? E)
> ------------------
>
> E  is a parameter in the head module, and  eucRem  is opened in
> open EuclideanRing E ...
> as shown above.
> I wonder, why does this C-c C-d fail.
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170112/1c81ab40/attachment-0001.html>