Using Quaternions in Idris

I am experimenting with using the Idris language to implement algebra and proofs in mathematical code. As a test I have attempted to implement quaternions in the code here.

To run the REPL I created a shell script file called idris.sh with this contents:
cd Idris-dev/libs/algebra
idris -p effects
This is then run by typing ./idris.sh in the command line:
mjb@linux:~> ./idris.sh

   /  _/___/ /____(_)
   / // __  / ___/ / ___/ Version 1.2.0
 _/ // /_/ / /  / (__  )  http://www.idris-lang.org/
/___/\__,_/_/  /_/____/   Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris>
Or use idris hello.idr to compile code:
$ idris hello.idr
     ____    __     _
   /  _/___/ /____(_)____
   / // __  / ___/ / ___/ Version 1.3.1
 _/ // /_/ / /  / (__  )  http://www.idris-lang.org/
/___/\__,_/_/  /_/____/   Type :? for help

Type checking ./hello.idr

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

Type checking ./quaternion.idr
Quat 1.0 2.0 0.0 0.0 : Quaternion Double
λΠ> :let q1 = 1.0 + i 2.0
defined
λΠ> :let q3 = 1.0 + i 2.0 + j 3.0
defined
λΠ> :let q4 = q3 + k 4.0
defined
λΠ> q4
Quat 1.0 2.0 3.0 4.0 : Quaternion Double
λΠ> :let q5 = normalise q4
defined
λΠ> q5
Quat 0.18257418583505536
     0.3651483716701107
     0.5477225575051661
     0.7302967433402214 : Quaternion Double
λΠ> :let m6 = quaternion2Matrix q5
defined
λΠ> m6
[[-0.6666666666666663, 0.13333333333333336, 0.7333333333333332],
 [0.6666666666666665, -0.33333333333333304, 0.6666666666666666],
 [0.33333333333333326, 0.9333333333333332, 0.13333333333333353]] : Vect 3
                                                                        (Vect 3 Double)
λΠ> matrix2Quaternion m6
Quat 0.18257418583505597
     0.36514837167010944
     0.5477225575051642
     0.7302967433402189 : Quaternion Double
λΠ> 
To leave Idris:
Idris> :q
Bye bye
mjb@linux:~> 

metadata block
see also:
Correspondence about this page

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

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