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
