diff --git a/distributors.cabal b/distributors.cabal
index 2794cd4..2ff7396 100644
--- a/distributors.cabal
+++ b/distributors.cabal
@@ -127,6 +127,7 @@ test-suite test
   other-modules:
       Examples.Arithmetic
       Examples.Chain
+      Examples.Expression
       Examples.Json
       Examples.Lambda
       Examples.LenVec
diff --git a/src/Control/Lens/Grammar.hs b/src/Control/Lens/Grammar.hs
index 8ac3779..a47e261 100644
--- a/src/Control/Lens/Grammar.hs
+++ b/src/Control/Lens/Grammar.hs
@@ -66,6 +66,8 @@ import Text.ParserCombinators.ReadP (ReadP, readP_to_S)
 import Witherable
 
 -- Re-exports
+import Control.Lens.Cons as X
+import Control.Lens.Empty as X
 import Control.Lens.Grammar.BackusNaur as X
 import Control.Lens.Grammar.Boole as X
 import Control.Lens.Grammar.Kleene as X
@@ -284,7 +286,7 @@ and generator support for `ruleRec`.
 type Grammar token a = forall p.
   ( Lexical token p
   , Alternator p
-  , forall x. BackusNaurForm (p x x)
+  , forall x y. BackusNaurForm (p x y)
   ) => p a a
 
 {- | For context-sensitivity,
diff --git a/src/Control/Lens/Grammar/Kleene.hs b/src/Control/Lens/Grammar/Kleene.hs
index fe8018a..78a0ae0 100644
--- a/src/Control/Lens/Grammar/Kleene.hs
+++ b/src/Control/Lens/Grammar/Kleene.hs
@@ -47,26 +47,31 @@ import qualified Test.QuickCheck.Gen as Gen
 import Text.ParserCombinators.ReadP (ReadP)
 import qualified Text.ParserCombinators.ReadP as ReadP
 
-{- | A `KleeneStarAlgebra` is a ring
+{- | A `KleeneStarAlgebra` is a semiring
 with a generally non-commutative multiplication,
 the `Monoid` concatenation operator `<>` with identity `mempty`;
 and an idempotent addition, the alternation operator `>|<`
 with identity `zeroK`.
 
-It has three unary operators `optK`, `plusK` and the eponymous `starK`.
-
-prop> starK x = optK (plusK x)
-prop> plusK x = x <> starK x
-prop> optK x = mempty >|< x
-
-The following invariants should hold.
-
 prop> x >|< x = x
 prop> zeroK >|< x = x = x >|< zeroK
-prop> mempty >|< x = optK x = x >|< mempty
 prop> zeroK <> x = zeroK = x <> zeroK
 prop> mempty <> x = x = x <> mempty
 
+It also has three unary Kleene quantifier operators;
+
+* `optK`, zero or one,
+
+prop> optK x = mempty >|< x = x >|< mempty
+
+* `plusK`, one or more,
+
+prop> plusK x = x <> starK x = starK x <> x
+
+* and the eponymous `starK`, zero or more.
+
+prop> starK x = optK (plusK x)
+
 -}
 class Monoid k => KleeneStarAlgebra k where
   starK, plusK, optK :: k -> k
@@ -90,11 +95,9 @@ anyK :: (Foldable f, KleeneStarAlgebra k) => (a -> k) -> f a -> k
 anyK f = foldl' (\b a -> b >|< f a) zeroK
 
 {- | The `RegEx`pression type forms the prototypical `KleeneStarAlgebra`.
-It is also a `TokenAlgebra`, such that the following invariants hold.
-
-prop> zeroK = tokenClass falseB
-prop> tokenClass x >|< tokenClass y = tokenClass (x >||< y)
-
+It is also a `TokenAlgebra` and `tokenClass` acts homomorphically on disjunction.
+`RegEx`pressions may be understood as normalizations of
+`KleeneStarAlgebra` expressions generated by lexical token expressions.
 -}
 data RegEx token
   = SeqEmpty
@@ -105,8 +108,8 @@ data RegEx token
   | KleenePlus (RegEx token)
   | RegExam (RegExam token (RegEx token))
 
-{- | A component of both `RegEx`pressions and `TokenClass`es,
-so that the latter can be embedded in the former with `tokenClass`.
+{- | Both `RegEx`pressions and `TokenClass`es are algebras over the t`RegExam` endo-`Functor`.
+`TokenClass` is the fixed point of t`RegExam`.
 -}
 data RegExam token alg
   = OneOf (Set token)
@@ -127,7 +130,9 @@ isPassExam :: RegExam token alg -> Bool
 isPassExam (NotOneOf xs (AndNotAsIn ys)) = Set.null xs && Set.null ys
 isPassExam _ = False
 
-{- | `CategoryTest`s for `Categorized` tokens.-}
+{- | `CategoryTest`s for `Categorized` tokens,
+taken in conjunction with `NotOneOf` some `Set` of tokens.
+-}
 data CategoryTest token
   = AndAsIn (Categorize token)
   | AndNotAsIn (Set (Categorize token))
@@ -143,6 +148,10 @@ prop> notB . notOneOf = oneOf
 prop> notB . asIn = notAsIn
 prop> notB . notAsIn = asIn
 
+`TokenClass` is the fixed point algebra of t`RegExam`.
+`TokenClass`es may be understood as normalizations of
+`BooleanAlgebra` expressions generated by `Tokenized`
+expressions.
 -}
 newtype TokenClass token = TokenClass (RegExam token (TokenClass token))
 
@@ -154,6 +163,12 @@ then `tokenClass` is expected to act homomorphically on disjunction.
 prop> empty = tokenClass falseB
 prop> tokenClass x <|> tokenClass y = tokenClass (x >||< y)
 
+Likewise, when a `TokenAlgebra` is a `KleeneStarAlgebra`,
+then `tokenClass` is expected to act homorphically on disjunction.
+
+prop> zeroK = tokenClass falseB
+prop> tokenClass x >|< tokenClass y = tokenClass (x >||< y)
+
 -}
 class Tokenized token p => TokenAlgebra token p where
   tokenClass :: TokenClass token -> p
diff --git a/src/Control/Lens/Grammar/Machine.hs b/src/Control/Lens/Grammar/Machine.hs
index 4f778b9..0fb7f50 100644
--- a/src/Control/Lens/Grammar/Machine.hs
+++ b/src/Control/Lens/Grammar/Machine.hs
@@ -242,7 +242,7 @@ parseForest et word = (concat (itemForests Set.empty Nothing 0 acceptedLen 0), d
   where
     (n, chart) = prefixGen et word
     relations = transducerRelations et
-    acceptedLen = maximum [j | j <- [0 .. n], acceptsChart j chart]
+    acceptedLen = maximum (0 : [j | j <- [0 .. n], acceptsChart j chart])
 
     acceptedWord = take acceptedLen word
     sliceAt start end = take (end - start) (drop start acceptedWord)
@@ -347,10 +347,12 @@ prefixGen
 prefixGen et word = go 0 (initialChart et) word
   where
     go j chart [] = (j, chart)
-    go j chart (x : xs) =
-      let scanned = scanFrom j x chart
-          closed = closeChartAt et (j + 1) (IntMap.insert (j + 1) scanned chart)
-      in go (j + 1) closed xs
+    go j chart (x : xs)
+      | IntMap.null scanned = (j + 1, closed)
+      | otherwise = go (j + 1) closed xs
+      where
+        scanned = scanFrom j x chart
+        closed = closeChartAt et (j + 1) (IntMap.insert (j + 1) scanned chart)
 
     scanFrom j input chart = IntMap.foldrWithKey advance IntMap.empty eJ
       where
diff --git a/src/Control/Lens/PartialIso.hs b/src/Control/Lens/PartialIso.hs
index fb105e7..a93dda6 100644
--- a/src/Control/Lens/PartialIso.hs
+++ b/src/Control/Lens/PartialIso.hs
@@ -298,16 +298,16 @@ difoldl1 pattern =
 
 {- | Right fold & unfold `APartialIso` to an `Control.Lens.Iso.Iso`. -}
 difoldr1
-  :: Cons s t a b
+  :: Snoc s t a b
   => APartialIso d c (b,d) (a,c)
   -> Iso (t,d) (s,c) (t,d) (s,c)
 difoldr1 pattern =
   let
     reorder = iso
-      (\((a,s),c) -> (s,(a,c)))
-      (\(t,(b,d)) -> ((b,t),d))
+      (\((s,a),c) -> (s,(a,c)))
+      (\(t,(b,d)) -> ((t,b),d))
     step
-      = crossPartialIso _Cons id
+      = crossPartialIso _Snoc id
       . reorder
       . crossPartialIso id (coPartialIso pattern)
   in from (iterating step)
@@ -323,7 +323,7 @@ difoldl pattern
 
 {- | Right fold & unfold `APartialIso` to a `Control.Lens.Prism.Prism`. -}
 difoldr
-  :: (AsEmpty t, Cons s t a b)
+  :: (AsEmpty t, Snoc s t a b)
   => APartialIso d c (b,d) (a,c)
   -> Prism d c (t,d) (s,c)
 difoldr pattern
diff --git a/src/Data/Profunctor/Distributor.hs b/src/Data/Profunctor/Distributor.hs
index b7633bf..0f43334 100644
--- a/src/Data/Profunctor/Distributor.hs
+++ b/src/Data/Profunctor/Distributor.hs
@@ -26,7 +26,7 @@ import Control.Lens.PartialIso
 import Data.Bifunctor.Clown
 import Data.Bifunctor.Joker
 import Data.Bifunctor.Product
-import Data.Foldable hiding (toList)
+import Data.Foldable (foldl')
 import Data.Functor.Adjunction
 import Data.Functor.Contravariant.Divisible
 import Data.Profunctor hiding (WrappedArrow)
@@ -248,6 +248,11 @@ class (Choice p, Distributor p, forall x. Alternative (p x))
 choice :: (Foldable f, Alternative p) => f (p a) -> p a
 choice = foldl' (<|>) empty
 
+instance Alternative f
+  => Alternator (Star f) where
+    alternate = either
+      (\(Star f) -> Star (either (fmap Left . f) (const empty)))
+      (\(Star f) -> Star (either (const empty) (fmap Right . f)))
 instance (Alternator p, Applicative f)
   => Alternator (WrappedPafb f p) where
     alternate =
diff --git a/src/Data/Profunctor/Monadic.hs b/src/Data/Profunctor/Monadic.hs
index d2e4cee..69e8b19 100644
--- a/src/Data/Profunctor/Monadic.hs
+++ b/src/Data/Profunctor/Monadic.hs
@@ -63,7 +63,7 @@ version of `pureP`.
 
 prop> pureP = P.return
 -}
-return :: (Monadic p, Choice p) => Prism a b () () -> p a b
+return :: (Monadic p, Choice p) => APrism a b () () -> p a b
 return = pureP
 
 {- | A `Profunctor` which is also a `MonadTry`. -}
diff --git a/src/Data/Profunctor/Monoidal.hs b/src/Data/Profunctor/Monoidal.hs
index 5b5c7d1..a1e83e3 100644
--- a/src/Data/Profunctor/Monoidal.hs
+++ b/src/Data/Profunctor/Monoidal.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-orphans -Wno-redundant-constraints #-}
 
 {-|
 Module      : Data.Profunctor.Monoidal
@@ -16,14 +16,17 @@ module Data.Profunctor.Monoidal
   , oneP, (>*<), (>*), (*<)
   , dimap2, foreverP, ditraverse
     -- * Monoidal & Choice
-  , pureP, asEmpty, (>:<), replicateP, onlyOne
-  , meander, eotFunList
+  , pureP, asEmpty, (>:<), snocP, replicateP, onlyOne
+    -- * Monoidal, Choice & Strong
+  , meander, traverseP, foldP
   ) where
 
 import Control.Lens
 import Control.Lens.Internal.Context
 import Control.Lens.PartialIso
 import Data.Distributive
+import Data.Profunctor
+import Data.Foldable (traverse_)
 import GHC.IsList
 
 -- Monoidal --
@@ -129,6 +132,10 @@ asEmpty = pureP _Empty
 x >:< xs = _Cons >? x >*< xs
 infixr 5 >:<
 
+{- | A `Monoidal` & `Choice` snoc combinator. -}
+snocP :: (Snoc s t a b, Monoidal p, Choice p) => p s t -> p a b -> p s t
+snocP xs x = _Snoc >? xs >*< x
+
 {- | Use when `IsList` with `onlyOne` `Item`. -}
 onlyOne
   :: (Monoidal p, Choice p, IsList s)
@@ -145,17 +152,25 @@ replicateP
 replicateP n _ | n <= 0 = asEmpty
 replicateP n a = a >:< replicateP (n-1) a
 
-{- | For any `Monoidal`, `Choice` & `Data.Profunctor.Strong` `Profunctor`,
+{- | For any `Monoidal`, `Choice` & `Strong` `Profunctor`,
 `meander` is invertible and gives a default implementation for the
 `Data.Profunctor.Traversing.wander`
 method of `Data.Profunctor.Traversing.Traversing`,
-though `Data.Profunctor.Strong` is not needed for its definition.
+though `Strong` isn't needed for its definition,
+but for its invertibility property.
+
+>>> :{
+traversalP :: (forall p. (Monoidal p, Choice p, Strong p) => p a b -> p s t) -> Traversal s t a b
+traversalP f = runStar . f . Star
+:}
+prop> traversalP . meander = id
+prop> meander . traversalP = id
 
 See Pickering, Gibbons & Wu,
 [Profunctor Optics - Modular Data Accessors](https://arxiv.org/abs/1703.10857)
 -}
 meander
-  :: (Monoidal p, Choice p)
+  :: (Monoidal p, Choice p, Strong p)
   => ATraversal s t a b -> p a b -> p s t
 meander f = dimap (f sell) iextract . meandering
   where
@@ -164,6 +179,26 @@ meander f = dimap (f sell) iextract . meandering
       => q u v -> q (Bazaar (->) u w x) (Bazaar (->) v w x)
     meandering q = eotFunList >~ right' (q >*< meandering q)
 
+{- | `traverseP` gives a default implementation for the
+`Data.Profunctor.Traversing.traverse'`
+method of `Data.Profunctor.Traversing.Traversing`.
+-}
+traverseP
+  :: (Traversable f, Monoidal p, Choice p, Strong p)
+  => p a b -> p (f a) (f b)
+traverseP = meander traverse
+
+{- | `foldP` gives a contravariant, profunctorial `Foldable` method.
+However, a `Profunctor` which is also `Contravariant` in its last argument
+is /constant/ over or /phantom/ in its last argument.
+
+prop> foldMap f = getConst . runStar (foldP (Star (Const . f)))
+-}
+foldP
+  :: (Foldable f, Monoidal p, Choice p, Strong p, forall x. (Contravariant (p x)))
+  => p a b -> p (f a) (f b)
+foldP = contramap (const ()) . meander traverse_
+
 {- |
 `eotFunList` is used to define `meander`.
 See van Laarhoven, [A non-regular data type challenge]
diff --git a/src/Data/Profunctor/Separator.hs b/src/Data/Profunctor/Separator.hs
index 21b4d18..3db101c 100644
--- a/src/Data/Profunctor/Separator.hs
+++ b/src/Data/Profunctor/Separator.hs
@@ -22,11 +22,17 @@ module Data.Profunctor.Separator
   , chain
   , chain1
   , intercalateP
+    -- * Operator Expressions
+  , Operator (..)
+  , withOperators
   ) where
 
+import Control.Applicative ((<|>))
 import Control.Lens
 import Control.Lens.PartialIso
 import Control.Lens.Grammar.Symbol
+import Data.Foldable (asum)
+import Data.Maybe (listToMaybe)
 import Data.Profunctor.Distributor
 import Data.Profunctor.Monoidal
 import GHC.Exts
@@ -125,3 +131,171 @@ intercalateP n (SepBy beg end _) _ | n <= 0 =
   beg >* asEmpty *< end
 intercalateP n (SepBy beg end comma) p =
   beg >* p >:< replicateP (n-1) (comma >* p) *< end
+
+data Operator p a b where
+  Infix :: APartialIso a b (a,a) (b,b) -> p () () -> Operator p a b
+  InfixL :: APartialIso a b (a,a) (b,b) -> p () () -> Operator p a b
+  InfixR :: APartialIso a b (a,a) (b,b) -> p () () -> Operator p a b
+  Prefix :: APartialIso a b a b -> p () () -> Operator p a b
+  Postfix :: APartialIso a b a b -> p () () -> Operator p a b
+
+{- | Build an expression `Alternator` from a table of `Operator`s and
+an atomic term `Alternator`, analagous to @buildExpressionParser@ from
+[parsec](https://hackage.haskell.org/package/parsec).
+
+The operator table is a list of list of operators, ordered from highest to lowest precedence.
+Each level is a list of `Operator`s which share precedence.
+Within a level, `InfixL`, `InfixR` & `Infix` set left, right & non-associativity for binary operators,
+while `Prefix` & `Postfix` are for unary operators.
+
+For example, an expression grammar over natural numbers with a
+right-associative exponent @^@ binding tighter than left-associative @*@,
+which binds tighter than left-associative @+@ & @-@:
+
+>>> import Numeric.Natural (Natural)
+>>> import Control.Lens.Grammar
+>>> import Control.Lens (Prism', prism', iso)
+>>> :{
+data Expr
+  = Nat Natural
+  | Exp Expr Expr
+  | Mul Expr Expr
+  | Add Expr Expr
+  | Sub Expr Expr
+  deriving stock (Eq, Ord, Show, Read)
+_Nat :: Prism' Expr Natural
+_Nat = prism' Nat (\case Nat n -> Just n; _ -> Nothing)
+_Exp, _Mul, _Add, _Sub :: Prism' Expr (Expr, Expr)
+_Exp = prism' (uncurry Exp) (\case Exp x y -> Just (x,y); _ -> Nothing)
+_Mul = prism' (uncurry Mul) (\case Mul x y -> Just (x,y); _ -> Nothing)
+_Add = prism' (uncurry Add) (\case Add x y -> Just (x,y); _ -> Nothing)
+_Sub = prism' (uncurry Sub) (\case Sub x y -> Just (x,y); _ -> Nothing)
+exprGrammar :: Grammar Char Expr
+exprGrammar = ruleRec "expr" $ \expr ->
+  let atom = rule "atom" $ nat <|> terminal "(" >* expr *< terminal ")"
+      nat  = rule "nat"  $ _Nat . iso show read >? someP (asIn @Char DecimalNumber)
+  in withOperators
+    [ [ InfixR _Exp (terminal "^") ]
+    , [ InfixL _Mul (terminal "*") ]
+    , [ InfixL _Add (terminal "+"), InfixL _Sub (terminal "-") ]
+    ] atom
+:}
+
+The right-associative @^@ groups to the right, @-@ to the left, and @*@
+binds tighter than @+@:
+
+>>> [e | (e,"") <- parseG exprGrammar "2^3^2"]
+[Exp (Nat 2) (Exp (Nat 3) (Nat 2))]
+>>> [e | (e,"") <- parseG exprGrammar "3-2-1"]
+[Sub (Sub (Nat 3) (Nat 2)) (Nat 1)]
+>>> [e | (e,"") <- parseG exprGrammar "2*3+4"]
+[Add (Mul (Nat 2) (Nat 3)) (Nat 4)]
+>>> [e | (e,"") <- parseG exprGrammar "2*(3+4)"]
+[Mul (Nat 2) (Add (Nat 3) (Nat 4))]
+
+Being bidirectional, the same grammar prints:
+
+>>> unparseG exprGrammar (Exp (Nat 2) (Exp (Nat 3) (Nat 2))) "" :: Maybe String
+Just "2^3^2"
+-}
+withOperators
+  :: Alternator p
+  => [[Operator p a b]] -- ^ operator table
+  -> p a b -- ^ atomic term
+  -> p a b -- ^ expression
+withOperators table p = foldl makeLevel p table
+  where
+    makeLevel term ops =
+      let
+        (nas, las, ras, pres, posts) =
+          foldr splitOp ([],[],[],[],[]) ops
+        termP = withPostP posts (withPreP pres term)
+      in
+        case (nas, las, ras) of
+          (_,  [], []) -> infixNP nas termP
+          ([], _,  []) -> infixLP manyP las termP
+          ([], [], _ ) -> infixRP manyP ras termP
+          _            ->
+            infixRP someP ras termP
+            <|> infixLP someP las termP
+            <|> infixNP nas termP
+
+    splitOp oper (nas, las, ras, pres, posts) = case oper of
+      Infix   pat sym -> ((pat,sym):nas, las, ras, pres, posts)
+      InfixL  pat sym -> (nas, (pat,sym):las, ras, pres, posts)
+      InfixR  pat sym -> (nas, las, (pat,sym):ras, pres, posts)
+      Prefix  pat sym -> (nas, las, ras, (pat,sym):pres, posts)
+      Postfix pat sym -> (nas, las, ras, pres, (pat,sym):posts)
+
+    tagSepP syms = choice [only i >? sym | (i, sym) <- zip [0 :: Int ..] syms]
+
+    withPreP ops inner =
+      difoldr (partialIso fwd bwd) >? manyP (tagSepP (snd <$> ops)) >*< inner
+      where
+        fns = [withPartialIso pat (,) | (pat, _) <- ops]
+        fwd x = asum
+          [ (\y -> (i,y)) <$> f x | (i, (f,_)) <- zip [0 :: Int ..] fns ]
+        bwd (i,y) = case drop i fns of
+          (_,g):_ -> g y
+          [] -> Nothing
+
+    withPostP ops inner =
+      difoldl (partialIso fwd bwd) >? inner >*< manyP (tagSepP (snd <$> ops))
+      where
+        fns = [withPartialIso pat (,) | (pat, _) <- ops]
+        fwd x = asum
+          [ (\y -> (y,i)) <$> f x | (i, (f,_)) <- zip [0 :: Int ..] fns ]
+        bwd (y,i) = case drop i fns of
+          (_,g):_ -> g y
+          [] -> Nothing
+
+    infixNP ops term =
+      difoldl (partialIso fwd bwd) >? term >*< oneTail
+      where
+        oneTail =
+          iso listToMaybe (maybe [] pure) >~
+            optionalP (tagSepP (snd <$> ops) >*< term)
+        fns = [withPartialIso pat (,) | (pat, _) <- ops]
+        fwd x = asum
+          [ (\(l,r) -> (l,(i,r))) <$> f x
+          | (i, (f,_)) <- zip [0 :: Int ..] fns ]
+        bwd (l,(i,r)) = case drop i fns of
+          (_,g):_ -> g (l,r)
+          [] -> Nothing
+
+    -- Left-associative applications, folded to the left. The @rep@ tail
+    -- combinator is `manyP` for a pure-left level (the empty tail folds back
+    -- to the bare term) or `someP` in a mixed level (an operator is required).
+    infixLP
+      :: Alternator p
+      => (p (Int,a) (Int,b) -> p [(Int,a)] [(Int,b)])
+      -> [(APartialIso a b (a,a) (b,b), p () ())] -> p a b -> p a b
+    infixLP rep ops term =
+      difoldl (partialIso fwd bwd) >?
+        term >*< rep (tagSepP (snd <$> ops) >*< term)
+      where
+        fns = [withPartialIso pat (,) | (pat, _) <- ops]
+        fwd x = asum
+          [ (\(l,r) -> (l,(i,r))) <$> f x
+          | (i, (f,_)) <- zip [0 :: Int ..] fns ]
+        bwd (l,(i,r)) = case drop i fns of
+          (_,g):_ -> g (l,r)
+          [] -> Nothing
+
+    -- Right-associative applications, folded to the right. As with `infixLP`,
+    -- @rep@ is `manyP` for a pure-right level or `someP` in a mixed level.
+    infixRP
+      :: Alternator p
+      => (p (a,Int) (b,Int) -> p [(a,Int)] [(b,Int)])
+      -> [(APartialIso a b (a,a) (b,b), p () ())] -> p a b -> p a b
+    infixRP rep ops term =
+      difoldr (partialIso fwd bwd) >?
+        rep (term >*< tagSepP (snd <$> ops)) >*< term
+      where
+        fns = [withPartialIso pat (,) | (pat, _) <- ops]
+        fwd x = asum
+          [ (\(l,r) -> ((l,i),r)) <$> f x
+          | (i, (f,_)) <- zip [0 :: Int ..] fns ]
+        bwd ((l,i),r) = case drop i fns of
+          (_,g):_ -> g (l,r)
+          [] -> Nothing
diff --git a/test/Examples/Expression.hs b/test/Examples/Expression.hs
new file mode 100644
index 0000000..996b5af
--- /dev/null
+++ b/test/Examples/Expression.hs
@@ -0,0 +1,103 @@
+module Examples.Expression
+  ( Expr (..)
+  , exprGrammar
+  , exprExamples
+  , powGrammar
+  , powExamples
+  , leftGrammar
+  , leftExamples
+  ) where
+
+import Control.Applicative
+import Control.Lens
+import Control.Lens.Grammar
+import Numeric.Natural
+
+data Expr
+  = Nat Natural
+  | Exp Expr Expr
+  | Mul Expr Expr
+  | Div Expr Expr
+  | Add Expr Expr
+  | Sub Expr Expr
+  deriving stock (Eq, Ord, Show, Read)
+
+makePrisms ''Expr
+
+-- | An expression grammar over natural numbers, built with `withOperators`
+-- from a precedence table: parenthesization binds tightest, then a
+-- right-associative exponent @^@, then left-associative @*@ & @/@, then
+-- left-associative @+@ & @-@.
+exprGrammar :: Grammar Char Expr
+exprGrammar = ruleRec "expr" $ \expr ->
+  let
+    atom = rule "atom" $
+      nat <|> terminal "(" >* expr *< terminal ")"
+    nat = rule "nat" $
+      _Nat . iso show read >? someP (asIn @Char DecimalNumber)
+  in withOperators
+    [ [ InfixR _Exp (terminal "^") ]
+    , [ InfixL _Mul (terminal "*"), InfixL _Div (terminal "/") ]
+    , [ InfixL _Add (terminal "+"), InfixL _Sub (terminal "-") ]
+    ] atom
+
+exprExamples :: [(Expr, String)]
+exprExamples =
+  [ (Nat 42, "42")
+  , (Add (Nat 1) (Nat 2), "1+2")
+  , (Sub (Sub (Nat 3) (Nat 2)) (Nat 1), "3-2-1")
+  , (Div (Div (Nat 8) (Nat 2)) (Nat 2), "8/2/2")
+  , (Exp (Nat 2) (Exp (Nat 3) (Nat 2)), "2^3^2")
+  , (Add (Mul (Nat 2) (Nat 3)) (Nat 4), "2*3+4")
+  , (Sub (Nat 1) (Div (Nat 6) (Nat 3)), "1-6/3")
+  , (Mul (Exp (Nat 2) (Nat 3)) (Nat 4), "2^3*4")
+  , (Mul (Nat 2) (Add (Nat 3) (Nat 4)), "2*(3+4)")
+  , (Exp (Add (Nat 1) (Nat 2)) (Nat 3), "(1+2)^3")
+  ]
+
+-- | A purely right-associative grammar built directly with `chain1` @Right@,
+-- so it exercises `chainr1` / `difoldr` independently of `withOperators`.
+-- This is a regression test for the right-fold: @2^3^2@ must associate as
+-- @Exp 2 (Exp 3 2)@, not @Exp 3 (Exp 2 2)@.
+powGrammar :: Grammar Char Expr
+powGrammar = ruleRec "pow" $ \e ->
+  let
+    atom = rule "atom" $
+      nat <|> terminal "(" >* e *< terminal ")"
+    nat = rule "nat" $
+      _Nat . iso show read >? someP (asIn @Char DecimalNumber)
+  in chain1 (\x -> Right x) _Exp (sepWith "^") atom
+
+powExamples :: [(Expr, String)]
+powExamples =
+  [ (Nat 2, "2")
+  , (Exp (Nat 2) (Nat 3), "2^3")
+  , (Exp (Nat 2) (Exp (Nat 3) (Nat 2)), "2^3^2")
+  , (Exp (Nat 2) (Exp (Nat 3) (Exp (Nat 4) (Nat 5))), "2^3^4^5")
+  ]
+
+-- | A purely left-associative expression grammar (no right-associative
+-- exponent) built with `withOperators`. Because every level is a single
+-- associativity, `withOperators` parses each leading term exactly once, so
+-- unlike the mixed `exprGrammar` this one is LL1 and is tested against the
+-- predictive @parsecG@ / megaparsec backends (@testCfg True@).
+leftGrammar :: Grammar Char Expr
+leftGrammar = ruleRec "expr" $ \expr ->
+  let
+    atom = rule "atom" $
+      nat <|> terminal "(" >* expr *< terminal ")"
+    nat = rule "nat" $
+      _Nat . iso show read >? someP (asIn @Char DecimalNumber)
+  in withOperators
+    [ [ InfixL _Mul (terminal "*"), InfixL _Div (terminal "/") ]
+    , [ InfixL _Add (terminal "+"), InfixL _Sub (terminal "-") ]
+    ] atom
+
+leftExamples :: [(Expr, String)]
+leftExamples =
+  [ (Nat 7, "7")
+  , (Sub (Sub (Nat 3) (Nat 2)) (Nat 1), "3-2-1")
+  , (Div (Div (Nat 8) (Nat 2)) (Nat 2), "8/2/2")
+  , (Sub (Add (Nat 1) (Mul (Nat 2) (Nat 3))) (Nat 4), "1+2*3-4")
+  , (Mul (Add (Nat 1) (Nat 2)) (Nat 3), "(1+2)*3")
+  ]
diff --git a/test/Main.hs b/test/Main.hs
index f73df07..eab2c5c 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -17,6 +17,7 @@ import qualified Text.Megaparsec as M
 
 import Examples.Arithmetic
 import Examples.Chain
+import Examples.Expression
 import Examples.Json
 import Examples.Lambda
 import Examples.LenVec
@@ -41,6 +42,9 @@ main = do
     describe "lambdaGrammar" $ testCfg True lambdaExamples lambdaGrammar
     describe "lenvecGrammar" $ testCsg True lenvecExamples lenvecGrammar
     describe "chainGrammar" $ testCfg True chainExamples chainGrammar
+    describe "exprGrammar" $ testCfg False exprExamples exprGrammar
+    describe "powGrammar" $ testCfg False powExamples powGrammar
+    describe "leftGrammar" $ testCfg True leftExamples leftGrammar
     describe "parseForest" parseForestTests
     describe "Parsector try rollback" tryRollbackTests
     describe "Kleene" kleeneProperties
@@ -89,7 +93,9 @@ doctests = do
   ghcEnvironment <- lookupEnv "GHC_ENVIRONMENT"
   let
     modulePaths =
-      [ "src/Control/Lens/Grammar.hs" ]
+      [ "src/Control/Lens/Grammar.hs"
+      , "src/Data/Profunctor/Separator.hs"
+      ]
     sourceDirs =
       [ "-isrc"
       , "-itest"
diff --git a/test/Properties/Kleene.hs b/test/Properties/Kleene.hs
index ab5f1c9..36b410f 100644
--- a/test/Properties/Kleene.hs
+++ b/test/Properties/Kleene.hs
@@ -7,9 +7,7 @@ import Test.Hspec
 import Test.Hspec.QuickCheck (prop)
 import Test.QuickCheck
 
-instance Arbitrary GeneralCategory where
-  arbitrary = arbitraryBoundedEnum
-  shrink = shrinkBoundedEnum
+-- NB: @Arbitrary GeneralCategory@ is now provided by QuickCheck itself.
 
 instance Arbitrary (TokenClass Char) where
   arbitrary = sized go