git.iko.soy/Idris-dev
on d3fa352 help sign in
Idris-dev/libs/contrib/Control/Algebra/NumericImplementations.idr
114 lines 1.9 kB history raw
1||| Implementations of algebraic interfaces (group, ring, etc) for numeric data types,
2||| and Complex number types.
3module Control.Algebra.NumericImplementations
5import Control.Algebra
6import Control.Algebra.VectorSpace
7import Data.Complex
8import Data.ZZ
10%access public export
12Semigroup Integer where
13 (<+>) = (+)
15Monoid Integer where
16 neutral = 0
18Group Integer where
19 inverse = (* -1)
21AbelianGroup Integer where
23Ring Integer where
24 (<.>) = (*)
26RingWithUnity Integer where
27 unity = 1
30Semigroup Int where
31 (<+>) = (+)
33Monoid Int where
34 neutral = 0
36Group Int where
37 inverse = (* -1)
39AbelianGroup Int where
41Ring Int where
42 (<.>) = (*)
44RingWithUnity Int where
45 unity = 1
48Semigroup Double where
49 (<+>) = (+)
51Monoid Double where
52 neutral = 0
54Group Double where
55 inverse = (* -1)
57AbelianGroup Double where
59Ring Double where
60 (<.>) = (*)
62RingWithUnity Double where
63 unity = 1
65Field Double where
66 inverseM f _ = 1 / f
69Semigroup Nat where
70 (<+>) = (+)
72Monoid Nat where
73 neutral = 0
75Semigroup ZZ where
76 (<+>) = (+)
78Monoid ZZ where
79 neutral = 0
81Group ZZ where
82 inverse = (* -1)
84AbelianGroup ZZ where
86Ring ZZ where
87 (<.>) = (*)
89RingWithUnity ZZ where
90 unity = 1
93Semigroup a => Semigroup (Complex a) where
94 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
96Monoid a => Monoid (Complex a) where
97 neutral = (neutral :+ neutral)
99Group a => Group (Complex a) where
100 inverse (r :+ i) = (inverse r :+ inverse i)
102Ring a => AbelianGroup (Complex a) where {}
104Ring a => Ring (Complex a) where
105 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
107RingWithUnity a => RingWithUnity (Complex a) where
108 unity = (unity :+ neutral)
110RingWithUnity a => Module a (Complex a) where
111 (<#>) x = map (x <.>)
113RingWithUnity a => InnerProductSpace a (Complex a) where
114 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z