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

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Type-Driven Development with Idris

 

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

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