git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/libs/contrib/Control/Algebra/NumericImplementations.idr
134 lines 2.3 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
12-- Integer
14Semigroup Integer where
15 (<+>) = (+)
17Monoid Integer where
18 neutral = 0
20Group Integer where
21 inverse = (* -1)
23AbelianGroup Integer where
25Ring Integer where
26 (<.>) = (*)
28RingWithUnity Integer where
29 unity = 1
31-- Int
33Semigroup Int where
34 (<+>) = (+)
36Monoid Int where
37 neutral = 0
39Group Int where
40 inverse = (* -1)
42AbelianGroup Int where
44Ring Int where
45 (<.>) = (*)
47RingWithUnity Int where
48 unity = 1
50-- Double
52Semigroup Double where
53 (<+>) = (+)
55Monoid Double where
56 neutral = 0
58Group Double where
59 inverse = (* -1)
61AbelianGroup Double where
63Ring Double where
64 (<.>) = (*)
66RingWithUnity Double where
67 unity = 1
69Field Double where
70 inverseM f _ = 1 / f
72-- Nat
74[PlusNatSemi] Semigroup Nat where
75 (<+>) = (+)
77[PlusNatMonoid] Monoid Nat using PlusNatSemi where
78 neutral = 0
80[MultNatSemi] Semigroup Nat where
81 (<+>) = (*)
83[MultNatMonoid] Monoid Nat using MultNatSemi where
84 neutral = 1
86-- ZZ
88[PlusZZSemi] Semigroup ZZ where
89 (<+>) = (+)
91[PlusZZMonoid] Monoid ZZ using PlusZZSemi where
92 neutral = 0
94Group ZZ using PlusZZMonoid where
95 inverse = (* -1)
97AbelianGroup ZZ where
99[MultZZSemi] Semigroup ZZ where
100 (<+>) = (*)
102[MultZZMonoid] Monoid ZZ using MultZZSemi where
103 neutral = 1
105Ring ZZ where
106 (<.>) = (*)
108RingWithUnity ZZ where
109 unity = 1
111-- Complex
113Semigroup a => Semigroup (Complex a) where
114 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
116Monoid a => Monoid (Complex a) where
117 neutral = (neutral :+ neutral)
119Group a => Group (Complex a) where
120 inverse (r :+ i) = (inverse r :+ inverse i)
122Ring a => AbelianGroup (Complex a) where {}
124Ring a => Ring (Complex a) where
125 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
127RingWithUnity a => RingWithUnity (Complex a) where
128 unity = (unity :+ neutral)
130RingWithUnity a => Module a (Complex a) where
131 (<#>) x = map (x <.>)
133RingWithUnity a => InnerProductSpace a (Complex a) where
134 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z