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:~>
|
