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:
- Static types which can correspond to mathematical types.
- Dependant Types
- A large library on mathematical structures has been implemented.
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:
- SPAD does not conform to modern expectations and so has a steep learning curve.
- Pattern matching is unpredictable for users.
- Problems with type system, for example difficult to implement higher order types (kinds), so cant implement category theoretic structures such as monads.
- Uses a non-standard parser, this means that error message are not very helpful.
- Low level code is written in Lisp, this causes a number of problems, for example it is not possible to write parallel code.
- Proofs are not implemented and messy code would make that difficult.
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:
- Hard to notate variables, expressions and equations.
- Assignment uses '=' instead of ':=' which means that '=' cant be used for equations.
- No way to output REPL session to formats such as MathML, LaTeX, etc.
The current algebra library is very minimal and the notation is non-standard:
- Complex numbers written 1 :+ 2 rather than 1 + i 2
- Matrix columns do not line up
