[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Wed, 2013-09-25 at 06:56 +0800, Mianlai ZHOU wrote:
> Hi,
> 
> I have a question regarding this. Is Agda an ideal tool for writing a computer 
> algebra library?


I think, it has a good chance to become such, 
after  1) may be some minor improvements in the Language
2) further development of the prover assistant (as an additional
library).

But this concerns only a _generic_ approach to computer algebra (CA): 
describing various categories and constructs over them, as it is in the
classical 20-th century textbooks on algebra. 
 
> As someone coming from Mathematica background, I am particularly interested 
> in this because in principle languages like Agda *should* be more 
> suitable for computer algebra than any other existing languages.

"any other" sounds too strong. 
For example, there exists the  Coq language and tool,  developed very
far. 
I start studying Agda because I have wrote in Haskell a large CA
library, and Agda is more close to Haskell; this is somehow my current
personal taste.

There also exists the  Aldor  language and tool
(+ Axiom library).
I expect that it is _currently_ the best for writing CA in practice.
It also has dependent types (DT).
But  a) the Algor language is not purely functional,  
b) it does not support _proofs_ (DT provide a certain advantage even
apart of supporting proofs).

If you are coming from the Mathematica background, it has sense first to
study applying Haskell to CA. 

As to Agda, I am studying it and its library (mainly, by practicing)
during 13 months. I have managed to describe a category tower from
DecidableSet to EuclideanRing and Field, and the constructor of
ResidueRing (somewhat 1/2 of it), 
with also providing most of the corresponding proofs.
I like that this is all type-checked.
I need another year-two to see how it will perform in instances, on
examples.

Practical advantages of Agda in CA over real existing CA tools (say,
Haskell or Aldor) can be proved only in perspective, after, say, 10
years.

Because in scientific practice, mathematicians do not care much for
proofs in programs. They mainly need just to compute a concrete result,
say, in about 10 days, in order to partially confirm some hypothesis.
No matter what programming tool is applied.
And the method proofs are provided in papers and in books. Also they do
not care much for formal verification, they prefer understanding an
in-formal proof. Neither do they care much for logic or constructive
logic. They use just  classical mathematics + algorithms.
(And this whole approach is natural, by the way).

As to Agda, I shall be able to give real notes on this language and tool
after doing the next portion of CA. For example, there are some
important possibilities in Standard library which I have never tried and
which may help.

Regards,

------
Sergei


> _______________________________________
> From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Sergei Meshveliani [mechvel at botik.ru]
> Sent: Wednesday, September 25, 2013 1:36 AM
> To: Dmytro Starosud
> Cc: agda at lists.chalmers.se
> Subject: Re: [Agda] stdlib for practical programming
> 
> On Tue, 2013-09-24 at 19:00 +0300, Dmytro Starosud wrote:
> 
> After 1 year experience with writing a computer algebra library in Agda
> I start to think that classes are not needed, that
> dependent records + implicit parameters  of Agda is better.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> This message and any attachment are intended solely for the addressee and may contain confidential information.                        
> If you have received this message in error, please send it back to me, and immediately delete it.                                               
>   
> Please do not use, copy or disclose the information contained in this message or in any attachment.                                        
> 
> Any views or opinions expressed by the author of this email do not necessarily reflect the views of The University of Nottingham Ningbo China.    
> 
>                                                  
> This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks.       
>                                                      
> Email communications with The University of Nottingham Ningbo China may be monitored as permitted by UK and Chinese legislation.         
>