@@ -0,0 +1,274 @@
1+module Control.Algebra
2+
3+import Data.Heap
4+
5+-- XXX: change?
6+infixl 6 <->
7+infixl 6 <.>
8+infixl 5 <#>
9+
10+||| Sets equipped with a single binary operation that is associative, along with
11+||| a neutral element for that binary operation and inverses for all elements.
12+||| Must satisfy the following laws:
13+||| + Associativity of `<+>`:
14+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
15+||| + Neutral for `<+>`:
16+||| forall a, a <+> neutral == a
17+||| forall a, neutral <+> a == a
18+||| + Inverse for `<+>`:
19+||| forall a, a <+> inverse a == neutral
20+||| forall a, inverse a <+> a == neutral
21+class Monoid a => Group a where
22+ inverse : a -> a
23+
24+(<->) : Group a => a -> a -> a
25+(<->) left right = left <+> (inverse right)
26+
27+||| Sets equipped with a single binary operation that is associative and
28+||| commutative, along with a neutral element for that binary operation and
29+||| inverses for all elements. Must satisfy the following laws:
30+|||
31+||| + Associativity of `<+>`:
32+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
33+||| + Commutativity of `<+>`:
34+||| forall a b, a <+> b == b <+> a
35+||| + Neutral for `<+>`:
36+||| forall a, a <+> neutral == a
37+||| forall a, neutral <+> a == a
38+||| + Inverse for `<+>`:
39+||| forall a, a <+> inverse a == neutral
40+||| forall a, inverse a <+> a == neutral
41+class Group a => AbelianGroup a where { }
42+
43+
44+||| Sets equipped with two binary operations, one associative and commutative
45+||| supplied with a neutral element, and the other associative, with
46+||| distributivity laws relating the two operations. Must satisfy the following
47+||| laws:
48+|||
49+||| + Associativity of `<+>`:
50+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
51+||| + Commutativity of `<+>`:
52+||| forall a b, a <+> b == b <+> a
53+||| + Neutral for `<+>`:
54+||| forall a, a <+> neutral == a
55+||| forall a, neutral <+> a == a
56+||| + Inverse for `<+>`:
57+||| forall a, a <+> inverse a == neutral
58+||| forall a, inverse a <+> a == neutral
59+||| + Associativity of `<.>`:
60+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
61+||| + Distributivity of `<.>` and `<->`:
62+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
63+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
64+class AbelianGroup a => Ring a where
65+ (<.>) : a -> a -> a
66+
67+
68+||| Sets equipped with two binary operations, one associative and commutative
69+||| supplied with a neutral element, and the other associative supplied with a
70+||| neutral element, with distributivity laws relating the two operations. Must
71+||| satisfy the following laws:
72+|||
73+||| + Associativity of `<+>`:
74+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
75+||| + Commutativity of `<+>`:
76+||| forall a b, a <+> b == b <+> a
77+||| + Neutral for `<+>`:
78+||| forall a, a <+> neutral == a
79+||| forall a, neutral <+> a == a
80+||| + Inverse for `<+>`:
81+||| forall a, a <+> inverse a == neutral
82+||| forall a, inverse a <+> a == neutral
83+||| + Associativity of `<.>`:
84+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
85+||| + Neutral for `<.>`:
86+||| forall a, a <.> unity == a
87+||| forall a, unity <.> a == a
88+||| + Distributivity of `<.>` and `<->`:
89+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
90+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
91+class Ring a => RingWithUnity a where
92+ unity : a
93+
94+
95+||| Sets equipped with a binary operation that is commutative, associative and
96+||| idempotent. Must satisfy the following laws:
97+|||
98+||| + Associativity of join:
99+||| forall a b c, join a (join b c) == join (join a b) c
100+||| + Commutativity of join:
101+||| forall a b, join a b == join b a
102+||| + Idempotency of join:
103+||| forall a, join a a == a
104+|||
105+||| Join semilattices capture the notion of sets with a "least upper bound".
106+class JoinSemilattice a where
107+ join : a -> a -> a
108+
109+instance JoinSemilattice Nat where
110+ join = maximum
111+
112+instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
113+ join = merge
114+
115+||| Sets equipped with a binary operation that is commutative, associative and
116+||| idempotent. Must satisfy the following laws:
117+|||
118+||| + Associativity of meet:
119+||| forall a b c, meet a (meet b c) == meet (meet a b) c
120+||| + Commutativity of meet:
121+||| forall a b, meet a b == meet b a
122+||| + Idempotency of meet:
123+||| forall a, meet a a == a
124+|||
125+||| Meet semilattices capture the notion of sets with a "greatest lower bound".
126+class MeetSemilattice a where
127+ meet : a -> a -> a
128+
129+instance MeetSemilattice Nat where
130+ meet = minimum
131+
132+
133+||| Sets equipped with a binary operation that is commutative, associative and
134+||| idempotent and supplied with a unitary element. Must satisfy the following
135+||| laws:
136+|||
137+||| + Associativity of join:
138+||| forall a b c, join a (join b c) == join (join a b) c
139+||| + Commutativity of join:
140+||| forall a b, join a b == join b a
141+||| + Idempotency of join:
142+||| forall a, join a a == a
143+||| + Bottom (Unitary Element):
144+||| forall a, join a bottom == a
145+|||
146+||| Join semilattices capture the notion of sets with a "least upper bound"
147+||| equipped with a "bottom" element.
148+class JoinSemilattice a => BoundedJoinSemilattice a where
149+ bottom : a
150+
151+
152+instance BoundedJoinSemilattice Nat where
153+ bottom = Z
154+
155+
156+||| Sets equipped with a binary operation that is commutative, associative and
157+||| idempotent and supplied with a unitary element. Must satisfy the following
158+||| laws:
159+|||
160+||| + Associativity of meet:
161+||| forall a b c, meet a (meet b c) == meet (meet a b) c
162+||| + Commutativity of meet:
163+||| forall a b, meet a b == meet b a
164+||| + Idempotency of meet:
165+||| forall a, meet a a == a
166+||| + Top (Unitary Element):
167+||| forall a, meet a top == a
168+|||
169+||| Meet semilattices capture the notion of sets with a "greatest lower bound"
170+||| equipped with a "top" element.
171+class MeetSemilattice a => BoundedMeetSemilattice a where
172+ top : a
173+
174+
175+
176+||| Sets equipped with two binary operations that are both commutative,
177+||| associative and idempotent, along with absorbtion laws for relating the two
178+||| binary operations. Must satisfy the following:
179+|||
180+||| + Associativity of meet and join:
181+||| forall a b c, meet a (meet b c) == meet (meet a b) c
182+||| forall a b c, join a (join b c) == join (join a b) c
183+||| + Commutativity of meet and join:
184+||| forall a b, meet a b == meet b a
185+||| forall a b, join a b == join b a
186+||| + Idempotency of meet and join:
187+||| forall a, meet a a == a
188+||| forall a, join a a == a
189+||| + Absorbtion laws for meet and join:
190+||| forall a b, meet a (join a b) == a
191+||| forall a b, join a (meet a b) == a
192+class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
193+
194+
195+instance Lattice Nat where { }
196+
197+||| Sets equipped with two binary operations that are both commutative,
198+||| associative and idempotent and supplied with neutral elements, along with
199+||| absorbtion laws for relating the two binary operations. Must satisfy the
200+||| following:
201+|||
202+||| + Associativity of meet and join:
203+||| forall a b c, meet a (meet b c) == meet (meet a b) c
204+||| forall a b c, join a (join b c) == join (join a b) c
205+||| + Commutativity of meet and join:
206+||| forall a b, meet a b == meet b a
207+||| forall a b, join a b == join b a
208+||| + Idempotency of meet and join:
209+||| forall a, meet a a == a
210+||| forall a, join a a == a
211+||| + Absorbtion laws for meet and join:
212+||| forall a b, meet a (join a b) == a
213+||| forall a b, join a (meet a b) == a
214+||| + Neutral for meet and join:
215+||| forall a, meet a top == top
216+||| forall a, join a bottom == bottom
217+class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
218+
219+
220+-- Fields.
221+||| Sets equipped with two binary operations, both associative and commutative
222+||| supplied with a neutral element, with
223+||| distributivity laws relating the two operations. Must satisfy the following
224+||| laws:
225+|||
226+||| + Associativity of `<+>`:
227+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
228+||| + Commutativity of `<+>`:
229+||| forall a b, a <+> b == b <+> a
230+||| + Neutral for `<+>`:
231+||| forall a, a <+> neutral == a
232+||| forall a, neutral <+> a == a
233+||| + Inverse for `<+>`:
234+||| forall a, a <+> inverse a == neutral
235+||| forall a, inverse a <+> a == neutral
236+||| + Associativity of `<.>`:
237+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
238+||| + Unity for `<.>`:
239+||| forall a, a <.> unity == a
240+||| forall a, unity <.> a == a
241+||| + InverseM of `<.>`:
242+||| forall a, a <.> inverseM a == unity
243+||| forall a, inverseM a <.> a == unity
244+||| + Distributivity of `<.>` and `<->`:
245+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
246+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
247+class RingWithUnity a => Field a where
248+ inverseM : a -> a
249+
250+
251+||| A module over a ring is an additive abelian group of 'vectors' endowed with a
252+||| scale operation multiplying vectors by ring elements, and distributivity laws
253+||| relating the scale operation to both ring addition and module addition.
254+||| Must satisfy the following laws:
255+|||
256+||| + Compatibility of scalar multiplication with ring multiplication:
257+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
258+||| + Ring unity is the identity element of scalar multiplication:
259+||| forall v, unity <#> v = v
260+||| + Distributivity of `<#>` and `<+>`:
261+||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
262+||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
263+class (RingWithUnity a, AbelianGroup b) => Module a b where
264+ (<#>) : a -> b -> b
265+
266+
267+||| A vector space is a module over a ring that is also a field
268+class (Field a, Module a b) => VectorSpace a b where {}
269+
270+
271+-- XXX todo:
272+-- Structures where "abs" make sense.
273+-- Euclidean domains, etc.
274+-- Where to put fromInteger and fromRational?