@@ -2,12 +2,16 @@ module prelude.algebra
22
33import builtins
44
5+-- XXX: change?
6+infixl 6 <->
7+infixl 6 <+>
8+infixl 6 <*>
9+
510%access public
611
7−-- XXX: change?
8−infix 6 <->
9−infix 6 <+>
10−infix 6 <*>
12+--------------------------------------------------------------------------------
13+-- A modest class hierarchy
14+--------------------------------------------------------------------------------
1115
1216-- Sets equipped with a single binary operation that is associative. Must
1317-- satisfy the following laws:
@@ -16,6 +20,9 @@ infix 6 <*>
1620class Semigroup a where
1721 (<+>) : a -> a -> a
1822
23+class Semigroup a => VerifiedSemigroup a where
24+ semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
25+
1926-- Sets equipped with a single binary operation that is associative, along with
2027-- a neutral element for that binary operation. Must satisfy the following
2128-- laws:
@@ -27,6 +34,10 @@ class Semigroup a where
2734class Semigroup a => Monoid a where
2835 neutral : a
2936
37+class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38+ monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39+ monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
40+
3041-- Sets equipped with a single binary operation that is associative, along with
3142-- a neutral element for that binary operation and inverses for all elements.
3243-- Must satisfy the following laws:
@@ -41,6 +52,10 @@ class Semigroup a => Monoid a where
4152class Monoid a => Group a where
4253 inverse : a -> a
4354
55+class (VerifiedMonoid a, Group a) => VerifiedGroup a where
56+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
58+
4459(<->) : Group a => a -> a -> a
4560(<->) left right = left <+> (inverse right)
4661
@@ -59,6 +74,9 @@ class Monoid a => Group a where
5974-- forall a, inverse a <+> a == neutral
6075class Group a => AbelianGroup a where { }
6176
77+class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
78+ abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
79+
6280-- Sets equipped with two binary operations, one associative and commutative
6381-- supplied with a neutral element, and the other associative, with
6482-- distributivity laws relating the two operations. Must satisfy the following
@@ -81,6 +99,11 @@ class Group a => AbelianGroup a where { }
8199class AbelianGroup a => Ring a where
82100 (<*>) : a -> a -> a
83101
102+class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
103+ ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104+ ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
106+
84107-- Sets equipped with two binary operations, one associative and commutative
85108-- supplied with a neutral element, and the other associative supplied with a
86109-- neutral element, with distributivity laws relating the two operations. Must
@@ -106,6 +129,10 @@ class AbelianGroup a => Ring a where
106129class Ring a => RingWithUnity a where
107130 unity : a
108131
132+class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
133+ ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134+ ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
135+
109136-- Sets equipped with a binary operation that is commutative, associative and
110137-- idempotent. Must satisfy the following laws:
111138-- Associativity of join:
@@ -118,6 +145,11 @@ class Ring a => RingWithUnity a where
118145class JoinSemilattice a where
119146 join : a -> a -> a
120147
148+class JoinSemilattice a => VerifiedJoinSemilattice a where
149+ joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
150+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
152+
121153-- Sets equipped with a binary operation that is commutative, associative and
122154-- idempotent. Must satisfy the following laws:
123155-- Associativity of meet:
@@ -130,6 +162,11 @@ class JoinSemilattice a where
130162class MeetSemilattice a where
131163 meet : a -> a -> a
132164
165+class MeetSemilattice a => VerifiedMeetSemilattice a where
166+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
169+
133170-- Sets equipped with a binary operation that is commutative, associative and
134171-- idempotent and supplied with a neutral element. Must satisfy the following
135172-- laws:
@@ -139,13 +176,16 @@ class MeetSemilattice a where
139176-- forall a b, join a b == join b a
140177-- Idempotency of join:
141178-- forall a, join a a == a
142−-- Neutral for join:
179+-- Bottom:
143180-- forall a, join a bottom == bottom
144181-- Join semilattices capture the notion of sets with a "least upper bound"
145182-- equipped with a "bottom" element.
146183class JoinSemilattice a => BoundedJoinSemilattice a where
147184 bottom : a
148185
186+class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
187+ boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
188+
149189-- Sets equipped with a binary operation that is commutative, associative and
150190-- idempotent and supplied with a neutral element. Must satisfy the following
151191-- laws:
@@ -155,13 +195,16 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
155195-- forall a b, meet a b == meet b a
156196-- Idempotency of meet:
157197-- forall a, meet a a == a
158−-- Neutral for meet:
198+-- Top:
159199-- forall a, meet a top == top
160200-- Meet semilattices capture the notion of sets with a "greatest lower bound"
161201-- equipped with a "top" element.
162202class MeetSemilattice a => BoundedMeetSemilattice a where
163203 top : a
164204
205+class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
206+ boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
207+
165208-- Sets equipped with two binary operations that are both commutative,
166209-- associative and idempotent, along with absorbtion laws for relating the two
167210-- binary operations. Must satisfy the following:
@@ -179,6 +222,10 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
179222-- forall a b, join a (meet a b) == a
180223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
181224
225+class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
226+ latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227+ latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
228+
182229-- Sets equipped with two binary operations that are both commutative,
183230-- associative and idempotent and supplied with neutral elements, along with
184231-- absorbtion laws for relating the two binary operations. Must satisfy the
@@ -199,6 +246,9 @@ class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
199246-- forall a, meet a top == top
200247-- forall a, join a bottom == bottom
201248class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
249+
250+class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
251+
202252
203253-- XXX todo:
204254-- Fields and vector spaces.