@@ -2,31 +2,201 @@ 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+-- Sets equipped with a single binary operation that is associative. Must
8+-- satisfy the following laws:
9+-- Associativity of <+>:
10+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
811class Semigroup a where
9− (<.>) : a -> a -> a
12+ (<+>) : a -> a -> a
1013
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
14+-- Sets equipped with a single binary operation that is associative, along with
15+-- a neutral element for that binary operation. Must satisfy the following
16+-- laws:
17+-- Associativity of <+>:
18+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
19+-- Neutral for <+>:
20+-- forall a, a <+> neutral == a
21+-- forall a, neutral <+> a == a
1522class Semigroup a => Monoid a where
1623 neutral : a
1724
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
25+-- Sets equipped with a single binary operation that is associative, along with
26+-- a neutral element for that binary operation and inverses for all elements.
27+-- Must satisfy the following laws:
28+-- Associativity of <+>:
29+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
30+-- Neutral for <+>:
31+-- forall a, a <+> neutral == a
32+-- forall a, neutral <+> a == a
33+-- Inverse for <+>:
34+-- forall a, a <+> inverse a == neutral
35+-- forall a, inverse a <+> a == neutral
2536class Monoid a => Group a where
2637 inverse : a -> a
27− (<->) : a -> a -> a
2838
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
39+(<->) : (Group a) => a -> a -> a
40+(<->) left right = left <+> (inverse right)
41+
42+-- Sets equipped with a single binary operation that is associative and
43+-- commutative, along with a neutral element for that binary operation and
44+-- inverses for all elements. Must satisfy the following laws:
45+-- Associativity of <+>:
46+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
47+-- Commutativity of <+>:
48+-- forall a b, a <+> b == b <+> a
49+-- Neutral for <+>:
50+-- forall a, a <+> neutral == a
51+-- forall a, neutral <+> a == a
52+-- Inverse for <+>:
53+-- forall a, a <+> inverse a == neutral
54+-- forall a, inverse a <+> a == neutral
55+class Group a => AbelianGroup a where { }
56+
57+-- Sets equipped with two binary operations, one associative and commutative
58+-- supplied with a neutral element, and the other associative, with
59+-- distributivity laws relating the two operations. Must satisfy the following
60+-- laws:
61+-- Associativity of <+>:
62+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
63+-- Commutativity of <+>:
64+-- forall a b, a <+> b == b <+> a
65+-- Neutral for <+>:
66+-- forall a, a <+> neutral == a
67+-- forall a, neutral <+> a == a
68+-- Inverse for <+>:
69+-- forall a, a <+> inverse a == neutral
70+-- forall a, inverse a <+> a == neutral
71+-- Associativity of <*>:
72+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
73+-- Distributivity of <*> and <->:
74+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
75+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
76+class AbelianGroup a => Ring a where
77+ (<*>) : a -> a -> a
78+
79+-- Sets equipped with two binary operations, one associative and commutative
80+-- supplied with a neutral element, and the other associative supplied with a
81+-- neutral element, with distributivity laws relating the two operations. Must
82+-- satisfy the following laws:
83+-- Associativity of <+>:
84+-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
85+-- Commutativity of <+>:
86+-- forall a b, a <+> b == b <+> a
87+-- Neutral for <+>:
88+-- forall a, a <+> neutral == a
89+-- forall a, neutral <+> a == a
90+-- Inverse for <+>:
91+-- forall a, a <+> inverse a == neutral
92+-- forall a, inverse a <+> a == neutral
93+-- Associativity of <*>:
94+-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
95+-- Neutral for <*>:
96+-- forall a, a <*> unity == a
97+-- forall a, unity <*> a == a
98+-- Distributivity of <*> and <->:
99+-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
100+-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
101+class Ring a => RingWithUnity a where
102+ unity : a
103+
104+-- Sets equipped with a binary operation that is commutative, associative and
105+-- idempotent. Must satisfy the following laws:
106+-- Associativity of join:
107+-- forall a b c, join a (join b c) == join (join a b) c
108+-- Commutativity of join:
109+-- forall a b, join a b == join b a
110+-- Idempotency of join:
111+-- forall a, join a a == a
112+-- Join semilattices capture the notion of sets with a "least upper bound".
113+class JoinSemilattice a where
114+ join : a -> a -> a
115+
116+-- Sets equipped with a binary operation that is commutative, associative and
117+-- idempotent. Must satisfy the following laws:
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+-- Meet semilattices capture the notion of sets with a "greatest lower bound".
125+class MeetSemilattice a where
126+ meet : a -> a -> a
127+
128+-- Sets equipped with a binary operation that is commutative, associative and
129+-- idempotent and supplied with a neutral element. Must satisfy the following
130+-- laws:
131+-- Associativity of join:
132+-- forall a b c, join a (join b c) == join (join a b) c
133+-- Commutativity of join:
134+-- forall a b, join a b == join b a
135+-- Idempotency of join:
136+-- forall a, join a a == a
137+-- Neutral for join:
138+-- forall a, join a bottom == bottom
139+-- Join semilattices capture the notion of sets with a "least upper bound"
140+-- equipped with a "bottom" element.
141+class JoinSemilattice a => BoundedJoinSemilattice a where
142+ bottom : a
143+
144+-- Sets equipped with a binary operation that is commutative, associative and
145+-- idempotent and supplied with a neutral element. Must satisfy the following
146+-- laws:
147+-- Associativity of meet:
148+-- forall a b c, meet a (meet b c) == meet (meet a b) c
149+-- Commutativity of meet:
150+-- forall a b, meet a b == meet b a
151+-- Idempotency of meet:
152+-- forall a, meet a a == a
153+-- Neutral for meet:
154+-- forall a, meet a top == top
155+-- Meet semilattices capture the notion of sets with a "greatest lower bound"
156+-- equipped with a "top" element.
157+class MeetSemilattice a => BoundedMeetSemilattice a where
158+ top : a
159+
160+-- Sets equipped with two binary operations that are both commutative,
161+-- associative and idempotent, along with absorbtion laws for relating the two
162+-- binary operations. Must satisfy the following:
163+-- Associativity of meet and join:
164+-- forall a b c, meet a (meet b c) == meet (meet a b) c
165+-- forall a b c, join a (join b c) == join (join a b) c
166+-- Commutativity of meet and join:
167+-- forall a b, meet a b == meet b a
168+-- forall a b, join a b == join b a
169+-- Idempotency of meet and join:
170+-- forall a, meet a a == a
171+-- forall a, join a a == a
172+-- Absorbtion laws for meet and join:
173+-- forall a b, meet a (join a b) == a
174+-- forall a b, join a (meet a b) == a
175+class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
176+
177+-- Sets equipped with two binary operations that are both commutative,
178+-- associative and idempotent and supplied with neutral elements, along with
179+-- absorbtion laws for relating the two binary operations. Must satisfy the
180+-- following:
181+-- Associativity of meet and join:
182+-- forall a b c, meet a (meet b c) == meet (meet a b) c
183+-- forall a b c, join a (join b c) == join (join a b) c
184+-- Commutativity of meet and join:
185+-- forall a b, meet a b == meet b a
186+-- forall a b, join a b == join b a
187+-- Idempotency of meet and join:
188+-- forall a, meet a a == a
189+-- forall a, join a a == a
190+-- Absorbtion laws for meet and join:
191+-- forall a b, meet a (join a b) == a
192+-- forall a b, join a (meet a b) == a
193+-- Neutral for meet and join:
194+-- forall a, meet a top == top
195+-- forall a, join a bottom == bottom
196+class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
197+
198+-- XXX todo:
199+-- Fields and vector spaces.
200+-- Structures where "abs" make sense.
201+-- Euclidean domains, etc.
202+-- Where to put fromInteger and fromRational?