# Using Expressions in Idris

I am experimenting with using the Idris language to implement algebra and proofs in mathematical code. Algebra requires expressions with variables in the mathematical sense. To experiment with this I have started implementing this code.

The code is here.

Below is an example session in REPL showing how to use the code.

 ```Type checking ./quaternion.idr λΠ> :let a = ExpFld 3.0 defined λΠ> :let b = Var "b" defined λΠ> a+b ExpFld 3.0 + Var "b" : ExpressionField λΠ> ```

 ```Type checking ./quaternion.idr λΠ> :let w = Var "w" defined λΠ> :let x = Var "x" defined λΠ> :let y = Var "y" defined λΠ> :let z = Var "z" defined λΠ> :let q = w + i x + j y + k z Can't disambiguate name: contrib.Data.Algebra.+, Prelude.Interfaces.+, contrib.Data.Algebra.fld.+, contrib.Data.Algebra.quatOps.+, contrib.Data.Algebra.scalarOpsLeft.+, contrib.Data.Algebra.scalarOpsRight.+ λΠ> :let q = w + i x + j y defined λΠ> :let q = q + k z defined λΠ> q Quat (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0) (Var "x" + ExpFld 0.0 + ExpFld 0.0) (ExpFld 0.0 + Var "y" + ExpFld 0.0) (ExpFld 0.0 + ExpFld 0.0 + Var "z") : Quaternion ExpressionField λΠ> :let m = quaternion2Matrix q defined λΠ> m [[ExpFld 1.0 - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")), ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) - (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)), ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0))], [ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)), ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")), ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") - (Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0))], [ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") - (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)), ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") + (Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)), ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0))]] : Vect 3 (Vect 3 ExpressionField) λΠ> matrix2Quaternion m Quat (Function "sqrt" [ExpFld 1.0 - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z"))) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0))) + ExpFld 1.0] / ExpFld 2.0) ((ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") + (Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)) - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") - (Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0))) / (Function "sqrt" [ExpFld 1.0 - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z"))) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0))) + ExpFld 1.0] / ExpFld 2.0 * ExpFld 4.0)) ((ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)) - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + ExpFld 0.0 + Var "z") - (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0))) / (Function "sqrt" [ExpFld 1.0 - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z"))) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0))) + ExpFld 1.0] / ExpFld 2.0 * ExpFld 4.0)) ((ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0)) - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) - (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (Var "w" + ExpFld 0.0 + ExpFld 0.0 + ExpFld 0.0))) / (Function "sqrt" [ExpFld 1.0 - ExpFld 2.0 * ((ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z")) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + ExpFld 0.0 + Var "z") * (ExpFld 0.0 + ExpFld 0.0 + Var "z"))) + (ExpFld 1.0 - ExpFld 2.0 * ((Var "x" + ExpFld 0.0 + ExpFld 0.0) * (Var "x" + ExpFld 0.0 + ExpFld 0.0) + (ExpFld 0.0 + Var "y" + ExpFld 0.0) * (ExpFld 0.0 + Var "y" + ExpFld 0.0))) + ExpFld 1.0] / ExpFld 2.0 * ExpFld 4.0)) : Quaternion ExpressionField λΠ> ```

### The 'Well-Typed Interpreter' Example

In order to implement this better I looked at the 'Well-Typed Interpreter' example from here: http://docs.idris-lang.org/en/latest/tutorial/interp.html