module Prelude.Algebra
import Builtins
-- XXX: change?
infixl 6 <->
infixl 6 <+>
infixl 6 <*>
%access public
--------------------------------------------------------------------------------
-- A modest class hierarchy
--------------------------------------------------------------------------------
-- Sets equipped with a single binary operation that is associative. Must
-- satisfy the following laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
class Semigroup a where
(<+>) : a -> a -> a
class Semigroup a => VerifiedSemigroup a where
semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
-- Sets equipped with a single binary operation that is associative, along with
-- a neutral element for that binary operation. Must satisfy the following
-- laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-- Neutral for <+>:
-- forall a, a <+> neutral == a
-- forall a, neutral <+> a == a
class Semigroup a => Monoid a where
neutral : a
class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
-- Sets equipped with a single binary operation that is associative, along with
-- a neutral element for that binary operation and inverses for all elements.
-- Must satisfy the following laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-- Neutral for <+>:
-- forall a, a <+> neutral == a
-- forall a, neutral <+> a == a
-- Inverse for <+>:
-- forall a, a <+> inverse a == neutral
-- forall a, inverse a <+> a == neutral
class Monoid a => Group a where
inverse : a -> a
class (VerifiedMonoid a, Group a) => VerifiedGroup a where
groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
(<->) : Group a => a -> a -> a
(<->) left right = left <+> (inverse right)
-- Sets equipped with a single binary operation that is associative and
-- commutative, along with a neutral element for that binary operation and
-- inverses for all elements. Must satisfy the following laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-- Commutativity of <+>:
-- forall a b, a <+> b == b <+> a
-- Neutral for <+>:
-- forall a, a <+> neutral == a
-- forall a, neutral <+> a == a
-- Inverse for <+>:
-- forall a, a <+> inverse a == neutral
-- forall a, inverse a <+> a == neutral
class Group a => AbelianGroup a where { }
class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
-- Sets equipped with two binary operations, one associative and commutative
-- supplied with a neutral element, and the other associative, with
-- distributivity laws relating the two operations. Must satisfy the following
-- laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-- Commutativity of <+>:
-- forall a b, a <+> b == b <+> a
-- Neutral for <+>:
-- forall a, a <+> neutral == a
-- forall a, neutral <+> a == a
-- Inverse for <+>:
-- forall a, a <+> inverse a == neutral
-- forall a, inverse a <+> a == neutral
-- Associativity of <*>:
-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
-- Distributivity of <*> and <->:
-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
class AbelianGroup a => Ring a where
(<*>) : a -> a -> a
class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
-- Sets equipped with two binary operations, one associative and commutative
-- supplied with a neutral element, and the other associative supplied with a
-- neutral element, with distributivity laws relating the two operations. Must
-- satisfy the following laws:
-- Associativity of <+>:
-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-- Commutativity of <+>:
-- forall a b, a <+> b == b <+> a
-- Neutral for <+>:
-- forall a, a <+> neutral == a
-- forall a, neutral <+> a == a
-- Inverse for <+>:
-- forall a, a <+> inverse a == neutral
-- forall a, inverse a <+> a == neutral
-- Associativity of <*>:
-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
-- Neutral for <*>:
-- forall a, a <*> unity == a
-- forall a, unity <*> a == a
-- Distributivity of <*> and <->:
-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
class Ring a => RingWithUnity a where
unity : a
class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
-- Sets equipped with a binary operation that is commutative, associative and
-- idempotent. Must satisfy the following laws:
-- Associativity of join:
-- forall a b c, join a (join b c) == join (join a b) c
-- Commutativity of join:
-- forall a b, join a b == join b a
-- Idempotency of join:
-- forall a, join a a == a
-- Join semilattices capture the notion of sets with a "least upper bound".
class JoinSemilattice a where
join : a -> a -> a
class JoinSemilattice a => VerifiedJoinSemilattice a where
joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
-- Sets equipped with a binary operation that is commutative, associative and
-- idempotent. Must satisfy the following laws:
-- Associativity of meet:
-- forall a b c, meet a (meet b c) == meet (meet a b) c
-- Commutativity of meet:
-- forall a b, meet a b == meet b a
-- Idempotency of meet:
-- forall a, meet a a == a
-- Meet semilattices capture the notion of sets with a "greatest lower bound".
class MeetSemilattice a where
meet : a -> a -> a
class MeetSemilattice a => VerifiedMeetSemilattice a where
meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
-- Sets equipped with a binary operation that is commutative, associative and
-- idempotent and supplied with a neutral element. Must satisfy the following
-- laws:
-- Associativity of join:
-- forall a b c, join a (join b c) == join (join a b) c
-- Commutativity of join:
-- forall a b, join a b == join b a
-- Idempotency of join:
-- forall a, join a a == a
-- Bottom:
-- forall a, join a bottom == bottom
-- Join semilattices capture the notion of sets with a "least upper bound"
-- equipped with a "bottom" element.
class JoinSemilattice a => BoundedJoinSemilattice a where
bottom : a
class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
-- Sets equipped with a binary operation that is commutative, associative and
-- idempotent and supplied with a neutral element. Must satisfy the following
-- laws:
-- Associativity of meet:
-- forall a b c, meet a (meet b c) == meet (meet a b) c
-- Commutativity of meet:
-- forall a b, meet a b == meet b a
-- Idempotency of meet:
-- forall a, meet a a == a
-- Top:
-- forall a, meet a top == top
-- Meet semilattices capture the notion of sets with a "greatest lower bound"
-- equipped with a "top" element.
class MeetSemilattice a => BoundedMeetSemilattice a where
top : a
class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
-- Sets equipped with two binary operations that are both commutative,
-- associative and idempotent, along with absorbtion laws for relating the two
-- binary operations. Must satisfy the following:
-- Associativity of meet and join:
-- forall a b c, meet a (meet b c) == meet (meet a b) c
-- forall a b c, join a (join b c) == join (join a b) c
-- Commutativity of meet and join:
-- forall a b, meet a b == meet b a
-- forall a b, join a b == join b a
-- Idempotency of meet and join:
-- forall a, meet a a == a
-- forall a, join a a == a
-- Absorbtion laws for meet and join:
-- forall a b, meet a (join a b) == a
-- forall a b, join a (meet a b) == a
class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
-- Sets equipped with two binary operations that are both commutative,
-- associative and idempotent and supplied with neutral elements, along with
-- absorbtion laws for relating the two binary operations. Must satisfy the
-- following:
-- Associativity of meet and join:
-- forall a b c, meet a (meet b c) == meet (meet a b) c
-- forall a b c, join a (join b c) == join (join a b) c
-- Commutativity of meet and join:
-- forall a b, meet a b == meet b a
-- forall a b, join a b == join b a
-- Idempotency of meet and join:
-- forall a, meet a a == a
-- forall a, join a a == a
-- Absorbtion laws for meet and join:
-- forall a b, meet a (join a b) == a
-- forall a b, join a (meet a b) == a
-- Neutral for meet and join:
-- forall a, meet a top == top
-- forall a, join a bottom == bottom
class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
-- XXX todo:
-- Fields and vector spaces.
-- Structures where "abs" make sense.
-- Euclidean domains, etc.
-- Where to put fromInteger and fromRational?