Algebra in Idris

I am interested in implementing algebra and proofs in computer code. I would like to do this using static types in such a way that each mathematical structure is implemented as a computer type.

I am experimenting with using the Idris language to do this. As a test I have attempted to implement quaternions in the Idris code here. (more information about this code here with example session)

Upto now my favorite environment for implementing algebra is Axiom (and a fork of this: FriCAS) these projects use a language called SPAD this has the basic structure that I want:

However Axiom / FriCAS are not ideal, when it was written SPAD was far ahead of its time but modern languages are finally now catching up and implementing these things in a more consistent way, Some of the issues with SPAD are:

I am therefore experimenting with Idris, however I am finding some problems in implementing this stuff in Idris, although Idris has the kind of structure that I want there are problems when it comes to the user interface (input/output). I think it is really important that mathematical structures are represented using a notation that mathematians can recognise (both in REPL and compiler). Some of these issues are:

The current algebra library is very minimal and the notation is non-standard:

metadata block
see also:

pages on this site

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Type-Driven Development with Idris


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.