module Control.Algebra.Lattice import Control.Algebra import Data.Heap ||| 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 instance JoinSemilattice Nat where join = maximum instance Ord a => JoinSemilattice (MaxiphobicHeap a) where join = merge ||| 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 instance MeetSemilattice Nat where meet = minimum ||| Sets equipped with a binary operation that is commutative, associative and ||| idempotent and supplied with a unitary 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 (Unitary Element): ||| forall a, join a bottom == a ||| ||| 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 instance BoundedJoinSemilattice Nat where bottom = Z ||| Sets equipped with a binary operation that is commutative, associative and ||| idempotent and supplied with a unitary 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 (Unitary Element): ||| forall a, meet a top == a ||| ||| 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 ||| 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 { } instance Lattice Nat where { } ||| 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 { }