[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

[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