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


metadata block
see also:
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.