@@ -1,11 +1,8 @@
11module Control.Algebra
22
3−import Data.Heap
4−
5−-- XXX: change?
63infixl 6 <->
74infixl 6 <.>
8−infixl 5 <#>
5+
96
107||| Sets equipped with a single binary operation that is associative, along with
118||| a neutral element for that binary operation and inverses for all elements.
@@ -40,7 +37,6 @@ class Monoid a => Group a where
4037||| forall a, inverse a <+> a == neutral
4138class Group a => AbelianGroup a where { }
4239
43−
4440||| Sets equipped with two binary operations, one associative and commutative
4541||| supplied with a neutral element, and the other associative, with
4642||| distributivity laws relating the two operations. Must satisfy the following
@@ -91,133 +87,6 @@ class AbelianGroup a => Ring a where
9187class Ring a => RingWithUnity a where
9288 unity : a
9389
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.
22190||| Sets equipped with two binary operations, both associative and commutative
22291||| supplied with a neutral element, with
22392||| distributivity laws relating the two operations. Must satisfy the following
@@ -248,26 +117,6 @@ class RingWithUnity a => Field a where
248117 inverseM : a -> a
249118
250119
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−
271120-- XXX todo:
272121-- Structures where "abs" make sense.
273122-- Euclidean domains, etc.