diff --git a/Algebra/Enumerable.hs b/Algebra/Enumerable.hs
--- a/Algebra/Enumerable.hs
+++ b/Algebra/Enumerable.hs
@@ -8,7 +8,7 @@
 -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
 --
 ----------------------------------------------------------------------------
-module Algebra.Enumerable (
+module Algebra.Enumerable {-# DEPRECATED "Use Data.Universe.Class" #-} (
     Enumerable(..), universeBounded,
     Enumerated(..)
   ) where
diff --git a/Algebra/Lattice.hs b/Algebra/Lattice.hs
--- a/Algebra/Lattice.hs
+++ b/Algebra/Lattice.hs
@@ -1,5 +1,10 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709
+{-# OPTIONS_GHC -fno-warn-amp #-}
+#endif
 ----------------------------------------------------------------------------
 -- |
 -- Module      :  Algebra.Lattice
@@ -13,7 +18,7 @@
 -- or @join@) and a unique infimum (also called a greatest lower bound or
 -- @meet@).
 --
--- In this module lattices are defined using `meet` and `join` operators,
+-- In this module lattices are defined using 'meet' and 'join' operators,
 -- as it's constructive one.
 --
 ----------------------------------------------------------------------------
@@ -26,90 +31,115 @@
     BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice,
     joins, meets,
 
+    -- * Monoid wrappers
+    Meet(..), Join(..),
+
     -- * Fixed points of chains in lattices
     lfp, lfpFrom, unsafeLfp,
     gfp, gfpFrom, unsafeGfp,
   ) where
 
-import Algebra.Enumerable
 import qualified Algebra.PartialOrd as PO
 
-import qualified Data.Set as S
+import           Data.Universe.Class
+
+#if MIN_VERSION_base(4,8,0)
+#else
+import           Data.Foldable (Foldable, foldMap)
+#endif
+
+import           Data.Proxy
+import           Data.Semigroup
+import           Data.Tagged
+import           Data.Void
+
+import qualified Data.IntMap as IM
 import qualified Data.IntSet as IS
 import qualified Data.Map as M
-import qualified Data.IntMap as IM
+import qualified Data.Set as S
 
-import Data.Hashable
+import           Data.Hashable
 import qualified Data.HashSet as HS
 import qualified Data.HashMap.Lazy as HM
 
+import           Data.Data
+
+infixr 6 /\ -- This comment needed because of CPP
+infixr 5 \/
+
 -- | A algebraic structure with element joins: <http://en.wikipedia.org/wiki/Semilattice>
 --
--- @
--- Associativity: x `join` (y `join` z) == (x `join` y) `join` z
--- Commutativity: x `join` y == y `join` x
--- Idempotency:   x `join` x == x
--- @
+-- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z
+-- > Commutativity: x \/ y == y \/ x
+-- > Idempotency:   x \/ x == x
 class JoinSemiLattice a where
+    (\/) :: a -> a -> a
+    (\/) = join
+
     join :: a -> a -> a
+    join = (\/)
 
+#if __GLASGOW_HASKELL__ >= 709
+    {-# MINIMAL (\/) | join #-}
+#endif
+
 -- | The partial ordering induced by the join-semilattice structure
 joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool
-joinLeq x y = x `join` y == y
+joinLeq x y = (x \/ y) == y
 
 -- | The join of at a list of join-semilattice elements (of length at least one)
 joins1 :: JoinSemiLattice a => [a] -> a
-joins1 = foldr1 join
+joins1 = foldr1 (\/)
 
 -- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>
 --
--- @
--- Associativity: x `meet` (y `meet` z) == (x `meet` y) `meet` z
--- Commutativity: x `meet` y == y `meet` x
--- Idempotency:   x `meet` x == x
--- @
+-- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z
+-- > Commutativity: x /\ y == y /\ x
+-- > Idempotency:   x /\ x == x
 class MeetSemiLattice a where
+    (/\) :: a -> a -> a
+    (/\) = meet
+
     meet :: a -> a -> a
+    meet = (/\)
 
+#if __GLASGOW_HASKELL__ >= 709
+    {-# MINIMAL (/\) | meet #-}
+#endif
+
 -- | The partial ordering induced by the meet-semilattice structure
 meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool
-meetLeq x y = x `meet` y == x
+meetLeq x y = (x /\ y) == x
 
 -- | The meet of at a list of meet-semilattice elements (of length at least one)
 meets1 :: MeetSemiLattice a => [a] -> a
-meets1 = foldr1 meet
+meets1 = foldr1 (/\)
 
 -- | The combination of two semi lattices makes a lattice if the absorption law holds:
 -- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>
 --
--- @
--- Absorption: a `join` (a `meet` b) == a `meet` (a `join` b) == a
--- @
+-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a
 class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where
 
--- | A join-semilattice with some element |bottom| that `join` approaches.
+-- | A join-semilattice with some element |bottom| that \/ approaches.
 --
--- @
--- Identity: x `join` bottom == x
--- @
+-- > Identity: x \/ bottom == x
 class JoinSemiLattice a => BoundedJoinSemiLattice a where
     bottom :: a
 
 -- | The join of a list of join-semilattice elements
-joins :: BoundedJoinSemiLattice a => [a] -> a
-joins = foldr join bottom
+joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a
+joins = getJoin . foldMap Join
 
--- | A meet-semilattice with some element |top| that `meet` approaches.
+-- | A meet-semilattice with some element |top| that /\ approaches.
 --
--- @
--- Identity: x `meet` top == x
--- @
+-- > Identity: x /\ top == x
 class MeetSemiLattice a => BoundedMeetSemiLattice a where
     top :: a
 
 -- | The meet of a list of meet-semilattice elements
-meets :: BoundedMeetSemiLattice a => [a] -> a
-meets = foldr meet top
+meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a
+meets = getMeet . foldMap Meet
 
 
 -- | Lattices with both bounds
@@ -121,27 +151,27 @@
 --
 
 instance Ord a => JoinSemiLattice (S.Set a) where
-    join = S.union
+    (\/) = S.union
 
-instance (Ord a, Enumerable a) => MeetSemiLattice (S.Set (Enumerated a)) where
-    meet = S.intersection
+instance Ord a => MeetSemiLattice (S.Set a) where
+    (/\) = S.intersection
 
-instance (Ord a, Enumerable a) => Lattice (S.Set (Enumerated a)) where
+instance Ord a => Lattice (S.Set a) where
 
 instance Ord a => BoundedJoinSemiLattice (S.Set a) where
     bottom = S.empty
 
-instance (Ord a, Enumerable a) => BoundedMeetSemiLattice (S.Set (Enumerated a)) where
-    top = S.fromList universe
+instance (Ord a, Finite a) => BoundedMeetSemiLattice (S.Set a) where
+    top = S.fromList universeF
 
-instance (Ord a, Enumerable a) => BoundedLattice (S.Set (Enumerated a)) where
+instance (Ord a, Finite a) => BoundedLattice (S.Set a) where
 
 --
 -- IntSets
 --
 
 instance JoinSemiLattice IS.IntSet where
-    join = IS.union
+    (\/) = IS.union
 
 instance BoundedJoinSemiLattice IS.IntSet where
     bottom = IS.empty
@@ -151,10 +181,10 @@
 --
 
 instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where
-    join = HS.union
+    (\/) = HS.union
 
 instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where
-    meet = HS.intersection
+    (/\) = HS.intersection
 
 instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where
     bottom = HS.empty
@@ -164,27 +194,27 @@
 --
 
 instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where
-    join = M.unionWith join
+    (\/) = M.unionWith (\/)
 
-instance (Ord k, Enumerable k, MeetSemiLattice v) => MeetSemiLattice (M.Map (Enumerated k) v) where
-    meet = M.intersectionWith meet
+instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where
+    (/\) = M.intersectionWith (/\)
 
-instance (Ord k, Enumerable k, Lattice v) => Lattice (M.Map (Enumerated k) v) where
+instance (Ord k, Lattice v) => Lattice (M.Map k v) where
 
 instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where
     bottom = M.empty
 
-instance (Ord k, Enumerable k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map (Enumerated k) v) where
-    top = M.fromList (universe `zip` repeat top)
+instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map k v) where
+    top = M.fromList (universeF `zip` repeat top)
 
-instance (Ord k, Enumerable k, BoundedLattice v) => BoundedLattice (M.Map (Enumerated k) v) where
+instance (Ord k, Finite k, BoundedLattice v) => BoundedLattice (M.Map k v) where
 
 --
 -- IntMaps
 --
 
 instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where
-    join = IM.unionWith join
+    (\/) = IM.unionWith (\/)
 
 instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where
     bottom = IM.empty
@@ -194,10 +224,10 @@
 --
 
 instance (Eq k, Hashable k) => JoinSemiLattice (HM.HashMap k v) where
-    join = HM.union
+    (\/) = HM.union
 
 instance (Eq k, Hashable k) => MeetSemiLattice (HM.HashMap k v) where
-    meet = HM.intersection
+    (/\) = HM.intersection
 
 instance (Eq k, Hashable k) => BoundedJoinSemiLattice (HM.HashMap k v) where
     bottom = HM.empty
@@ -207,10 +237,10 @@
 --
 
 instance JoinSemiLattice v => JoinSemiLattice (k -> v) where
-    f `join` g = \x -> f x `join` g x
+    f \/ g = \x -> f x \/ g x
 
 instance MeetSemiLattice v => MeetSemiLattice (k -> v) where
-    f `meet` g = \x -> f x `meet` g x
+    f /\ g = \x -> f x /\ g x
 
 instance Lattice v => Lattice (k -> v) where
 
@@ -222,15 +252,31 @@
 
 instance BoundedLattice v => BoundedLattice (k -> v) where
 
+-- Unit
+instance JoinSemiLattice () where
+  _ \/ _ = ()
+
+instance BoundedJoinSemiLattice () where
+  bottom = ()
+
+instance MeetSemiLattice () where
+  _ /\ _ = ()
+
+instance BoundedMeetSemiLattice () where
+  top = ()
+
+instance Lattice () where
+instance BoundedLattice () where
+
 --
 -- Tuples
 --
 
 instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where
-    (x1, y1) `join` (x2, y2) = (x1 `join` x2, y1 `join` y2)
+    (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2)
 
 instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where
-    (x1, y1) `meet` (x2, y2) = (x1 `meet` x2, y1 `meet` y2)
+    (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2)
 
 instance (Lattice a, Lattice b) => Lattice (a, b) where
 
@@ -247,10 +293,10 @@
 --
 
 instance JoinSemiLattice Bool where
-    join = (||)
+    (\/) = (||)
 
 instance MeetSemiLattice Bool where
-    meet = (&&)
+    (/\) = (&&)
 
 instance Lattice Bool where
 
@@ -262,7 +308,119 @@
 
 instance BoundedLattice Bool where
 
+--- Monoids
 
+-- | Monoid wrapper for JoinSemiLattice
+newtype Join a = Join { getJoin :: a }
+  deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data)
+
+instance JoinSemiLattice a => Semigroup (Join a) where
+  Join a <> Join b = Join (a \/ b)
+
+instance BoundedJoinSemiLattice a => Monoid (Join a) where
+  mempty = Join bottom
+  Join a `mappend` Join b = Join (a \/ b)
+
+-- | Monoid wrapper for MeetSemiLattice
+newtype Meet a = Meet { getMeet :: a }
+  deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data)
+
+instance MeetSemiLattice a => Semigroup (Meet a) where
+  Meet a <> Meet b = Meet (a /\ b)
+
+instance BoundedMeetSemiLattice a => Monoid (Meet a) where
+  mempty = Meet top
+  Meet a `mappend` Meet b = Meet (a /\ b)
+
+-- All
+instance JoinSemiLattice All where
+  All a \/ All b = All $ a \/ b
+
+instance BoundedJoinSemiLattice All where
+  bottom = All False
+
+instance MeetSemiLattice All where
+  All a /\ All b = All $ a /\ b
+
+instance BoundedMeetSemiLattice All where
+  top = All True
+
+instance Lattice All where
+instance BoundedLattice All where
+
+-- Any
+instance JoinSemiLattice Any where
+  Any a \/ Any b = Any $ a \/ b
+
+instance BoundedJoinSemiLattice Any where
+  bottom = Any False
+
+instance MeetSemiLattice Any where
+  Any a /\ Any b = Any $ a /\ b
+
+instance BoundedMeetSemiLattice Any where
+  top = Any True
+
+instance Lattice Any where
+instance BoundedLattice Any where
+
+-- Endo
+instance JoinSemiLattice a => JoinSemiLattice (Endo a) where
+  Endo a \/ Endo b = Endo $ a \/ b
+
+instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where
+  bottom = Endo bottom
+
+instance MeetSemiLattice a => MeetSemiLattice (Endo a) where
+  Endo a /\ Endo b = Endo $ a /\ b
+
+instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where
+  top = Endo top
+
+instance Lattice a => Lattice (Endo a) where
+instance BoundedLattice a => BoundedLattice (Endo a) where
+
+-- Tagged
+instance JoinSemiLattice a => JoinSemiLattice (Tagged t a) where
+  Tagged a \/ Tagged b = Tagged $ a \/ b
+
+instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where
+  bottom = Tagged bottom
+
+instance MeetSemiLattice a => MeetSemiLattice (Tagged t a) where
+  Tagged a /\ Tagged b = Tagged $ a /\ b
+
+instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where
+  top = Tagged top
+
+instance Lattice a => Lattice (Tagged t a) where
+instance BoundedLattice a => BoundedLattice (Tagged t a) where
+
+-- Proxy
+instance JoinSemiLattice (Proxy a) where
+  _ \/ _ = Proxy
+
+instance BoundedJoinSemiLattice (Proxy a) where
+  bottom = Proxy
+
+instance MeetSemiLattice (Proxy a) where
+  _ /\ _ = Proxy
+
+instance BoundedMeetSemiLattice (Proxy a) where
+  top = Proxy
+
+instance Lattice (Proxy a) where
+instance BoundedLattice (Proxy a) where
+
+-- Void
+instance JoinSemiLattice Void where
+  a \/ _ = a
+
+instance MeetSemiLattice Void where
+  a /\ _ = a
+
+instance Lattice Void where
+
 -- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
 -- Assumes that the function is monotone and does not check if that is correct.
 {-# INLINE unsafeLfp #-}
@@ -279,7 +437,7 @@
 -- Forces the function to be monotone.
 {-# INLINE lfpFrom #-}
 lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
-lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x `join` x)
+lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x)
 
 
 -- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
@@ -298,4 +456,4 @@
 -- Forces the function to be antinone.
 {-# INLINE gfpFrom #-}
 gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
-gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x `meet` x)
+gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x)
diff --git a/Algebra/Lattice/Dropped.hs b/Algebra/Lattice/Dropped.hs
--- a/Algebra/Lattice/Dropped.hs
+++ b/Algebra/Lattice/Dropped.hs
@@ -4,7 +4,11 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+#if __GLASGOW_HASKELL__ < 709
 {-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
 ----------------------------------------------------------------------------
 -- |
 -- Module      :  Algebra.Lattice.Dropped
@@ -16,6 +20,7 @@
 ----------------------------------------------------------------------------
 module Algebra.Lattice.Dropped (
     Dropped(..)
+  , retractDropped
   ) where
 
 #ifndef MIN_VERSION_base
@@ -26,13 +31,14 @@
 
 #if MIN_VERSION_base(4,8,0)
 #else
+import Control.Applicative
 import Data.Monoid (Monoid(..))
 import Data.Foldable
 import Data.Traversable
 #endif
 
-import Control.Applicative
 import Control.DeepSeq
+import Control.Monad
 import Data.Data
 import Data.Hashable
 import GHC.Generics
@@ -63,6 +69,15 @@
   traverse _ Top      = pure Top
   traverse f (Drop a) = Drop <$> f a
 
+instance Applicative Dropped where
+  pure = return
+  (<*>) = ap
+
+instance Monad Dropped where
+  return        = Drop
+  Top >>= _     = Top
+  Drop x >>= f  = f x
+
 instance NFData a => NFData (Dropped a) where
   rnf Top      = ()
   rnf (Drop a) = rnf a
@@ -70,14 +85,14 @@
 instance Hashable a => Hashable (Dropped a)
 
 instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where
-    Top    `join` _      = Top
-    _      `join` Top    = Top
-    Drop x `join` Drop y = Drop (x `join` y)
+    Top    \/ _      = Top
+    _      \/ Top    = Top
+    Drop x \/ Drop y = Drop (x \/ y)
 
 instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where
-    Top    `meet` drop_y = drop_y
-    drop_x `meet` Top    = drop_x
-    Drop x `meet` Drop y = Drop (x `meet` y)
+    Top    /\ drop_y = drop_y
+    drop_x /\ Top    = drop_x
+    Drop x /\ Drop y = Drop (x /\ y)
 
 instance Lattice a => Lattice (Dropped a) where
 
@@ -88,3 +103,8 @@
     top = Top
 
 instance BoundedLattice a => BoundedLattice (Dropped a) where
+
+-- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@.
+retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a
+retractDropped Top       = top
+retractDropped (Drop x)  = x
diff --git a/Algebra/Lattice/Levitated.hs b/Algebra/Lattice/Levitated.hs
--- a/Algebra/Lattice/Levitated.hs
+++ b/Algebra/Lattice/Levitated.hs
@@ -4,7 +4,11 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+#if __GLASGOW_HASKELL__ < 709
 {-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
 ----------------------------------------------------------------------------
 -- |
 -- Module      :  Algebra.Lattice.Levitated
@@ -16,6 +20,7 @@
 ----------------------------------------------------------------------------
 module Algebra.Lattice.Levitated (
     Levitated(..)
+  , retractLevitated
   ) where
 
 #ifndef MIN_VERSION_base
@@ -26,13 +31,14 @@
 
 #if MIN_VERSION_base(4,8,0)
 #else
+import Control.Applicative
 import Data.Monoid (Monoid(..))
 import Data.Foldable
 import Data.Traversable
 #endif
 
-import Control.Applicative
 import Control.DeepSeq
+import Control.Monad
 import Data.Data
 import Data.Hashable
 import GHC.Generics
@@ -67,6 +73,16 @@
   traverse _ Top          = pure Top
   traverse f (Levitate a) = Levitate <$> f a
 
+instance Applicative Levitated where
+  pure = return
+  (<*>) = ap
+
+instance Monad Levitated where
+  return            = Levitate
+  Top >>= _         = Top
+  Bottom >>= _      = Bottom
+  Levitate x >>= f  = f x
+
 instance NFData a => NFData (Levitated a) where
   rnf Top          = ()
   rnf Bottom       = ()
@@ -75,18 +91,18 @@
 instance Hashable a => Hashable (Levitated a)
 
 instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where
-    Top        `join` _          = Top
-    _          `join` Top        = Top
-    Levitate x `join` Levitate y = Levitate (x `join` y)
-    Bottom     `join` lev_y      = lev_y
-    lev_x      `join` Bottom     = lev_x
+    Top        \/ _          = Top
+    _          \/ Top        = Top
+    Levitate x \/ Levitate y = Levitate (x \/ y)
+    Bottom     \/ lev_y      = lev_y
+    lev_x      \/ Bottom     = lev_x
 
 instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where
-    Top        `meet` lev_y      = lev_y
-    lev_x      `meet` Top        = lev_x
-    Levitate x `meet` Levitate y = Levitate (x `meet` y)
-    Bottom     `meet` _          = Bottom
-    _          `meet` Bottom     = Bottom
+    Top        /\ lev_y      = lev_y
+    lev_x      /\ Top        = lev_x
+    Levitate x /\ Levitate y = Levitate (x /\ y)
+    Bottom     /\ _          = Bottom
+    _          /\ Bottom     = Bottom
 
 instance Lattice a => Lattice (Levitated a) where
 
@@ -97,3 +113,9 @@
     top = Top
 
 instance Lattice a => BoundedLattice (Levitated a) where
+
+-- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@.
+retractLevitated :: BoundedLattice a => Levitated a -> a
+retractLevitated Top           = top
+retractLevitated Bottom        = bottom
+retractLevitated (Levitate x)  = x
diff --git a/Algebra/Lattice/Lifted.hs b/Algebra/Lattice/Lifted.hs
--- a/Algebra/Lattice/Lifted.hs
+++ b/Algebra/Lattice/Lifted.hs
@@ -3,7 +3,11 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
+#if __GLASGOW_HASKELL__ < 709
 {-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
 ----------------------------------------------------------------------------
 -- |
 -- Module      :  Algebra.Lattice.Lifted
@@ -15,6 +19,7 @@
 ----------------------------------------------------------------------------
 module Algebra.Lattice.Lifted (
     Lifted(..)
+  , retractLifted
   ) where
 
 #ifndef MIN_VERSION_base
@@ -25,13 +30,14 @@
 
 #if MIN_VERSION_base(4,8,0)
 #else
+import Control.Applicative
 import Data.Monoid (Monoid(..))
 import Data.Foldable
 import Data.Traversable
 #endif
 
-import Control.Applicative
 import Control.DeepSeq
+import Control.Monad
 import Data.Data
 import Data.Hashable
 import GHC.Generics
@@ -62,6 +68,15 @@
   traverse _ Bottom   = pure Bottom
   traverse f (Lift a) = Lift <$> f a
 
+instance Applicative Lifted where
+  pure = return
+  (<*>) = ap
+
+instance Monad Lifted where
+  return        = Lift
+  Bottom >>= _  = Bottom
+  Lift x >>= f  = f x
+
 instance NFData a => NFData (Lifted a) where
   rnf Bottom   = ()
   rnf (Lift a) = rnf a
@@ -69,14 +84,14 @@
 instance Hashable a => Hashable (Lifted a)
 
 instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where
-    Lift x `join` Lift y = Lift (x `join` y)
-    Bottom `join` lift_y = lift_y
-    lift_x `join` Bottom = lift_x
+    Lift x \/ Lift y = Lift (x \/ y)
+    Bottom \/ lift_y = lift_y
+    lift_x \/ Bottom = lift_x
 
 instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where
-    Lift x `meet` Lift y = Lift (x `meet` y)
-    Bottom `meet` _      = Bottom
-    _      `meet` Bottom = Bottom
+    Lift x /\ Lift y = Lift (x /\ y)
+    Bottom /\ _      = Bottom
+    _      /\ Bottom = Bottom
 
 instance Lattice a => Lattice (Lifted a) where
 
@@ -87,3 +102,8 @@
     top = Lift top
 
 instance BoundedLattice a => BoundedLattice (Lifted a) where
+
+-- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@.
+retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a
+retractLifted Bottom    = bottom
+retractLifted (Lift x)  = x
diff --git a/Algebra/PartialOrd.hs b/Algebra/PartialOrd.hs
--- a/Algebra/PartialOrd.hs
+++ b/Algebra/PartialOrd.hs
@@ -18,7 +18,8 @@
     gfpFrom, unsafeGfpFrom
   ) where
 
-import Algebra.Enumerable
+import           Data.Universe.Class (Finite(..))
+import           Data.Universe.Instances.Eq ()
 
 import qualified Data.Set as S
 import qualified Data.IntSet as IS
@@ -28,7 +29,7 @@
 
 -- | A partial ordering on sets: <http://en.wikipedia.org/wiki/Partially_ordered_set>
 --
--- This can be defined using either |joinLeq| or |meetLeq|, or a more efficient definition
+-- This can be defined using either 'joinLeq' or 'meetLeq', or a more efficient definition
 -- can be derived directly.
 --
 -- @
@@ -37,7 +38,7 @@
 -- Transitive:    a `leq` b && b `leq` c ==> a `leq` c
 -- @
 --
--- The superclass equality (which can be defined using |partialOrdEq|) must obey these laws:
+-- The superclass equality (which can be defined using 'partialOrdEq') must obey these laws:
 --
 -- @
 -- Reflexive:  a == a
@@ -63,11 +64,8 @@
 instance PartialOrd v => PartialOrd (IM.IntMap v) where
     im1 `leq` im2 = im1 `IM.isSubmapOf` im2 && IM.fold (\(x1, x2) b -> b && x1 `leq` x2) True (IM.intersectionWith (,) im1 im2)
 
-instance (Eq v, Enumerable k) => Eq (k -> v) where
-    f == g = all (\k -> f k == g k) universe
-
-instance (PartialOrd v, Enumerable k) => PartialOrd (k -> v) where
-    f `leq` g = all (\k -> f k `leq` g k) universe
+instance (PartialOrd v, Finite k) => PartialOrd (k -> v) where
+    f `leq` g = all (\k -> f k `leq` g k) universeF
 
 instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
     -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,12 @@
+# 1.4 (2015-09-19)
+
+- Infix operators
+- `meets` and `joins` generalised to work on any `Foldable`
+- Deprecate `Algebra.Enumerable`, use [universe package](http://hackage.haskell.org/package/universe)
+- Add `Applicative` and `Monad` typeclasses to `Dropped`, `Lifted` and `Levitated`
+- Add `Semigroup` instance to `Join` and `Meet`
+- Add instances for `()`, `Proxy`, `Tagged` and `Void`
+
 # 1.3 (2015-05-18)
 
 - relaxed constraint for `BoundedLattice (Levitated a)`
diff --git a/lattices.cabal b/lattices.cabal
--- a/lattices.cabal
+++ b/lattices.cabal
@@ -1,5 +1,5 @@
 name:               lattices
-version:            1.3
+version:            1.4
 cabal-version:      >= 1.10
 category:           Math
 license:            BSD3
@@ -11,6 +11,7 @@
 copyright:          (C) 2010-2015 Maximilian Bolingbroke
 build-type:         Simple
 extra-source-files: README.md CHANGELOG.md
+tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.2
 synopsis:           Fine-grained library for constructing and manipulating lattices
 description:
   In mathematics, a lattice is a partially ordered set in which every two elements have a unique supremum (also called a least upper bound or @join@) and a unique infimum (also called a greatest lower bound or @meet@).
@@ -27,13 +28,31 @@
                     Algebra.Lattice.Lifted,
                     Algebra.PartialOrd
 
-  build-depends:    base >= 3 && < 5,
-                    containers >= 0.3 && < 0.6,
-                    deepseq >= 1.1 && < 1.5,
-                    hashable >= 1.2 && < 1.3,
-                    unordered-containers >= 0.2  && < 0.3
+  build-depends:    base                       >= 4.5  && < 4.9,
+                    containers                 >= 0.3  && < 0.6,
+                    deepseq                    >= 1.1  && < 1.5,
+                    hashable                   >= 1.2  && < 1.3,
+                    semigroups                 >= 0.16 && < 0.18,
+                    tagged                     >= 0.7  && < 0.8,
+                    void                       >= 0.7  && < 0.8,
+                    unordered-containers       >= 0.2  && < 0.3,
+                    universe-base              >= 1.0  && < 1.1,
+                    universe-reverse-instances >= 1.0  && < 1.1
   ghc-options:      -Wall
   default-language: Haskell2010
 
   if impl(ghc >= 7.4 && < 7.5)
     build-depends:  ghc-prim
+
+test-suite test
+  type:                exitcode-stdio-1.0
+  main-is:             Tests.hs
+  hs-source-dirs:      test
+  ghc-options:         -Wall
+  default-language:    Haskell2010
+  build-depends:       base              >= 4.5  && < 4.9,
+                       tasty             >= 0.10 && < 0.12,
+                       tasty-quickcheck  >= 0.8  && < 0.9,
+                       lattices,
+                       transformers,
+                       QuickCheck
diff --git a/test/Tests.hs b/test/Tests.hs
new file mode 100644
--- /dev/null
+++ b/test/Tests.hs
@@ -0,0 +1,146 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE KindSignatures #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Main (main) where
+
+#if MIN_VERSION_base(4,8,0)
+#else
+import Control.Applicative
+import Data.Foldable
+#endif
+
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Monoid
+import Data.Traversable
+import Control.Monad (ap)
+import Test.QuickCheck.Function
+import Test.Tasty
+import Test.Tasty.QuickCheck as QC
+
+import qualified Algebra.Lattice.Dropped as D
+import qualified Algebra.Lattice.Lifted as U
+import qualified Algebra.Lattice.Levitated as L
+
+-- For old GHC to work
+data Proxy1 (a :: * -> *) = Proxy1
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests" [theseProps]
+
+theseProps :: TestTree
+theseProps = testGroup "These"
+  [ functorLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
+  , functorLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
+  , functorLaws "Leviated" (Proxy1 :: Proxy1 L.Levitated)
+  , traversableLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
+  , traversableLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
+  , traversableLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)
+  , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
+  , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
+  , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)
+  ]
+
+functorLaws :: forall (f :: * -> *). ( Functor f
+                                     , Arbitrary (f Int)
+                                     , Eq (f Int)
+                                     , Show (f Int))
+            => String
+            -> Proxy1 f
+            -> TestTree
+functorLaws name _ = testGroup ("Functor laws: " <> name)
+  [ QC.testProperty "identity" identityProp
+  , QC.testProperty "composition" compositionProp
+  ]
+  where
+    identityProp :: f Int -> Property
+    identityProp x = fmap id x === x
+
+    compositionProp :: f Int -> Fun Int Int -> Fun Int Int -> Property
+    compositionProp x (Fun _ f) (Fun _ g) = fmap g (fmap f x) === fmap (g . f) x
+
+traversableLaws :: forall (t :: * -> *). ( Traversable t
+                                         , Arbitrary (t Int)
+                                         , Eq (t Int)
+                                         , Show (t Int))
+                => String
+                -> Proxy1 t
+                -> TestTree
+traversableLaws name _ = testGroup ("Traversable laws: " <> name)
+  [ QC.testProperty "identity" identityProp
+  , QC.testProperty "composition" compositionProp
+  , QC.testProperty "functor" functorProp
+  , QC.testProperty "foldable" foldableProp
+  ]
+  where
+    identityProp :: t Int -> Property
+    identityProp x = traverse Identity x === Identity x
+
+    compositionProp :: t Int -> Fun Int (Maybe Int) -> Fun Int ([] Int) -> Property
+    compositionProp x (Fun _ f) (Fun _ g) = traverse (Compose . fmap g . f) x === (Compose . fmap (traverse g) . traverse f $ x)
+
+    functorProp :: t Int -> Fun Int Int -> Property
+    functorProp x (Fun _ f) = fmap f x === fmapDefault f x
+
+    foldableProp :: t Int -> Fun Int [Int] -> Property
+    foldableProp x (Fun _ f) = foldMap f x === foldMapDefault f x
+
+monadLaws :: forall (m :: * -> *). ( Monad m
+#if !MIN_VERSION_base(4, 8, 0)
+                                   , Applicative m
+#endif
+                                   , Arbitrary (m Int)
+                                   , Eq (m Int)
+                                   , Show (m Int)
+                                   , Arbitrary (m (Fun Int Int))
+                                   , Show (m (Fun Int Int)))
+          => String
+          -> Proxy1 m
+          -> TestTree
+monadLaws name _ = testGroup ("Monad laws: " <> name)
+  [ QC.testProperty "left identity" leftIdentityProp
+  , QC.testProperty "right identity" rightIdentityProp
+  , QC.testProperty "composition" compositionProp
+  , QC.testProperty "Applicative pure" pureProp
+  , QC.testProperty "Applicative ap" apProp
+  ]
+  where
+    leftIdentityProp :: Int -> Fun Int (m Int) -> Property
+    leftIdentityProp x (Fun _ k) = (return x >>= k) === k x
+
+    rightIdentityProp :: m Int -> Property
+    rightIdentityProp m = (m >>= return) === m
+
+    compositionProp :: m Int -> Fun Int (m Int) -> Fun Int (m Int) -> Property
+    compositionProp m (Fun _ k) (Fun _ h) = (m >>= (\x -> k x >>= h)) === ((m >>= k) >>= h)
+
+    pureProp :: Int -> Property
+    pureProp x = pure x === (return x :: m Int)
+
+    apProp :: m (Fun Int Int) -> m Int -> Property
+    apProp f x = (f' <*> x) === ap f' x
+       where f' = apply <$> f
+
+
+-- Orphan instances
+
+instance Arbitrary a => Arbitrary (D.Dropped a) where
+  arbitrary = frequency [ (1, pure D.Top)
+                        , (9, D.Drop <$> arbitrary)
+                        ]
+
+instance Arbitrary a => Arbitrary (U.Lifted a) where
+  arbitrary = frequency [ (1, pure U.Bottom)
+                        , (9, U.Lift <$> arbitrary)
+                        ]
+
+instance Arbitrary a => Arbitrary (L.Levitated a) where
+  arbitrary = frequency [ (1, pure L.Top)
+                        , (1, pure L.Bottom)
+                        , (9, L.Levitate <$> arbitrary)
+                        ]