@@ -2,31 +2,206 @@ module prelude.algebra
22
33import builtins
44
5−-- Sets with an associative binary operation
6−-- Must satisfy:
7−-- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c
5+%access public
6+
7+-- XXX: change?
8+infix 6 <->
9+infix 6 <+>
10+infix 6 <*>
11+
12+-- Sets equipped with a single binary operation that is associative. Must
13+-- satisfy the following laws:
14+-- Associativity of <+>:
15+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
816class Semigroup a where
9− (<.>) : a -> a -> a
17+ (<+>) : a -> a -> a
1018
11−-- Sets with an associative binary operation and a neutral element
12−-- Must satisfy:
13−-- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c
14−-- forall a. neutral <*> a = a <*> neutral = a
19+-- Sets equipped with a single binary operation that is associative, along with
20+-- a neutral element for that binary operation. Must satisfy the following
21+-- laws:
22+-- Associativity of <+>:
23+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
24+-- Neutral for <+>:
25+-- forall a, a <+> neutral == a
26+-- forall a, neutral <+> a == a
1527class Semigroup a => Monoid a where
1628 neutral : a
1729
18−-- Sets with an associative binary operation, a neutral element, as well as
19−-- inverses
20−-- Must satisfy:
21−-- forall a, b, c. a <*> (b <*> c) = (a <*> b) <*> c
22−-- forall a. neutral <*> a = a <*> neutral = a
23−-- forall a. inverse a <*> a = a <*> inverse = neutral
24−-- forall a. inverse (inverse a) = a
30+-- Sets equipped with a single binary operation that is associative, along with
31+-- a neutral element for that binary operation and inverses for all elements.
32+-- Must satisfy the following laws:
33+-- Associativity of <+>:
34+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
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
2541class Monoid a => Group a where
2642 inverse : a -> a
27− (<->) : a -> a -> a
2843
29−-- XXX: to add:
30−-- ring, field, euclidean domain, abelian group, vector spaces, etc.?
31−-- do we want proofs of properties in the type classes?
32−-- derived classes, some mechanism for multiple e.g. monoids on same type
44+(<->) : Group a => a -> a -> a
45+(<->) left right = left <+> (inverse right)
46+
47+-- Sets equipped with a single binary operation that is associative and
48+-- commutative, along with a neutral element for that binary operation and
49+-- inverses for all elements. Must satisfy the following laws:
50+-- Associativity of <+>:
51+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
52+-- Commutativity of <+>:
53+-- forall a b, a <+> b == b <+> a
54+-- Neutral for <+>:
55+-- forall a, a <+> neutral == a
56+-- forall a, neutral <+> a == a
57+-- Inverse for <+>:
58+-- forall a, a <+> inverse a == neutral
59+-- forall a, inverse a <+> a == neutral
60+class Group a => AbelianGroup a where { }
61+
62+-- Sets equipped with two binary operations, one associative and commutative
63+-- supplied with a neutral element, and the other associative, with
64+-- distributivity laws relating the two operations. Must satisfy the following
65+-- laws:
66+-- Associativity of <+>:
67+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
68+-- Commutativity of <+>:
69+-- forall a b, a <+> b == b <+> a
70+-- Neutral for <+>:
71+-- forall a, a <+> neutral == a
72+-- forall a, neutral <+> a == a
73+-- Inverse for <+>:
74+-- forall a, a <+> inverse a == neutral
75+-- forall a, inverse a <+> a == neutral
76+-- Associativity of <*>:
77+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
78+-- Distributivity of <*> and <->:
79+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
80+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
81+class AbelianGroup a => Ring a where
82+ (<*>) : a -> a -> a
83+
84+-- Sets equipped with two binary operations, one associative and commutative
85+-- supplied with a neutral element, and the other associative supplied with a
86+-- neutral element, with distributivity laws relating the two operations. Must
87+-- satisfy the following laws:
88+-- Associativity of <+>:
89+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
90+-- Commutativity of <+>:
91+-- forall a b, a <+> b == b <+> a
92+-- Neutral for <+>:
93+-- forall a, a <+> neutral == a
94+-- forall a, neutral <+> a == a
95+-- Inverse for <+>:
96+-- forall a, a <+> inverse a == neutral
97+-- forall a, inverse a <+> a == neutral
98+-- Associativity of <*>:
99+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
100+-- Neutral for <*>:
101+-- forall a, a <*> unity == a
102+-- forall a, unity <*> a == a
103+-- Distributivity of <*> and <->:
104+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
105+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
106+class Ring a => RingWithUnity a where
107+ unity : a
108+
109+-- Sets equipped with a binary operation that is commutative, associative and
110+-- idempotent. Must satisfy the following laws:
111+-- Associativity of join:
112+-- forall a b c, join a (join b c) == join (join a b) c
113+-- Commutativity of join:
114+-- forall a b, join a b == join b a
115+-- Idempotency of join:
116+-- forall a, join a a == a
117+-- Join semilattices capture the notion of sets with a "least upper bound".
118+class JoinSemilattice a where
119+ join : a -> a -> a
120+
121+-- Sets equipped with a binary operation that is commutative, associative and
122+-- idempotent. Must satisfy the following laws:
123+-- Associativity of meet:
124+-- forall a b c, meet a (meet b c) == meet (meet a b) c
125+-- Commutativity of meet:
126+-- forall a b, meet a b == meet b a
127+-- Idempotency of meet:
128+-- forall a, meet a a == a
129+-- Meet semilattices capture the notion of sets with a "greatest lower bound".
130+class MeetSemilattice a where
131+ meet : a -> a -> a
132+
133+-- Sets equipped with a binary operation that is commutative, associative and
134+-- idempotent and supplied with a neutral element. Must satisfy the following
135+-- laws:
136+-- Associativity of join:
137+-- forall a b c, join a (join b c) == join (join a b) c
138+-- Commutativity of join:
139+-- forall a b, join a b == join b a
140+-- Idempotency of join:
141+-- forall a, join a a == a
142+-- Neutral for join:
143+-- forall a, join a bottom == bottom
144+-- Join semilattices capture the notion of sets with a "least upper bound"
145+-- equipped with a "bottom" element.
146+class JoinSemilattice a => BoundedJoinSemilattice a where
147+ bottom : a
148+
149+-- Sets equipped with a binary operation that is commutative, associative and
150+-- idempotent and supplied with a neutral element. Must satisfy the following
151+-- laws:
152+-- Associativity of meet:
153+-- forall a b c, meet a (meet b c) == meet (meet a b) c
154+-- Commutativity of meet:
155+-- forall a b, meet a b == meet b a
156+-- Idempotency of meet:
157+-- forall a, meet a a == a
158+-- Neutral for meet:
159+-- forall a, meet a top == top
160+-- Meet semilattices capture the notion of sets with a "greatest lower bound"
161+-- equipped with a "top" element.
162+class MeetSemilattice a => BoundedMeetSemilattice a where
163+ top : a
164+
165+-- Sets equipped with two binary operations that are both commutative,
166+-- associative and idempotent, along with absorbtion laws for relating the two
167+-- binary operations. Must satisfy the following:
168+-- Associativity of meet and join:
169+-- forall a b c, meet a (meet b c) == meet (meet a b) c
170+-- forall a b c, join a (join b c) == join (join a b) c
171+-- Commutativity of meet and join:
172+-- forall a b, meet a b == meet b a
173+-- forall a b, join a b == join b a
174+-- Idempotency of meet and join:
175+-- forall a, meet a a == a
176+-- forall a, join a a == a
177+-- Absorbtion laws for meet and join:
178+-- forall a b, meet a (join a b) == a
179+-- forall a b, join a (meet a b) == a
180+class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
181+
182+-- Sets equipped with two binary operations that are both commutative,
183+-- associative and idempotent and supplied with neutral elements, along with
184+-- absorbtion laws for relating the two binary operations. Must satisfy the
185+-- following:
186+-- Associativity of meet and join:
187+-- forall a b c, meet a (meet b c) == meet (meet a b) c
188+-- forall a b c, join a (join b c) == join (join a b) c
189+-- Commutativity of meet and join:
190+-- forall a b, meet a b == meet b a
191+-- forall a b, join a b == join b a
192+-- Idempotency of meet and join:
193+-- forall a, meet a a == a
194+-- forall a, join a a == a
195+-- Absorbtion laws for meet and join:
196+-- forall a b, meet a (join a b) == a
197+-- forall a b, join a (meet a b) == a
198+-- Neutral for meet and join:
199+-- forall a, meet a top == top
200+-- forall a, join a bottom == bottom
201+class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
202+
203+-- XXX todo:
204+-- Fields and vector spaces.
205+-- Structures where "abs" make sense.
206+-- Euclidean domains, etc.
207+-- Where to put fromInteger and fromRational?