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.

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
λΠ> 

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.