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

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

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