The Coq mailing list

[mechvel AT scico.botik.ru]

I tried an example with the direct product of many domains.
It fails to "break" the Agda type checker
(Development of March 5, 2020).
This was

---------------------------------------------------------
R₀ = (ℕₛ ×ₛ (ℤₛ ×ₛ (ℕₛ ×ₛ (ℕᵇₛ ×ₛ (ℤᵇₛ ×ₛ ℚₛ))))) ×ₛ ℚₛ
R = R₀ ×ₛ R₀

open Semiring R using (Carrier; _≈_; refl; 1#; *-monoid)
open Monoid-theory   *-monoid using (_^_)
open Semiring-theory R        using (sum; fromℕ)

res : Carrier
res = (sum (1# ∷ 1# ∷ [])) ^ 3

theorem : res ≈ fromℕ 8
theorem = refl {res}
---------------------------------------------------------

It uses the semirings of
ℕ, ℤ, ℕᵇ (binary natural), ℤᵇ (binary integer), ℚₛ (fraction over 
Integer).

This  Test.agda  is type-checked within the same minimum of 1 Gb space
and in almost the same time
(provided that all other needed modules of the applied and standard 
libraries are type-checked)
almost independently on the number of the domains in the expression for 
R₀.

The domains in the direct product are too independent ...

--
Sergei


On 2020-03-06 22:40, 
mechvel AT scico.botik.ru
 wrote:
> Continuing a sub-discussion about the  type check performance,
>
> I add that I have tried now the current Development Agda version
> (March 5, 2020).
>
> I compare it to the last official version of 2.6.0.1
> at a certain BFLib project (Binary Integer + General Fraction 
> arithmetcic).
> This library is may be 5 times smaller than DoCon-A, but it is large
> in comparison to
> usual Agda application practice.
>
> It is applied
>       > time agda $agdaLibOpt BRationalTest.agda  +RTS -M<size> -RTS
>
> (on  ghc-8.8.3, Ubuntu Linux 18.04, 3 GHz personal computer)
>
> which type-checks everything in the given memory space.
> Development Agda type-checks it in the minimum of  1400 Mb memory,
> it is about 1.5 times less space eager and 20% faster.
>
> This gives a certain hope, assuming that 2.6.0.1 probably wins
> something relatively to
> the versions of 2017.
> This needs testing and effort in upgrading DoCon-A.
>
> Regards,
>
> ------
> Sergei
>
>
>
> On 2020-03-04 20:07, 
> mechvel AT scico.botik.ru
>  wrote:
> > On 2020-03-04 14:22, 
> > mechvel AT scico.botik.ru
> >  wrote:
> > > On 2020-03-04 02:04, Jason Gross wrote:
> > > > I'm confused by this.  Are you saying that in Agda typechecking is
> > > > exponential in the number of files?  Or exponential in the number of
> > > > nested abstractions?  Or something else?  Do you have a toy example
> > > > demonstrating this behavior?
> > >
> > > No toy example, so far, but I think such can be provided.
> > >
> > > I have a real-world example of the DoCon-A library for algebra:
> > >
> > >   http://www.botik.ru/pub/local/Mechveliani/docon-A/2.02/
> > >
> > > This is a small part of the intended general purpose library for 
> > > algebra
> > > (for algebra methods, it is very small, but comparing to the Agda
> > > practice, it is large).
> > >
> > > It is written in  install.txt
> > > "for the  -M15G  key  (15 Gb heap) installation takes about 50 
> > > minutes on a
> > >  3 GHz personal computer.
> > > "
> >
> >
> > I am sorry.
> >
> > I need to add the following.
> > This as about the Agda versions of about  2017.
> >
> > It may occur that the current Agda version improves something there.
> > This needs testing, needs more effort in porting the library.
> > I use the last Agda versions, but on certain smaller projects.
>
> _______________________________________________
> Agda mailing list
> Agda AT lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda