diff --git a/CHANGELOG.md b/CHANGELOG.md
index 693daf6..ba221d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,46 @@
 # Changelog for `distributors`
 
+## 0.4.0.0 - 2026-04-10
+
+### New Modules
+
+- `Control.Monad.Fail.Try` - `MonadTry` class with `try` & `fail` for backtracking parsers
+- `Data.Profunctor.Grammar.Parsector` - Invertible LL(1) parser with Parsec-style error reporting:
+  `ParsecState`, `ParsecError`, `parsecP`, `unparsecP`; implements hints, LL(1) commitment
+  via `parsecLooked`, and `try` for explicit backtracking
+- `Data.Profunctor.Separator` - Separator/delimiter combinators: `sepWith`, `noSep`,
+  `beginWith`, `endWith`, `several`, `several1`, `intercalateP`, `chain`, `chain1`
+- `Data.Traversable.Homogeneous` - `Homogeneous` class for static containers with uniform elements;
+  `ditraverse` for distributive traversals
+
+### New Combinators
+
+- `Control.Lens.Grammar.Kleene`: `tokenClass` embedding into `RegEx`; `KleeneAlgebra` laws
+  as QuickCheck properties; `RegExam` helpers `failExam`, `passExam`, `isFailExam`
+- `Control.Lens.Grammar.Boole`: `trueB`, `falseB` added to `BooleanAlgebra`;
+  `andB`, `orB`, `allB`, `anyB` fold combinators
+- `Data.Profunctor.Monadic`: `MonadicTry` constraint alias; `P.return` combinator;
+  improved documentation for qualified do-notation pattern bonding
+- `Data.Profunctor.Distributor`: `manyP` / `optionalP` now place the empty case on
+  the right of `>+<` for correct LL(1) behaviour (`p >*< manyP p >+< oneP`)
+
+### Changes
+
+- `<|>` in `Parsector` now commits when the left branch consumes input (LL(1));
+  use `try` to opt into backtracking
+- `TokenTest` renamed to `TokenClass` throughout
+- `chain`, `chain1`, `intercalateP` moved from `Data.Profunctor.Distributor`
+  to the new `Data.Profunctor.Separator`
+- `BackusNaurForm`: `rule` documentation clarified; added reference to Breitner's
+  *Showcasing Applicative*
+
+### Testing
+
+- `test/Properties/Kleene` - QuickCheck properties for `KleeneStarAlgebra`,
+  `TokenAlgebra`, `BooleanAlgebra TokenClass`
+- `test/Examples/Chain` - Chain grammar example
+- `test/Main`: `testCtxGrammarExample` extended with `parsecG` / `unparsecG` round-trip checks
+
 ## 0.3.0.0 - 2026-02-05
 
 ### New Modules
diff --git a/distributors.cabal b/distributors.cabal
index 9a92b07..7350ef4 100644
--- a/distributors.cabal
+++ b/distributors.cabal
@@ -5,7 +5,7 @@ cabal-version: 2.2
 -- see: https://github.com/sol/hpack
 
 name:           distributors
-version:        0.3.0.0
+version:        0.4.0.0
 synopsis:       Unifying Parsers, Printers & Grammars
 description:    Distributors provides mathematically inspired abstractions for coders to write parsers that can also be inverted to printers.
 category:       Profunctors, Optics, Parsing
@@ -41,11 +41,15 @@ library
       Control.Lens.Monocle
       Control.Lens.PartialIso
       Control.Lens.Wither
+      Control.Monad.Fail.Try
       Data.Profunctor.Distributor
       Data.Profunctor.Filtrator
       Data.Profunctor.Grammar
+      Data.Profunctor.Grammar.Parsector
       Data.Profunctor.Monadic
       Data.Profunctor.Monoidal
+      Data.Profunctor.Separator
+      Data.Traversable.Homogeneous
   other-modules:
       Paths_distributors
   autogen-modules:
@@ -116,12 +120,14 @@ test-suite test
   main-is: Main.hs
   other-modules:
       Examples.Arithmetic
+      Examples.Chain
       Examples.Json
       Examples.Lambda
       Examples.LenVec
       Examples.RegString
       Examples.SemVer
       Examples.SExpr
+      Properties.Kleene
       Paths_distributors
   autogen-modules:
       Paths_distributors
@@ -168,6 +174,7 @@ test-suite test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
       MemoTrie >=0.6 && <1
+    , QuickCheck >=2.14 && <3
     , adjunctions >=4.4 && <5
     , base >=4.15 && <5
     , bifunctors >=5.5 && <6
diff --git a/package.yaml b/package.yaml
index 3f0209e..a4bcd1c 100644
--- a/package.yaml
+++ b/package.yaml
@@ -1,5 +1,5 @@
 name: distributors
-version: 0.3.0.0
+version: 0.4.0.0
 github: "morphismtech/distributors"
 license: BSD-3-Clause
 author: "Eitan Chatav"
@@ -97,3 +97,4 @@ tests:
       - distributors
       - doctest >= 0.18 && < 1
       - hspec >= 2.7 && < 3
+      - QuickCheck >= 2.14 && < 3
diff --git a/src/Control/Lens/Bifocal.hs b/src/Control/Lens/Bifocal.hs
index 6a09aaf..2bf5e5e 100644
--- a/src/Control/Lens/Bifocal.hs
+++ b/src/Control/Lens/Bifocal.hs
@@ -39,6 +39,7 @@ import Control.Lens.PartialIso
 import Data.Profunctor
 import Data.Profunctor.Distributor
 import Data.Profunctor.Filtrator
+import Data.Profunctor.Separator
 import Witherable
 
 {- | `Bifocal`s are bidirectional parser optics.
diff --git a/src/Control/Lens/Diopter.hs b/src/Control/Lens/Diopter.hs
index c78b06c..231209f 100644
--- a/src/Control/Lens/Diopter.hs
+++ b/src/Control/Lens/Diopter.hs
@@ -27,6 +27,7 @@ module Control.Lens.Diopter
 import Control.Lens
 import Control.Lens.Internal.Profunctor
 import Data.Profunctor.Distributor
+import Data.Traversable.Homogeneous
 import Data.Void
 import GHC.Generics
 
@@ -41,8 +42,7 @@ type Diopter s t a b = forall p f.
   (Distributor p, Applicative f)
     => p a (f b) -> p s (f t)
 
-{- | If you see `ADiopter` in a signature for a function,
-the function is expecting a `Diopter`. -}
+{- | `ADiopter` is monomorphically a `Diopter`. -}
 type ADiopter s t a b =
   Dioptrice a b a (Identity b) -> Dioptrice a b s (Identity t)
 
diff --git a/src/Control/Lens/Grammar.hs b/src/Control/Lens/Grammar.hs
index 27ce10b..d038c74 100644
--- a/src/Control/Lens/Grammar.hs
+++ b/src/Control/Lens/Grammar.hs
@@ -23,13 +23,17 @@ module Control.Lens.Grammar
   , RegBnf (..)
   , regbnfG
   , regbnfGrammar
-    -- * Context-sensitive grammar
+    -- * Unrestricted, context-sensitive grammar
   , CtxGrammar
   , printG
   , parseG
   , unparseG
+  , parsecG
+  , unparsecG
     -- * Utility
   , putStringLn
+    -- * Re-exports
+  , module X
   ) where
 
 import Control.Applicative
@@ -47,17 +51,34 @@ import Data.Profunctor.Filtrator
 import Data.Profunctor.Monadic
 import Data.Profunctor.Monoidal
 import Data.Profunctor.Grammar
-import qualified Data.Set as Set
+import Data.Profunctor.Grammar.Parsector
+import Data.Profunctor.Separator
 import Data.String
 import GHC.Exts
 import Prelude hiding (filter)
 import Witherable
 
+-- Re-exports
+import Control.Lens.Grammar.BackusNaur as X
+import Control.Lens.Grammar.Boole as X
+import Control.Lens.Grammar.Kleene as X
+import Control.Lens.Grammar.Symbol as X
+import Control.Lens.Grammar.Token as X
+import Control.Lens.PartialIso as X
+import Control.Monad.Fail.Try as X
+import Data.Profunctor.Distributor as X
+import Data.Profunctor.Filtrator as X
+import Data.Profunctor.Grammar as X
+import Data.Profunctor.Grammar.Parsector as X
+import Data.Profunctor.Monoidal as X
+import Data.Profunctor.Separator as X
+import Data.Traversable.Homogeneous as X
+
 {- |
 A regular grammar may be constructed using
 `Lexical` and `Alternator` combinators.
 Let's see an example using
-[semantic versioning](https://semver.org/).
+[semantic versioning](https://semver.org/) syntax.
 
 >>> import Numeric.Natural (Natural)
 >>> :{
@@ -73,12 +94,17 @@ data SemVer = SemVer          -- e.g., 2.1.5-rc.1+build.123
 
 We'd like to define an optic @_SemVer@,
 corresponding to the constructor pattern @SemVer@.
+You _could_ generate it with the TemplateHaskell combinator,
+`makeNestedPrisms`.
+
+@makeNestedPrisms ''SemVer@
+
 Unfortunately, we can't use TemplateHaskell to generate it in [GHCi]
 (https://wiki.haskell.org/GHC/GHCi),
 which is used to test this documenation.
-Normally we would write `makeNestedPrisms` @''SemVer@,
-but here is equivalent explicit Haskell code instead.
-Since @SemVer@ is a newtype, @_SemVer@ can be an `Control.Lens.Iso.Iso`.
+Here is equivalent Haskell code instead.
+Since @SemVer@ has only one constructor,
+@_SemVer@ can be an `Control.Lens.Iso.Iso`.
 
 >>> :set -XRecordWildCards
 >>> import Control.Lens (Iso', iso)
@@ -98,11 +124,11 @@ semverGrammar = _SemVer
   >?  numberG
   >*< terminal "." >* numberG
   >*< terminal "." >* numberG
-  >*< option [] (terminal "-" >* identifiersG)
-  >*< option [] (terminal "+" >* identifiersG)
+  >*< optionP _Empty (terminal "-" >* identifiersG)
+  >*< optionP _Empty (terminal "+" >* identifiersG)
   where
     numberG = iso show read >~ someP (asIn @Char DecimalNumber)
-    identifiersG = several1 (sepBy (terminal ".")) (someP charG)
+    identifiersG = several1 (sepWith ".") (someP charG)
     charG = asIn LowercaseLetter
       <|> asIn UppercaseLetter
       <|> asIn DecimalNumber
@@ -122,15 +148,17 @@ combinators like `<|>` work both `Functor`ially and `Profunctor`ially.
 +------------+---------------+
 | `<$>`      | `>?`          |
 +------------+---------------+
+| `pure`     | `pureP`       |
++------------+---------------+
 | `*>`       | `>*`          |
 +------------+---------------+
 | `<*`       | `*<`          |
 +------------+---------------+
 | `<*>`      | `>*<`         |
 +------------+---------------+
-| `<|>`      | `<|>`         |
+| `empty`    | `empty`       |
 +------------+---------------+
-| `option`   | `option`      |
+| `<|>`      | `<|>`         |
 +------------+---------------+
 | `choice`   | `choice`      |
 +------------+---------------+
@@ -212,16 +240,16 @@ arithGrammar :: Grammar Char Arith
 arithGrammar = ruleRec "arith" sumG
   where
     sumG arith = rule "sum" $
-      chain1 Left _Add (sepBy (terminal "+")) (prodG arith)
+      chain1 Left _Add (sepWith "+") (prodG arith)
     prodG arith = rule "product" $
-      chain1 Left _Mul (sepBy (terminal "*")) (factorG arith)
+      chain1 Left _Mul (sepWith "*") (factorG arith)
     factorG arith = rule "factor" $
       numberG <|> terminal "(" >* arith *< terminal ")"
     numberG = rule "number" $
       _Num . iso show read >? someP (asIn @Char DecimalNumber)
 :}
 
-We can generate a `RegBnf`, printers and parsers from @arithGrammar@.
+We can generate grammar strings, printers and parsers from @arithGrammar@.
 
 >>> putStringLn (regbnfG arithGrammar)
 {start} = \q{arith}
@@ -230,14 +258,20 @@ We can generate a `RegBnf`, printers and parsers from @arithGrammar@.
 {number} = \p{Nd}+
 {product} = \q{factor}(\*\q{factor})*
 {sum} = \q{product}(\+\q{product})*
-
 >>> [x | (x,"") <- parseG arithGrammar "1+2*3+4"]
 [Add (Add (Num 1) (Mul (Num 2) (Num 3))) (Num 4)]
 >>> unparseG arithGrammar (Add (Num 1) (Mul (Num 2) (Num 3))) "" :: Maybe String
 Just "1+2*3"
->>> do pr <- printG arithGrammar (Num 69); return (pr "") :: Maybe String
+>>> do pr <- printG arithGrammar (Num 69); pure (pr "") :: Maybe String
 Just "69"
 
+If all `rule`s are non-recursive, then a `Grammar`
+can be rewritten as a `RegGrammar`.
+Since Haskell permits general recursion, and `RegGrammar`s are
+embedded in Haskell, you can define context-free grammars with them.
+But it's recommended to use `Grammar`s for `rule` abstraction
+and generator support for `ruleRec`.
+
 -}
 type Grammar token a = forall p.
   ( Lexical token p
@@ -245,19 +279,7 @@ type Grammar token a = forall p.
   , Alternator p
   ) => p a a
 
-{- |
-In addition to context-sensitivity via `Monadic` combinators,
-`CtxGrammar`s adds general filtration via `Filtrator` to `Grammar`s.
-
->>> :{
-palindromeG :: CtxGrammar Char String
-palindromeG = rule "palindrome" $
-  satisfied (\wrd -> reverse wrd == wrd) >?< manyP (anyToken @Char)
-:}
-
-The `satisfied` pattern is used together with the `Choice` &
-`Data.Profunctor.Cochoice` applicator `>?<` for general filtration.
-For context-sensitivity,
+{- | For context-sensitivity,
 the `Monadic` interface is used by importing "Data.Profunctor.Monadic"
 qualified and using a "bonding" notation which mixes
 "idiom" style with qualified do-notation.
@@ -280,7 +302,7 @@ lenvecGrammar :: CtxGrammar Char LenVec
 lenvecGrammar = _LenVec >? P.do
   let
     numberG = iso show read >~ someP (asIn @Char DecimalNumber)
-    vectorG n = intercalateP n (sepBy (terminal ",")) numberG
+    vectorG n = intercalateP n (sepWith ",") numberG
   len <- numberG             -- bonds to _LenVec
   terminal ";"               -- doesn't bond
   vectorG (fromIntegral len) -- bonds to _LenVec
@@ -290,16 +312,17 @@ The qualified do-notation changes the signature of
 @P.@`Data.Profunctor.Monadic.>>=`,
 so that we must apply the constructor pattern @_LenVec@
 to the do-block with the `>?` applicator.
-Any bound named variable, @var <- action@,
+Any scoped bound action, @var <- action@,
 gets "bonded" to the constructor pattern.
 Any unbound actions, except for the last action in the do-block,
 does not get bonded to the pattern.
 The last action does get bonded to the pattern.
-Any unnamed bound action, @_ <- action@,
+Any unscoped bound action, @_ <- action@,
 also gets bonded to the pattern,
-but being unnamed means it isn't added to the context.
-If all bound actions are unnamed, then a `CtxGrammar` can
-be rewritten as a `Grammar` since it is context-free.
+but being unscoped means it isn't added to the context.
+If all bound actions are unscoped,
+and filtration & failure handling aren't used,
+then a `CtxGrammar` can be rewritten as a `Grammar` since it is context-free.
 We can't generate a `RegBnf` since the `rule`s
 of a `CtxGrammar` aren't static, but dynamic and contextual.
 We can generate parsers and printers as expected.
@@ -312,15 +335,59 @@ We can generate parsers and printers as expected.
 ["2;6,7"]
 >>> [pr "" | pr <- printG lenvecGrammar (LenVec 200 [100])] :: [String]
 []
+
+In addition to context-sensitivity via `Monadic` combinators,
+`CtxGrammar`s add unrestricted filtration to `Grammar`s.
+The `satisfy` combinator is an unrestricted token filter.
+And the `satisfied` pattern is used together with the `Choice` &
+`Data.Profunctor.Cochoice` applicator `>?<` for unrestricted filtration.
+
+>>> :{
+palindromeG :: CtxGrammar Char String
+palindromeG = rule "palindrome" $
+  satisfied (\wrd -> reverse wrd == wrd) >?< manyP (anyToken @Char)
+:}
+
 >>> [pal | word <- ["racecar", "word"], (pal, "") <- parseG palindromeG word]
 ["racecar"]
+
+Since `CtxGrammar`s are embedded in Haskell,
+permitting computable predicates,
+and `Filtrator` has a default definition for `Monadic` `Alternator`s,
+the context-sensitivity of `CtxGrammar` implies
+unrestricted filtration of grammars by computable predicates,
+which can recognize the class of recursively enumerable languages.
+
+Finally, `CtxGrammar`s support error reporting and backtracking.
+This has no effect on `printG`, `parseG` or `unparseG`;
+but it effects `parsecG` and `unparsecG`.
+For context, an @LL@ grammar can be (un)parsed by an @LL@ parser.
+An @LL@ parser (un)parses from left to right,
+and constucts leftmost derivations.
+An @LL(k)@ parser can look @k@ tokens ahead.
+`Parsor` is an @LL(∞)@ parser.
+`Parsector` is an @LL(1)@ parser.
+The backtracking `try` combinator
+restores full lookahead to `Parsector`.
+Since both `Parsor` & `Parsector` are @LL@ parsers they
+diverge if the `CtxGrammar` they're run on is left-recursive.
+
+>>> parsecG (rule "foo" (fail "bar") <|> fail "baz") "abc"
+ParsecState {parsecLooked = False, parsecOffset = 0, parsecStream = "abc", parsecHint = ParsecError {parsecExpect = TokenClass (OneOf (fromList "")), parsecLabels = []}, parsecResult = Left (ParsecError {parsecExpect = TokenClass (OneOf (fromList "")), parsecLabels = [Node {rootLabel = "foo", subForest = [Node {rootLabel = "bar", subForest = []}]},Node {rootLabel = "baz", subForest = []}]})}
+
+>>> parsecG (manyP (token 'a') >*< asIn @Char DecimalNumber) "aaab"
+ParsecState {parsecLooked = True, parsecOffset = 3, parsecStream = "b", parsecHint = ParsecError {parsecExpect = TokenClass (OneOf (fromList "")), parsecLabels = []}, parsecResult = Left (ParsecError {parsecExpect = TokenClass (Alternate (TokenClass (OneOf (fromList "a"))) (TokenClass (NotOneOf (fromList "") (AndAsIn DecimalNumber)))), parsecLabels = []})}
+
+>>> unparsecG (tokens "abc") "abx" ""
+ParsecState {parsecLooked = True, parsecOffset = 2, parsecStream = "ab", parsecHint = ParsecError {parsecExpect = TokenClass (OneOf (fromList "")), parsecLabels = []}, parsecResult = Left (ParsecError {parsecExpect = TokenClass (OneOf (fromList "c")), parsecLabels = []})}
+
 -}
 type CtxGrammar token a = forall p.
   ( Lexical token p
   , forall x. BackusNaurForm (p x x)
   , Alternator p
   , Filtrator p
-  , Monadic p
+  , MonadicTry p
   ) => p a a
 
 {- |
@@ -336,8 +403,9 @@ type Lexical token p =
   ) :: Constraint
 
 {- | `RegString`s are an embedded domain specific language
-of regular expression strings. Since they are strings,
-they have a string-like interface.
+of regular expression strings.
+
+Since they are strings, they have a string-like interface.
 
 >>> let rex = fromString "ab|c" :: RegString
 >>> putStringLn rex
@@ -353,7 +421,7 @@ ab|c
 `RegString`s are actually stored as an algebraic datatype, `RegEx`.
 
 >>> runRegString rex
-RegExam (Alternate (Terminal "ab") (Terminal "c"))
+RegExam (Alternate (Sequence (RegExam (OneOf (fromList "a"))) (RegExam (OneOf (fromList "b")))) (RegExam (OneOf (fromList "c"))))
 
 `RegString`s are similar to regular expression strings in many other
 programming languages. We can use them to see if a word and pattern
@@ -442,6 +510,14 @@ newtype RegString = RegString {runRegString :: RegEx Char}
 
 {- | `RegBnf`s are an embedded domain specific language
 of Backus-Naur forms extended by regular expression strings.
+
+A `RegBnf` consists of a distinguished `RegString` "start" rule,
+and a set of named `RegString` `rule`s.
+
+>>> putStringLn (rule "baz" (terminal "foo" >|< terminal "bar") :: RegBnf)
+{start} = \q{baz}
+{baz} = foo|bar
+
 Like `RegString`s they have a string-like interface.
 
 >>> let bnf = fromString "{start} = foo|bar" :: RegBnf
@@ -449,6 +525,8 @@ Like `RegString`s they have a string-like interface.
 {start} = foo|bar
 >>> bnf
 "{start} = foo|bar"
+>>> :type toList bnf
+toList bnf :: [Char]
 
 `RegBnf`s can be generated from context-free `Grammar`s with `regbnfG`.
 
@@ -458,6 +536,13 @@ regbnfG regbnfGrammar :: RegBnf
 Like `RegString`s, `RegBnf`s can be constructed using
 `Lexical`, `Monoid` and `KleeneStarAlgebra` combinators.
 But they also support `BackusNaurForm` `rule`s and `ruleRec`s.
+
+>>> putStringLn (rule "baz" (bnf >|< terminal "baz"))
+{start} = \q{baz}
+{baz} = foo|bar|baz
+>>> putStringLn (ruleRec "∞-loop" (\x -> x) :: RegBnf)
+{start} = \q{∞-loop}
+{∞-loop} = \q{∞-loop}
 -}
 newtype RegBnf = RegBnf {runRegBnf :: Bnf RegString}
   deriving newtype
@@ -486,31 +571,28 @@ are a context-free language.
 >>> putStringLn (regbnfG regexGrammar)
 {start} = \q{regex}
 {alternate} = \q{sequence}(\|\q{sequence})*
-{atom} = (\\q\{)\q{char}*\}|\q{char}|\q{char-class}|\(\q{regex}\)
+{atom} = \\q\q{nonterminal}|\q{class}|\(\q{regex}\)
 {category} = Ll|Lu|Lt|Lm|Lo|Mn|Mc|Me|Nd|Nl|No|Pc|Pd|Ps|Pe|Pi|Pf|Po|Sm|Sc|Sk|So|Zs|Zl|Zp|Cc|Cf|Cs|Co|Cn
-{category-test} = (\\p\{)\q{category}\}|(\\P\{)(\q{category}(\|\q{category})*)\}
 {char} = [^\(\)\*\+\?\[\\\]\^\{\|\}\P{Cc}]|\\\q{char-escaped}
-{char-any} = \[\^\]
-{char-class} = \q{fail}|\q{char-any}|\q{one-of}|\q{not-one-of}|\q{category-test}
 {char-control} = NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|DEL|PAD|HOP|BPH|NBH|IND|NEL|SSA|ESA|HTS|HTJ|VTS|PLD|PLU|RI|SS2|SS3|DCS|PU1|PU2|STS|CCH|MW|SPA|EPA|SOS|SGCI|SCI|CSI|ST|OSC|PM|APC
 {char-escaped} = [\(\)\*\+\?\[\\\]\^\{\|\}]|\q{char-control}
+{class} = \q{class-one-of}|\q{class-not-one-of}
+{class-category} = \\p\{\q{category}\}|\\P\{(\q{category}(\|\q{category})*)\}
+{class-not-one-of} = \q{class-category}|\[\^\q{char}*(\q{class-category}?\])
+{class-one-of} = \q{char}|\[\q{char}*\]
 {expression} = \q{atom}\?|\q{atom}\*|\q{atom}\+|\q{atom}
-{fail} = \[\]
-{not-one-of} = (\[\^)\q{char}+(\q{category-test}?\])
-{one-of} = \[\q{char}+\]
+{nonterminal} = \{\q{char}*\}
 {regex} = \q{alternate}
-{sequence} = \q{char}*|\q{expression}*
+{sequence} = \q{expression}*
 -}
 regexGrammar :: Grammar Char RegString
 regexGrammar = _RegString >~ ruleRec "regex" altG
   where
     altG rex = rule "alternate" $
-      chain1 Left (_RegExam . _Alternate) (sepBy (terminal "|")) (seqG rex)
+      chain1 Left (_RegExam . _Alternate) (sepWith "|") (seqG rex)
 
-    seqG rex = rule "sequence" $ choice
-      [ _Terminal >? manyP charG
-      , chain Left _Sequence (_Terminal . _Empty) noSep (exprG rex)
-      ]
+    seqG rex = rule "sequence" $
+      chain Left _Sequence _SeqEmpty noSep (exprG rex)
 
     exprG rex = rule "expression" $ choice
       [ _KleeneOpt >? atomG rex *< terminal "?"
@@ -520,20 +602,11 @@ regexGrammar = _RegString >~ ruleRec "regex" altG
       ]
 
     atomG rex = rule "atom" $ choice
-      [ _NonTerminal >? terminal "\\q{" >* manyP charG *< terminal "}"
-      , _Terminal >? charG >:< asEmpty
+      [ _NonTerminal >? terminal "\\q" >* nonterminalG
       , _RegExam >? classG
       , terminal "(" >* rex *< terminal ")"
       ]
 
-    catTestG = rule "category-test" $ choice
-      [ _AsIn >? terminal "\\p{" >* categoryG *< terminal "}"
-      , _NotAsIn >? several1 (sepBy (terminal "|"))
-          { beginBy = terminal "\\P{"
-          , endBy = terminal "}"
-          } categoryG
-      ]
-
     categoryG = rule "category" $ choice
       [ _LowercaseLetter >? terminal "Ll"
       , _UppercaseLetter >? terminal "Lu"
@@ -567,24 +640,32 @@ regexGrammar = _RegString >~ ruleRec "regex" altG
       , _NotAssigned >? terminal "Cn"
       ]
 
-    classG = rule "char-class" $ choice
-      [ _Fail >? failG
-      , _Pass >? anyG
-      , _OneOf >? oneOfG
-      , _NotOneOf >? notOneOfG
-      , _NotOneOf >? pure Set.empty >*< catTestG
+    classG = rule "class" $ choice
+      [ _OneOf >? classOneOfG
+      , _NotOneOf >? classNotOneOfG
       ]
 
-    failG = rule "fail" $ terminal "[]"
+    classCatG = rule "class-category" $ choice
+      [ _AndAsIn >? terminal "\\p{" >* categoryG *< terminal "}"
+      , _AndNotAsIn >? several1
+          (sepWith "|" & beginWith "\\P{" & endWith "}")
+          categoryG
+      ]
 
-    anyG = rule "char-any" $ terminal "[^]"
+    classOneOfG = rule "class-one-of" $ choice
+      [ onlyOne charG
+      , terminal "[" >* several noSep charG *< terminal "]"
+      ]
 
-    oneOfG = rule "one-of" $ terminal "[" >* several1 noSep charG *< terminal "]"
+    classNotOneOfG = rule "class-not-one-of" $ choice
+      [ asEmpty >*< classCatG
+      , terminal "[^" >* several noSep charG >*<
+          optionP (_AndNotAsIn . _Empty) classCatG *< terminal "]"
+      ]
 
-    notOneOfG = rule "not-one-of" $
-      terminal "[^" >* several1 noSep charG
-        >*< option (NotAsIn Set.empty) catTestG
-        *< terminal "]"
+nonterminalG :: Grammar Char String
+nonterminalG = rule "nonterminal" $
+  terminal "{" >* manyP charG *< terminal "}"
 
 charG :: Grammar Char Char
 charG = rule "char" $
@@ -671,30 +752,26 @@ That means that it can generate a self-hosted definition.
 >>> putStringLn (regbnfG regbnfGrammar)
 {start} = \q{regbnf}
 {alternate} = \q{sequence}(\|\q{sequence})*
-{atom} = (\\q\{)\q{char}*\}|\q{char}|\q{char-class}|\(\q{regex}\)
+{atom} = \\q\q{nonterminal}|\q{class}|\(\q{regex}\)
 {category} = Ll|Lu|Lt|Lm|Lo|Mn|Mc|Me|Nd|Nl|No|Pc|Pd|Ps|Pe|Pi|Pf|Po|Sm|Sc|Sk|So|Zs|Zl|Zp|Cc|Cf|Cs|Co|Cn
-{category-test} = (\\p\{)\q{category}\}|(\\P\{)(\q{category}(\|\q{category})*)\}
 {char} = [^\(\)\*\+\?\[\\\]\^\{\|\}\P{Cc}]|\\\q{char-escaped}
-{char-any} = \[\^\]
-{char-class} = \q{fail}|\q{char-any}|\q{one-of}|\q{not-one-of}|\q{category-test}
 {char-control} = NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|DEL|PAD|HOP|BPH|NBH|IND|NEL|SSA|ESA|HTS|HTJ|VTS|PLD|PLU|RI|SS2|SS3|DCS|PU1|PU2|STS|CCH|MW|SPA|EPA|SOS|SGCI|SCI|CSI|ST|OSC|PM|APC
 {char-escaped} = [\(\)\*\+\?\[\\\]\^\{\|\}]|\q{char-control}
+{class} = \q{class-one-of}|\q{class-not-one-of}
+{class-category} = \\p\{\q{category}\}|\\P\{(\q{category}(\|\q{category})*)\}
+{class-not-one-of} = \q{class-category}|\[\^\q{char}*(\q{class-category}?\])
+{class-one-of} = \q{char}|\[\q{char}*\]
 {expression} = \q{atom}\?|\q{atom}\*|\q{atom}\+|\q{atom}
-{fail} = \[\]
-{not-one-of} = (\[\^)\q{char}+(\q{category-test}?\])
-{one-of} = \[\q{char}+\]
-{regbnf} = (\{start\} = )\q{regex}(\LF\q{rule})*
+{nonterminal} = \{\q{char}*\}
+{regbnf} = \{start\} = \q{regex}(\LF\q{nonterminal}( = )\q{regex})*
 {regex} = \q{alternate}
-{rule} = \{\q{char}*(\} = )\q{regex}
-{sequence} = \q{char}*|\q{expression}*
+{sequence} = \q{expression}*
 -}
 regbnfGrammar :: Grammar Char RegBnf
 regbnfGrammar = rule "regbnf" $ _RegBnf . _Bnf >~
-  terminal "{start} = " >* regexGrammar
-    >*< several noSep (terminal "\n" >* ruleG)
-  where
-    ruleG = rule "rule" $ terminal "{" >* manyP charG *< terminal "} = "
-      >*< regexGrammar
+  terminal "{start} = " >* regexGrammar >*< several noSep
+    (terminal "\n" >* nonterminalG *< terminal " = " >*< regexGrammar)
+      
 
 {- | `regstringG` generates a `RegString` from a regular grammar.
 Since context-free `Grammar`s and `CtxGrammar`s aren't necessarily regular,
@@ -727,7 +804,7 @@ printG
   -> m (string -> string)
 printG printor = printP printor
 
-{- | `parseG` generates a parser from a `CtxGrammar`.
+{- | `parseG` generates a parser from a @LL(∞)@ `CtxGrammar`.
 Since both `RegGrammar`s and context-free `Grammar`s are `CtxGrammar`s,
 the type system will allow `parseG` to be applied to them.
 Running the parser on an input string value `uncons`es
@@ -743,10 +820,10 @@ parseG
   -> m (a, string)
 parseG parsor = parseP parsor
 
-{- | `unparseG` generates an unparser from a `CtxGrammar`.
+{- | `unparseG` generates a printer from a @LL(∞)@ `CtxGrammar`.
 Since both `RegGrammar`s and context-free `Grammar`s are `CtxGrammar`s,
 the type system will allow `unparseG` to be applied to them.
-Running the unparser on a syntax value and an input string
+Running the printer on a syntax value and an input string
 `snoc`s tokens at the end of the string, from left to right,
 returning the output string.
 -}
@@ -760,6 +837,41 @@ unparseG
   -> m string
 unparseG parsor = unparseP parsor
 
+{- | `parsecG` generates a parser from a @LL(1)@ `CtxGrammar`,
+with `try` for restoring full @LL(∞)@ lookahead.
+Since both `RegGrammar`s and context-free `Grammar`s are `CtxGrammar`s,
+the type system will allow `parsecG` to be applied to them.
+Running the parser on an input string value `uncons`es
+tokens from the beginning of an input string from left to right,
+returning a `parsecResult` which is a `ParsecError` or a syntax value,
+and a remaining output `parsecStream`.
+-}
+parsecG
+  :: (Cons string string token token, Snoc string string token token)
+  => (Item string ~ token, Categorized token)
+  => CtxGrammar token a
+  -> string {- ^ input -}
+  -> ParsecState string a
+parsecG parsector = parsecP parsector
+
+{- | `unparsecG` generates a printer from a @LL(1)@ `CtxGrammar`,
+with `try` for restoring full @LL(∞)@ lookahead.
+Since both `RegGrammar`s and context-free `Grammar`s are `CtxGrammar`s,
+the type system will allow `unparsecG` to be applied to them.
+Running the printer on a syntax value and an input string
+`snoc`s tokens at the end of the string, from left to right,
+returning a `parsecResult` which is a `ParsecError`
+or the input syntax value, and a remaining output `parsecStream`.
+-}
+unparsecG
+  :: (Cons string string token token, Snoc string string token token)
+  => (Item string ~ token, Categorized token)
+  => CtxGrammar token a
+  -> a {- ^ syntax -}
+  -> string {- ^ input -}
+  -> ParsecState string a
+unparsecG parsector = unparsecP parsector
+
 {- | `putStringLn` is a utility that generalizes `putStrLn`
 to string-like interfaces such as `RegString` and `RegBnf`.
 -}
diff --git a/src/Control/Lens/Grammar/BackusNaur.hs b/src/Control/Lens/Grammar/BackusNaur.hs
index 8beba91..79bdbe6 100644
--- a/src/Control/Lens/Grammar/BackusNaur.hs
+++ b/src/Control/Lens/Grammar/BackusNaur.hs
@@ -26,7 +26,6 @@ module Control.Lens.Grammar.BackusNaur
 
 import Control.Lens
 import Control.Lens.Extras
-import Control.Lens.Grammar.Boole
 import Control.Lens.Grammar.Kleene
 import Control.Lens.Grammar.Token
 import Control.Lens.Grammar.Symbol
@@ -38,16 +37,18 @@ import qualified Data.Set as Set
 import Data.Set (Set)
 
 {- | `BackusNaurForm` grammar combinators formalize
-`rule` abstraction and general recursion. Context-free
-`Control.Lens.Grammar.Grammar`s support the `BackusNaurForm` interface.
+`rule` abstraction and general recursion. Both Context-free
+`Control.Lens.Grammar.Grammar`s & `Control.Lens.Grammar.CtxGrammar`s
+support the `BackusNaurForm` interface.
+
+prop> rule name bnf = ruleRec name (\_ -> bnf)
+
+See Breitner, [Showcasing Applicative]
+(https://www.joachim-breitner.de/blog/710-Showcasing_Applicative)
 -}
 class BackusNaurForm bnf where
 
-  {- | For a `BackusNaurForm` parser instance,
-  `rule` can be used to detail parse errors.
-
-  prop> rule name bnf = ruleRec name (\_ -> bnf)
-  -}
+  {- | Rule abstraction, `rule` can be used to detail parse errors. -}
   rule :: String -> bnf -> bnf
   rule _ = id
 
@@ -97,9 +98,7 @@ diffB prefix (Bnf start rules) =
   where
     -- derivative wrt 1 token, memoized
     diff1B = memo2 $ \x -> \case
-      Terminal [] -> zeroK
-      Terminal (tokenY:streamY) ->
-        if x == tokenY then terminal streamY else zeroK
+      SeqEmpty -> zeroK
       NonTerminal nameY -> anyK (diff1B x) (rulesNamed nameY rules)
       Sequence y1 y2 ->
         if δ (Bnf y1 rules) then y1'y2 >|< y1y2' else y1'y2
@@ -109,14 +108,12 @@ diffB prefix (Bnf start rules) =
       KleeneStar y -> diff1B x y <> starK y
       KleeneOpt y -> diff1B x y
       KleenePlus y -> diff1B x y <> starK y
-      RegExam Fail -> zeroK
-      RegExam Pass -> mempty
       RegExam (OneOf chars) ->
         if x `elem` chars then mempty else zeroK
-      RegExam (NotOneOf chars (AsIn cat)) ->
+      RegExam (NotOneOf chars (AndAsIn cat)) ->
         if elem x chars || categorize x /= cat
           then zeroK else mempty
-      RegExam (NotOneOf chars (NotAsIn cats)) ->
+      RegExam (NotOneOf chars (AndNotAsIn cats)) ->
         if elem x chars || elem (categorize x) cats
           then zeroK else mempty
       RegExam (Alternate y1 y2) -> diff1B x y1 >|< diff1B x y2
@@ -126,7 +123,7 @@ diffB prefix (Bnf start rules) =
   => Bnf (RegEx token) -> Bool
 δ (Bnf start rules) = ν start where
   ν = memo $ \case
-    Terminal [] -> True
+    SeqEmpty -> True
     KleeneStar _ -> True
     KleeneOpt _ -> True
     KleenePlus y -> ν y
diff --git a/src/Control/Lens/Grammar/Boole.hs b/src/Control/Lens/Grammar/Boole.hs
index f5a5cef..5b6409d 100644
--- a/src/Control/Lens/Grammar/Boole.hs
+++ b/src/Control/Lens/Grammar/Boole.hs
@@ -16,20 +16,10 @@ module Control.Lens.Grammar.Boole
   ( -- * BooleanAlgebra
     BooleanAlgebra (..)
   , andB, orB, allB, anyB
-    -- * TokenAlgebra
-  , TokenAlgebra (..)
-  , TokenTest (..)
   ) where
 
-import Control.Applicative
-import Control.Lens.Grammar.Kleene
-import Control.Lens.Grammar.Token
 import Data.Foldable
 import Data.Monoid
-import Data.Profunctor
-import Data.Profunctor.Distributor
-import qualified Data.Set as Set
-import GHC.Generics
 
 -- | A `BooleanAlgebra`, like `Bool`, supporting classical logical operations.
 class BooleanAlgebra b where
@@ -52,159 +42,41 @@ class BooleanAlgebra b where
     :: (b ~ f bool, BooleanAlgebra bool, Functor f) => b -> b
   notB = fmap notB
 
-  -- | inclusion
-  fromBool :: Bool -> b
-  default fromBool
-    :: (b ~ f bool, BooleanAlgebra bool, Applicative f) => Bool -> b
-  fromBool = pure . fromBool
+  -- | true
+  trueB :: b
+  default trueB
+    :: (b ~ f bool, BooleanAlgebra bool, Applicative f) => b
+  trueB = pure trueB
+
+  -- | false
+  falseB :: b
+  default falseB
+    :: (b ~ f bool, BooleanAlgebra bool, Applicative f) => b
+  falseB = pure falseB
 
 -- | cumulative conjunction
 andB :: (Foldable f, BooleanAlgebra b) => f b -> b
-andB = foldl' (>&&<) (fromBool True)
+andB = foldl' (>&&<) trueB
 
 -- | cumulative disjunction
 orB :: (Foldable f, BooleanAlgebra b) => f b -> b
-orB = foldl' (>||<) (fromBool False)
+orB = foldl' (>||<) falseB
 
 -- | universal
 allB :: (Foldable f, BooleanAlgebra b) => (a -> b) -> f a -> b
-allB f = foldl' (\b a -> b >&&< f a) (fromBool True)
+allB f = foldl' (\b a -> b >&&< f a) trueB
 
 -- | existential
 anyB :: (Foldable f, BooleanAlgebra b) => (a -> b) -> f a -> b
-anyB f = foldl' (\b a -> b >||< f a) (fromBool False)
-
--- | `TokenTest` forms a closed `Tokenized` `BooleanAlgebra`
--- of `Categorized` `tokenClass`es.
-newtype TokenTest token = TokenTest (RegExam token (TokenTest token))
-
--- | `TokenAlgebra` extends `Tokenized` methods to support
--- `BooleanAlgebra` operations in a `tokenClass`
-class Tokenized token p => TokenAlgebra token p where
-  -- | Arguments of `tokenClass` can be constructed from
-  -- `Tokenized` and `BooleanAlgebra` methods.
-  tokenClass :: TokenTest token -> p
-  default tokenClass
-    :: (p ~ q token token, Alternator q, Cochoice q)
-    => TokenTest token -> p
-  tokenClass (TokenTest exam) = case exam of
-    Fail -> empty
-    Pass -> anyToken
-    OneOf chars -> oneOf chars
-    NotOneOf chars (AsIn cat) ->
-      satisfy (notOneOf chars >&&< asIn cat)
-    NotOneOf chars (NotAsIn cats) ->
-      satisfy (notOneOf chars >&&< allB notAsIn cats)
-    Alternate exam1 exam2 -> tokenClass exam1 <|> tokenClass exam2
+anyB f = foldl' (\b a -> b >||< f a) falseB
 
 --instances
 instance BooleanAlgebra (x -> Bool)
-instance Categorized token => TokenAlgebra token (token -> Bool) where
-  tokenClass (TokenTest exam) = case exam of
-    Fail -> const False
-    Pass -> const True
-    OneOf chars -> oneOf chars
-    NotOneOf chars (AsIn cat) -> notOneOf chars >&&< asIn cat
-    NotOneOf chars (NotAsIn cats) -> notOneOf chars >&&< allB notAsIn cats
-    Alternate exam1 exam2 -> tokenClass exam1 >||< tokenClass exam2
 instance (Applicative f, BooleanAlgebra bool)
   => BooleanAlgebra (Ap f bool)
-deriving stock instance Generic (TokenTest token)
-deriving stock instance
-  (Categorized token, Read token, Read (Categorize token))
-    => Read (TokenTest token)
-deriving stock instance
-  (Categorized token, Show token, Show (Categorize token))
-    => Show (TokenTest token)
 instance BooleanAlgebra Bool where
-  fromBool = id
+  falseB = False
+  trueB = True
   notB = not
   (>&&<) = (&&)
   (>||<) = (||)
-deriving newtype instance Categorized token
-  => Eq (TokenTest token)
-deriving newtype instance Categorized token
-  => Ord (TokenTest token)
-deriving newtype instance Categorized token
-  => BooleanAlgebra (TokenTest token)
-deriving newtype instance Categorized token
-  => Tokenized token (TokenTest token)
-instance Categorized token
-  => TokenAlgebra token (RegEx token) where
-  tokenClass (TokenTest tokenExam) = case tokenExam of
-    Fail -> RegExam Fail
-    Pass -> RegExam Pass
-    OneOf as -> RegExam (OneOf as)
-    NotOneOf as catTest -> RegExam (NotOneOf as catTest)
-    Alternate exam1 exam2 ->
-      RegExam (Alternate (tokenClass exam1) (tokenClass exam2))
-instance Categorized token
-  => BooleanAlgebra (RegExam token (TokenTest token)) where
-  fromBool = \case
-    False -> Fail
-    True -> Pass
-  notB Fail = Pass
-  notB Pass = Fail
-  notB (Alternate (TokenTest x) (TokenTest y)) = notB x >&&< notB y
-  notB (OneOf xs) = notOneOf xs
-  notB (NotOneOf xs (AsIn y)) = oneOf xs >||< notAsIn y
-  notB (NotOneOf xs (NotAsIn ys)) = oneOf xs >||< anyB asIn ys
-  _ >&&< Fail = Fail
-  Fail >&&< _ = Fail
-  x >&&< Pass = x
-  Pass >&&< y = y
-  x >&&< Alternate (TokenTest y) (TokenTest z) = (x >&&< y) >||< (x >&&< z)
-  Alternate (TokenTest x) (TokenTest y) >&&< z = (x >&&< z) >||< (y >&&< z)
-  OneOf xs >&&< OneOf ys = OneOf (Set.intersection xs ys)
-  OneOf xs >&&< NotOneOf ys (AsIn z) = OneOf
-    (Set.filter (\x -> categorize x == z) (Set.difference xs ys))
-  NotOneOf xs (AsIn y) >&&< OneOf zs = OneOf
-    (Set.filter (\z -> categorize z == y) (Set.difference zs xs))
-  OneOf xs >&&< NotOneOf ys (NotAsIn zs) = OneOf
-    (Set.filter (\x -> categorize x `notElem` zs) (Set.difference xs ys))
-  NotOneOf xs (NotAsIn ys) >&&< OneOf zs = OneOf
-    (Set.filter (\z -> categorize z `notElem` ys) (Set.difference zs xs))
-  NotOneOf xs (AsIn y) >&&< NotOneOf ws (AsIn z) =
-    if y /= z then Fail else NotOneOf
-      (Set.filter (\x -> categorize x == y)
-      (Set.union xs ws)) (AsIn y)
-  NotOneOf xs (AsIn y) >&&< NotOneOf ws (NotAsIn zs) =
-    if y `elem` zs then Fail else NotOneOf
-      (Set.filter (\x -> categorize x == y)
-      (Set.union xs ws)) (AsIn y)
-  NotOneOf xs (NotAsIn ys) >&&< NotOneOf ws (AsIn z) =
-    if z `elem` ys then Fail else NotOneOf
-      (Set.filter (\x -> categorize x == z) (Set.union xs ws))
-      (AsIn z)
-  NotOneOf xs (NotAsIn ys) >&&< NotOneOf ws (NotAsIn zs) =
-    let
-      xws = Set.union xs ws
-      yzs = Set.union ys zs
-    in
-      NotOneOf
-        (Set.filter (\x -> categorize x `notElem` yzs) xws)
-        (NotAsIn yzs)
-  x >||< Fail = x
-  Fail >||< y = y
-  _ >||< Pass = Pass
-  Pass >||< _ = Pass
-  x >||< Alternate y z = Alternate (TokenTest x) (TokenTest (Alternate y z))
-  Alternate x y >||< z = Alternate (TokenTest (Alternate x y)) (TokenTest z)
-  OneOf xs >||< OneOf ys = oneOf (Set.union xs ys)
-  OneOf xs >||< NotOneOf ys z =
-    Alternate (TokenTest (OneOf xs)) (TokenTest (NotOneOf ys z))
-  NotOneOf xs y >||< OneOf zs =
-    Alternate (TokenTest (NotOneOf xs y)) (TokenTest (OneOf zs))
-  NotOneOf xs (NotAsIn ys) >||< NotOneOf ws (NotAsIn zs) =
-    notOneOf (Set.intersection xs ws) >&&< allB notAsIn (Set.intersection ys zs)
-  NotOneOf xs (AsIn y) >||< NotOneOf ws (AsIn z) =
-    if y == z then NotOneOf (Set.intersection xs ws) (AsIn y)
-    else Alternate
-      (TokenTest (NotOneOf xs (AsIn y)))
-      (TokenTest (NotOneOf ws (AsIn z)))
-  NotOneOf xs (NotAsIn ys) >||< NotOneOf ws (AsIn z) = Alternate
-    (TokenTest (NotOneOf xs (NotAsIn ys)))
-    (TokenTest (NotOneOf ws (AsIn z)))
-  NotOneOf xs (AsIn y) >||< NotOneOf ws (NotAsIn zs) = Alternate
-    (TokenTest (NotOneOf xs (AsIn y)))
-    (TokenTest (NotOneOf ws (NotAsIn zs)))
diff --git a/src/Control/Lens/Grammar/Kleene.hs b/src/Control/Lens/Grammar/Kleene.hs
index f13a1f5..2139221 100644
--- a/src/Control/Lens/Grammar/Kleene.hs
+++ b/src/Control/Lens/Grammar/Kleene.hs
@@ -16,25 +16,30 @@ module Control.Lens.Grammar.Kleene
   ( -- * KleeneStarAlgebra
     KleeneStarAlgebra (..)
   , orK, anyK
-    -- * RegEx
+    -- * TokenAlgebra
+  , TokenAlgebra (..)
+    -- * RegEx & TokenClass
   , RegEx (..)
+  , TokenClass (..)
   , RegExam (..)
   , CategoryTest (..)
   ) where
 
 import Control.Applicative
+import Control.Lens.Grammar.Boole
 import Control.Lens.Grammar.Symbol
 import Control.Lens.Grammar.Token
 import Data.Foldable
 import Data.MemoTrie
 import Data.Monoid
 import Data.Profunctor
+import Data.Profunctor.Distributor
 import Data.Set (Set)
 import qualified Data.Set as Set
 import GHC.Generics
 
 {- | A `KleeneStarAlgebra` is a ring
-with a generally non-commutaive multiplication,
+with a generally non-commutative multiplication,
 the `Monoid` concatenation operator `<>` with identity `mempty`;
 and an idempotent addition, the alternation operator `>|<`
 with identity `zeroK`.
@@ -45,6 +50,14 @@ 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
+
 -}
 class Monoid k => KleeneStarAlgebra k where
   starK, plusK, optK :: k -> k
@@ -63,41 +76,95 @@ class Monoid k => KleeneStarAlgebra k where
 orK :: (Foldable f, KleeneStarAlgebra k) => f k -> k
 orK = foldl' (>|<) zeroK
 
--- | universal
+-- | existential
 anyK :: (Foldable f, KleeneStarAlgebra k) => (a -> k) -> f a -> k
 anyK f = foldl' (\b a -> b >|< f a) zeroK
 
--- | The `RegEx`pression type is the prototypical `KleeneStarAlgebra`.
+{- | 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)
+
+-}
 data RegEx token
-  = Terminal [token]
-  | NonTerminal String
+  = SeqEmpty
   | Sequence (RegEx token) (RegEx token)
+  | NonTerminal String
   | KleeneStar (RegEx token)
   | KleeneOpt (RegEx token)
   | KleenePlus (RegEx token)
   | RegExam (RegExam token (RegEx token))
 
-{- | A component of both `RegEx`pressions
-and `Control.Lens.Grammar.Boole.TokenTest`s, so that the latter can
-be embedded in the former with `Control.Lens.Grammar.Boole.tokenClass`.
+{- | A component of both `RegEx`pressions and `TokenClass`es,
+so that the latter can be embedded in the former with `tokenClass`.
 -}
 data RegExam token alg
-  = Fail
-  | Pass
-  | OneOf (Set token)
+  = OneOf (Set token)
   | NotOneOf (Set token) (CategoryTest token)
   | Alternate alg alg
 
+failExam :: RegExam token alg
+failExam = OneOf Set.empty
+
+passExam :: RegExam token alg
+passExam = NotOneOf Set.empty (AndNotAsIn Set.empty)
+
+isFailExam :: RegExam token alg -> Bool
+isFailExam (OneOf xs) = Set.null xs
+isFailExam _ = False
+
+isPassExam :: RegExam token alg -> Bool
+isPassExam (NotOneOf xs (AndNotAsIn ys)) = Set.null xs && Set.null ys
+isPassExam _ = False
+
 {- | `CategoryTest`s for `Categorized` tokens.-}
 data CategoryTest token
-  = AsIn (Categorize token)
-  | NotAsIn (Set (Categorize token))
+  = AndAsIn (Categorize token)
+  | AndNotAsIn (Set (Categorize token))
+
+{- | `TokenClass` forms a `Tokenized` `BooleanAlgebra`,
+such that the following invariants hold.
+
+prop> trueB = anyToken
+prop> trueB = notOneOf []
+prop> falseB = oneOf []
+prop> notB . oneOf = notOneOf
+prop> notB . notOneOf = oneOf
+prop> notB . asIn = notAsIn
+prop> notB . notAsIn = asIn
+
+-}
+newtype TokenClass token = TokenClass (RegExam token (TokenClass token))
+
+{- | `TokenAlgebra` extends `Tokenized` methods to support
+`BooleanAlgebra` operations within a `tokenClass`.
+When a `TokenAlgebra` is an `Alternative`,
+then `tokenClass` is expected to act homomorphically on disjunction.
+
+prop> empty = tokenClass falseB
+prop> tokenClass x <|> tokenClass y = tokenClass (x >||< y)
+
+-}
+class Tokenized token p => TokenAlgebra token p where
+  tokenClass :: TokenClass token -> p
+  default tokenClass
+    :: (p ~ q token token, Alternator q, Cochoice q)
+    => TokenClass token -> p
+  tokenClass (TokenClass exam) = case exam of
+    OneOf chars -> oneOf chars
+    NotOneOf chars (AndAsIn cat) ->
+      satisfy (notOneOf chars >&&< asIn cat)
+    NotOneOf chars (AndNotAsIn cats) ->
+      satisfy (notOneOf chars >&&< allB notAsIn cats)
+    Alternate exam1 exam2 -> tokenClass exam1 <|> tokenClass exam2
 
 --instances
 instance (Alternative f, Monoid k) => KleeneStarAlgebra (Ap f k)
 deriving stock instance Generic (RegEx token)
 deriving stock instance Generic (RegExam token alg)
 deriving stock instance Generic1 (RegExam token)
+deriving stock instance Generic (TokenClass token)
 deriving stock instance Generic (CategoryTest token)
 deriving stock instance Categorized token => Eq (RegEx token)
 deriving stock instance Categorized token => Ord (RegEx token)
@@ -107,67 +174,163 @@ deriving stock instance
 deriving stock instance
   (Categorized token, Show token, Show (Categorize token))
     => Show (RegEx token)
-instance TerminalSymbol token (RegEx token) where
-  terminal = Terminal . toList
+deriving stock instance
+  (Categorized token, Read token, Read (Categorize token))
+    => Read (TokenClass token)
+deriving stock instance
+  (Categorized token, Show token, Show (Categorize token))
+    => Show (TokenClass token)
+deriving newtype instance Categorized token => Eq (TokenClass token)
+deriving newtype instance Categorized token => Ord (TokenClass token)
+deriving newtype instance Categorized token => Tokenized token (TokenClass token)
+deriving newtype instance Categorized token => BooleanAlgebra (TokenClass token)
+instance Categorized token
+  => TokenAlgebra token (TokenClass token) where
+  tokenClass = id
+instance Categorized token
+  => TokenAlgebra token (RegExam token (TokenClass token)) where
+  tokenClass (TokenClass exam) = exam
+instance Categorized token => TerminalSymbol token (RegEx token) where
+  terminal = foldl (\acc t -> acc <> token t) mempty
 instance NonTerminalSymbol (RegEx token) where
   nonTerminal = NonTerminal
 instance Categorized token => Tokenized token (RegEx token) where
-  anyToken = RegExam Pass
-  token a = Terminal [a]
-  oneOf as | null as = RegExam Fail
-  oneOf as | length as == 1 = Terminal (toList as)
-  oneOf as = RegExam (OneOf (foldr Set.insert Set.empty as))
-  notOneOf as | null as = RegExam Pass
-  notOneOf as = RegExam
-    (NotOneOf (foldr Set.insert Set.empty as) (NotAsIn Set.empty))
-  asIn cat = RegExam (NotOneOf Set.empty (AsIn cat))
-  notAsIn cat = RegExam
-    (NotOneOf Set.empty (NotAsIn (Set.singleton cat)))
+  anyToken = RegExam passExam
+  token a = RegExam (OneOf (Set.singleton a))
+  oneOf as = RegExam (OneOf (Set.fromList (toList as)))
+  notOneOf as =
+    RegExam (NotOneOf (Set.fromList (toList as)) (AndNotAsIn Set.empty))
+  asIn cat = RegExam (NotOneOf Set.empty (AndAsIn cat))
+  notAsIn cat = RegExam (NotOneOf Set.empty (AndNotAsIn (Set.singleton cat)))
+instance Categorized token => TokenAlgebra token (token -> Bool) where
+  tokenClass (TokenClass exam) x = case exam of
+    OneOf xs -> Set.member x xs
+    NotOneOf xs (AndAsIn y) ->
+      Set.notMember x xs && categorize x == y
+    NotOneOf xs (AndNotAsIn ys) ->
+      Set.notMember x xs && Set.notMember (categorize x) ys
+    Alternate exam1 exam2 ->
+      tokenClass exam1 x || tokenClass exam2 x
+instance Categorized token => TokenAlgebra token (RegEx token) where
+  tokenClass (TokenClass exam) = case exam of
+    OneOf as -> RegExam (OneOf as)
+    NotOneOf as catTest -> RegExam (NotOneOf as catTest)
+    Alternate exam1 exam2 ->
+      RegExam (Alternate (tokenClass exam1) (tokenClass exam2))
+instance Categorized token => Monoid (RegEx token) where
+  mempty = SeqEmpty
 instance Categorized token => Semigroup (RegEx token) where
-  Terminal [] <> rex = rex
-  rex <> Terminal [] = rex
-  RegExam Fail <> _ = zeroK
-  _ <> RegExam Fail = zeroK
-  Terminal str0 <> Terminal str1 = Terminal (str0 <> str1)
-  KleeneStar rex0 <> rex1
-    | rex0 == rex1 = plusK rex0
-  rex0 <> KleeneStar rex1
-    | rex0 == rex1 = plusK rex1
+  SeqEmpty <> rex = rex
+  rex <> SeqEmpty = rex
+  RegExam exam <> _ | isFailExam exam = zeroK
+  _ <> RegExam exam | isFailExam exam = zeroK
+  KleeneStar rex0 <> rex1 | rex0 == rex1 = plusK rex0
+  rex0 <> KleeneStar rex1 | rex0 == rex1 = plusK rex1
   rex0 <> rex1 = Sequence rex0 rex1
-instance Categorized token => Monoid (RegEx token) where
-  mempty = Terminal []
 instance Categorized token => KleeneStarAlgebra (RegEx token) where
-  zeroK = RegExam Fail
-  optK (RegExam Fail) = mempty
-  optK (Terminal []) = mempty
+  zeroK = RegExam failExam
+  optK (RegExam exam) | isFailExam exam = mempty
+  optK SeqEmpty = mempty
   optK (KleenePlus rex) = starK rex
   optK rex = KleeneOpt rex
-  starK (RegExam Fail) = mempty
-  starK (Terminal []) = mempty
+  starK (RegExam exam) | isFailExam exam = mempty
+  starK SeqEmpty = mempty
   starK rex = KleeneStar rex
-  plusK (RegExam Fail) = zeroK
-  plusK (Terminal []) = mempty
+  plusK (RegExam exam) | isFailExam exam = zeroK
+  plusK SeqEmpty = mempty
   plusK rex = KleenePlus rex
-  KleenePlus rex >|< Terminal [] = starK rex
-  Terminal [] >|< KleenePlus rex = starK rex
-  rex >|< Terminal [] = optK rex
-  Terminal [] >|< rex = optK rex
-  rex >|< RegExam Fail = rex
-  RegExam Fail >|< rex = rex
   rex0 >|< rex1 | rex0 == rex1 = rex0
+  KleenePlus rex >|< SeqEmpty = starK rex
+  SeqEmpty >|< KleenePlus rex = starK rex
+  rex >|< SeqEmpty = optK rex
+  SeqEmpty >|< rex = optK rex
+  rex >|< RegExam exam | isFailExam exam = rex
+  RegExam exam >|< rex | isFailExam exam = rex
+  rex0 >|< rex1 | Just tokenOr <- maybeOr = tokenClass tokenOr
+    where
+      toTokenClass (RegExam exam) =
+        TokenClass <$> traverse toTokenClass exam
+      toTokenClass _ = Nothing
+      maybeOr = (>||<) <$> toTokenClass rex0 <*> toTokenClass rex1
   rex0 >|< rex1 = RegExam (Alternate rex0 rex1)
-instance Categorized token
-  => Tokenized token (RegExam token alg) where
-  anyToken = Pass
+instance Categorized token => Tokenized token (RegExam token alg) where
+  anyToken = passExam
   token a = OneOf (Set.singleton a)
-  oneOf as | null as = Fail
+  oneOf as | null as = failExam
   oneOf as = OneOf (Set.fromList (toList as))
-  notOneOf as | null as = Pass
+  notOneOf as | null as = passExam
   notOneOf as =
-    NotOneOf (Set.fromList (toList as)) (NotAsIn Set.empty)
-  asIn cat = NotOneOf Set.empty (AsIn cat)
-  notAsIn cat =
-    NotOneOf Set.empty (NotAsIn (Set.singleton cat))
+    NotOneOf (Set.fromList (toList as)) (AndNotAsIn Set.empty)
+  asIn cat = NotOneOf Set.empty (AndAsIn cat)
+  notAsIn cat = NotOneOf Set.empty (AndNotAsIn (Set.singleton cat))
+instance Categorized token
+  => BooleanAlgebra (RegExam token (TokenClass token)) where
+  falseB = failExam
+  trueB = passExam
+  notB exam | isFailExam exam = passExam
+  notB exam | isPassExam exam = failExam
+  notB (Alternate (TokenClass x) (TokenClass y)) = notB x >&&< notB y
+  notB (OneOf xs) = notOneOf xs
+  notB (NotOneOf xs (AndAsIn y)) = oneOf xs >||< notAsIn y
+  notB (NotOneOf xs (AndNotAsIn ys)) = oneOf xs >||< anyB asIn ys
+  x >&&< y | x == y = x
+  _ >&&< exam | isFailExam exam = failExam
+  exam >&&< _ | isFailExam exam = failExam
+  x >&&< exam | isPassExam exam = x
+  exam >&&< z | isPassExam exam = z
+  x >&&< Alternate (TokenClass y) (TokenClass z) = (x >&&< y) >||< (x >&&< z)
+  Alternate (TokenClass x) (TokenClass y) >&&< z = (x >&&< z) >||< (y >&&< z)
+  OneOf xs >&&< OneOf ys = OneOf (Set.intersection xs ys)
+  OneOf xs >&&< NotOneOf ys (AndAsIn z) = OneOf
+    (Set.filter (\x -> categorize x == z) (Set.difference xs ys))
+  NotOneOf xs (AndAsIn y) >&&< OneOf zs = OneOf
+    (Set.filter (\z -> categorize z == y) (Set.difference zs xs))
+  OneOf xs >&&< NotOneOf ys (AndNotAsIn zs) = OneOf
+    (Set.filter (\x -> categorize x `notElem` zs) (Set.difference xs ys))
+  NotOneOf xs (AndNotAsIn ys) >&&< OneOf zs = OneOf
+    (Set.filter (\z -> categorize z `notElem` ys) (Set.difference zs xs))
+  NotOneOf xs (AndAsIn y) >&&< NotOneOf ws (AndAsIn z) =
+    if y /= z then failExam else NotOneOf
+      (Set.filter (\x -> categorize x == y) (Set.union xs ws)) (AndAsIn y)
+  NotOneOf xs (AndAsIn y) >&&< NotOneOf ws (AndNotAsIn zs) =
+    if y `elem` zs then failExam else NotOneOf
+      (Set.filter (\x -> categorize x == y) (Set.union xs ws)) (AndAsIn y)
+  NotOneOf xs (AndNotAsIn ys) >&&< NotOneOf ws (AndAsIn z) =
+    if z `elem` ys then failExam else NotOneOf
+      (Set.filter (\x -> categorize x == z) (Set.union xs ws)) (AndAsIn z)
+  NotOneOf xs (AndNotAsIn ys) >&&< NotOneOf ws (AndNotAsIn zs) =
+    let
+      xws = Set.union xs ws
+      yzs = Set.union ys zs
+    in
+      NotOneOf
+        (Set.filter (\x -> categorize x `notElem` yzs) xws)
+        (AndNotAsIn yzs)
+  x >||< y | x == y = x
+  x >||< exam | isFailExam exam = x
+  exam >||< y | isFailExam exam = y
+  _ >||< exam | isPassExam exam = passExam
+  exam >||< _ | isPassExam exam = passExam
+  x >||< Alternate y z = Alternate (TokenClass x) (TokenClass (Alternate y z))
+  Alternate x y >||< z = Alternate (TokenClass (Alternate x y)) (TokenClass z)
+  OneOf xs >||< OneOf ys = oneOf (Set.union xs ys)
+  OneOf xs >||< NotOneOf ys z =
+    Alternate (TokenClass (OneOf xs)) (TokenClass (NotOneOf ys z))
+  NotOneOf xs y >||< OneOf zs =
+    Alternate (TokenClass (NotOneOf xs y)) (TokenClass (OneOf zs))
+  NotOneOf xs (AndNotAsIn ys) >||< NotOneOf ws (AndNotAsIn zs) =
+    notOneOf (Set.intersection xs ws) >&&< allB notAsIn (Set.intersection ys zs)
+  NotOneOf xs (AndAsIn y) >||< NotOneOf ws (AndAsIn z) =
+    if y == z then NotOneOf (Set.intersection xs ws) (AndAsIn y)
+    else Alternate
+      (TokenClass (NotOneOf xs (AndAsIn y)))
+      (TokenClass (NotOneOf ws (AndAsIn z)))
+  NotOneOf xs (AndNotAsIn ys) >||< NotOneOf ws (AndAsIn z) = Alternate
+    (TokenClass (NotOneOf xs (AndNotAsIn ys)))
+    (TokenClass (NotOneOf ws (AndAsIn z)))
+  NotOneOf xs (AndAsIn y) >||< NotOneOf ws (AndNotAsIn zs) = Alternate
+    (TokenClass (NotOneOf xs (AndAsIn y)))
+    (TokenClass (NotOneOf ws (AndNotAsIn zs)))
 deriving stock instance
   (Categorized token, Read token, Read alg, Read (Categorize token))
     => Read (RegExam token alg)
@@ -177,10 +340,8 @@ deriving stock instance
 deriving stock instance Functor (RegExam token)
 deriving stock instance Foldable (RegExam token)
 deriving stock instance Traversable (RegExam token)
-deriving stock instance (Categorized token, Eq alg)
-  => Eq (RegExam token alg)
-deriving stock instance (Categorized token, Ord alg)
-  => Ord (RegExam token alg)
+deriving stock instance (Categorized token, Eq alg) => Eq (RegExam token alg)
+deriving stock instance (Categorized token, Ord alg) => Ord (RegExam token alg)
 deriving stock instance Categorized token => Eq (CategoryTest token)
 deriving stock instance Categorized token => Ord (CategoryTest token)
 deriving stock instance
@@ -192,62 +353,55 @@ deriving stock instance
 instance (Categorized token, HasTrie token)
   => HasTrie (RegEx token) where
     data (RegEx token :->: b) = RegExTrie
-      { terminalTrie :: [token] :->: b
+      { seqEmptyTrie :: b
       , nonTerminalTrie :: String :->: b
       , sequenceTrie :: (RegEx token, RegEx token) :->: b
       , alternateTrie :: (RegEx token, RegEx token) :->: b
       , kleeneStarTrie :: RegEx token :->: b
       , kleeneOptTrie :: RegEx token :->: b
       , kleenePlusTrie :: RegEx token :->: b
-      , failTrie :: b
-      , passTrie :: b
       , oneOfTrie :: [token] :->: b
       , notOneOfTrie :: ([token], Either Int [Int]) :->: b
       }
     trie f = RegExTrie
-      { terminalTrie = trie (f . terminal)
+      { seqEmptyTrie = f mempty
       , nonTerminalTrie = trie (f . nonTerminal)
       , sequenceTrie = trie (f . uncurry (<>))
       , alternateTrie = trie (f . uncurry (>|<))
       , kleeneStarTrie = trie (f . starK)
       , kleeneOptTrie = trie (f . optK)
       , kleenePlusTrie = trie (f . plusK)
-      , failTrie = f zeroK
-      , passTrie = f anyToken
       , oneOfTrie = trie (f . oneOf)
       , notOneOfTrie = trie (f . testNotOneOf)
       }
     untrie rex = \case
-      Terminal word -> untrie (terminalTrie rex) word
+      SeqEmpty -> seqEmptyTrie rex
       NonTerminal name -> untrie (nonTerminalTrie rex) name
       Sequence x1 x2 -> untrie (sequenceTrie rex) (x1,x2)
       KleeneStar x -> untrie (kleeneStarTrie rex) x
       KleenePlus x -> untrie (kleenePlusTrie rex) x
       KleeneOpt x -> untrie (kleeneOptTrie rex) x
-      RegExam Fail -> failTrie rex
-      RegExam Pass -> passTrie rex
       RegExam (OneOf chars) -> untrie (oneOfTrie rex) (Set.toList chars)
-      RegExam (NotOneOf chars (AsIn cat)) ->
+      RegExam (NotOneOf chars (AndAsIn cat)) ->
         untrie (notOneOfTrie rex) (Set.toList chars, Left (fromEnum cat))
-      RegExam (NotOneOf chars (NotAsIn cats)) ->
+      RegExam (NotOneOf chars (AndNotAsIn cats)) ->
         untrie (notOneOfTrie rex)
           (Set.toList chars, Right (Set.toList (Set.map fromEnum cats)))
       RegExam (Alternate x1 x2) -> untrie (alternateTrie rex) (x1,x2)
     enumerate rex = mconcat
-      [ first' Terminal <$> enumerate (terminalTrie rex)
+      [ [(SeqEmpty, seqEmptyTrie rex)]
       , first' NonTerminal <$> enumerate (nonTerminalTrie rex)
       , first' (uncurry Sequence) <$> enumerate (sequenceTrie rex)
       , first' (RegExam . uncurry Alternate) <$> enumerate (alternateTrie rex)
       , first' KleeneStar <$> enumerate (kleeneStarTrie rex)
       , first' KleeneOpt <$> enumerate (kleeneOptTrie rex)
       , first' KleenePlus <$> enumerate (kleenePlusTrie rex)
-      , [(RegExam Fail, failTrie rex)]
-      , [(RegExam Pass, passTrie rex)]
       , first' (RegExam . OneOf . Set.fromList) <$> enumerate (oneOfTrie rex)
       , first' testNotOneOf <$> enumerate (notOneOfTrie rex)
       ]
 testNotOneOf
   :: Categorized token
   => ([token], Either Int [Int]) -> RegEx token
-testNotOneOf (chars, catTest) = RegExam $
-  NotOneOf (Set.fromList chars) (either (AsIn . toEnum) (NotAsIn . Set.map toEnum . Set.fromList) catTest)
+testNotOneOf (chars, catTest) = RegExam $ NotOneOf
+  (Set.fromList chars)
+  (either (AndAsIn . toEnum) (AndNotAsIn . Set.map toEnum . Set.fromList) catTest)
diff --git a/src/Control/Lens/Grammar/Symbol.hs b/src/Control/Lens/Grammar/Symbol.hs
index 4f69e98..d5ab6b3 100644
--- a/src/Control/Lens/Grammar/Symbol.hs
+++ b/src/Control/Lens/Grammar/Symbol.hs
@@ -26,7 +26,7 @@ class TerminalSymbol token s | s -> token where
   default terminal
     :: (p () () ~ s, Tokenized token (p token token), Monoidal p, Cochoice p)
     => [token] -> s
-  terminal = foldr (\a p -> only a ?< anyToken *> p) oneP
+  terminal = foldr (\a p -> only a ?< token a *> p) oneP
 
 -- | A `nonTerminal` symbol in a grammar.
 class NonTerminalSymbol s where
diff --git a/src/Control/Lens/Grammar/Token.hs b/src/Control/Lens/Grammar/Token.hs
index bb9d825..7aaf2bc 100644
--- a/src/Control/Lens/Grammar/Token.hs
+++ b/src/Control/Lens/Grammar/Token.hs
@@ -60,14 +60,22 @@ class Categorized token => Tokenized token p | p -> token where
     => token -> p
   token = satisfy . token
 
-  {- | A single token which is `oneOf` a set. -}
+  {- | A single token which is `oneOf` a set.
+
+  prop> token x = oneOf [x]
+  
+  -}
   oneOf :: Foldable f => f token -> p
   default oneOf
     :: (p ~ q token token, Choice q, Cochoice q, Foldable f)
     => f token -> p
   oneOf = satisfy . oneOf
 
-  {- | A single token which is `notOneOf` a set. -}
+  {- | A single token which is `notOneOf` a set.
+  
+  prop> anyToken = notOneOf []
+  
+  -}
   notOneOf :: Foldable f => f token -> p
   default notOneOf
     :: (p ~ q token token, Choice q, Cochoice q, Foldable f)
diff --git a/src/Control/Lens/Grate.hs b/src/Control/Lens/Grate.hs
index 9db64ae..520065b 100644
--- a/src/Control/Lens/Grate.hs
+++ b/src/Control/Lens/Grate.hs
@@ -48,8 +48,7 @@ type Grate s t a b = forall p f.
   (Closed p, Monoidal p, Distributive f, Applicative f)
     => p a (f b) -> p s (f t)
 
-{- | If you see `AGrate` in a signature for a function,
-the function is expecting a `Grate`. -}
+{- | `AGrate` is monomorphically a `Grate`. -}
 type AGrate s t a b =
   Grating a b a (Identity b) -> Grating a b s (Identity t)
 
diff --git a/src/Control/Lens/Internal/NestedPrismTH.hs b/src/Control/Lens/Internal/NestedPrismTH.hs
index 83e2520..76c7e08 100644
--- a/src/Control/Lens/Internal/NestedPrismTH.hs
+++ b/src/Control/Lens/Internal/NestedPrismTH.hs
@@ -33,21 +33,42 @@ import qualified Data.Set as Set
 import Data.Set (Set)
 import Prelude
 
--- | Generate a `Control.Lens.Prism.Prism`
+-- | Similar to `Control.Lens.Internal.PrismTH.makePrisms`,
+-- `makeNestedPrisms` generates a `Control.Lens.Prism.Prism`
 -- for each constructor of a data type.
--- `Control.Lens.Iso.Iso`s generated when possible.
--- `Control.Lens.Review.Review`s are created for constructors with existentially
--- quantified constructors and GADTs.
---
--- See `Control.Lens.Internal.PrismTH.makePrisms` for details and examples.
+-- `Control.Lens.Iso.Iso`s are generated when possible.
+-- `Control.Lens.Review.Review`s are generated for constructors
+-- with existentially quantified constructors and GADTs.
 -- The difference in `makeNestedPrisms`
 -- is that constructors with @n > 2@ arguments
 -- will use right-nested pairs, rather than a flat @n@-tuple.
--- This makes them suitable for use on the left-hand-side of
--- `Control.Lens.PartialIso.>~`,
--- `Control.Lens.PartialIso.>?` and `Control.Lens.PartialIso.>?<`;
--- with repeated use of `Data.Profunctor.Distributor.>*<`
--- on the right-hand-side, resulting in right-nested pairs.
+-- This makes them suitable for pattern bonding,
+-- by use of the applicator `Control.Lens.PartialIso.>?`
+-- to `Data.Profunctor.Monoidal.Monoidal` idiom notation
+-- with `Data.Profunctor.Monoidal.>*<`,
+-- or to `Data.Profunctor.Monadic.Monadic` qualified do-notation.
+--
+-- /e.g./
+--
+-- @
+-- data FooBar a
+--   = Foo a
+--   | Bar Int
+--   | Baz Int Char
+--   | Buzz Double String Bool
+--   | Boop
+-- makeNestedPrisms ''FooBar
+-- @
+--
+-- will create
+--
+-- @
+-- _Foo :: Prism (FooBarBaz a) (FooBarBaz b) a b
+-- _Bar :: Prism' (FooBarBaz a) Int
+-- _Baz :: Prism' (FooBarBaz a) (Int, Char)
+-- _Buzz :: Prism' (FooBarBaz a) (Double, (String, Bool))
+-- _Boop :: Prism' (FooBarBaz a) ()
+-- @
 makeNestedPrisms :: Name -> DecsQ
 makeNestedPrisms typeName =
   do info <- D.reifyDatatype typeName
diff --git a/src/Control/Lens/Monocle.hs b/src/Control/Lens/Monocle.hs
index c2d055e..da093f7 100644
--- a/src/Control/Lens/Monocle.hs
+++ b/src/Control/Lens/Monocle.hs
@@ -19,6 +19,7 @@ module Control.Lens.Monocle
   , monocle
   , withMonocle
   , cloneMonocle
+  , imprism
   , mapMonocle
   , ditraversed
   , forevered
@@ -42,8 +43,7 @@ type Monocle s t a b = forall p f.
   (Monoidal p, Applicative f)
     => p a (f b) -> p s (f t)
 
-{- | If you see `AMonocle` in a signature for a function,
-the function is expecting a `Monocle`. -}
+{- | `AMonocle` is monomorphically a `Monocle`. -}
 type AMonocle s t a b =
   Monocular a b a (Identity b) -> Monocular a b s (Identity t)
 
@@ -61,6 +61,16 @@ monomorphically typed `Monocle` for different purposes.
 cloneMonocle :: AMonocle s t a b -> Monocle s t a b
 cloneMonocle mon = unwrapPafb . mapMonocle mon . WrapPafb
 
+{- | Convert a `Monocle` to an improper `Control.Lens.Prism.Prism`.
+
+>>> review (imprism ditraversed) 1 :: Complex Int
+1 :+ 1
+>>> preview (imprism ditraversed) (1 :+ 2 :: Complex Int)
+Just 1
+-}
+imprism :: Monocle s t a b -> Prism s t a b
+imprism mon = clonePrism mon
+
 {- | Build a `Monocle` from a `Traversable` & `Distributive`,
 homogeneous, countable product.
 
diff --git a/src/Control/Lens/PartialIso.hs b/src/Control/Lens/PartialIso.hs
index 64c927a..cace084 100644
--- a/src/Control/Lens/PartialIso.hs
+++ b/src/Control/Lens/PartialIso.hs
@@ -117,8 +117,7 @@ some equivalence class of terms.
 -}
 type PartialIso' s a = PartialIso s s a a
 
-{- | If you see `APartialIso` in a signature for a function,
-the function is expecting a `PartialIso`. -}
+{- | `APartialIso` is monomorphically a `PartialIso`. -}
 type APartialIso s t a b =
   PartialExchange a b a (Maybe b) -> PartialExchange a b s (Maybe t)
 
@@ -222,7 +221,7 @@ infixl 4 >?
 (?<) pat = withPrism pat $ \f g -> unright . dimap (either id f) g
 infixl 4 ?<
 
-{- | Action of `APartialIso` on `Choice` and `Cochoice` `Profunctor`s. -}
+{- | Action of `APartialIso` on `Choice` & `Cochoice` partial profunctors. -}
 (>?<)
   :: (Choice p, Cochoice p)
   => APartialIso s t a b
@@ -265,18 +264,18 @@ notNulled = partialIso nonEmp nonEmp where
   nonEmp s = if isn't _Empty s then Just s else Nothing
 
 {- | The either-of-tuples representation of `Maybe`. -}
-eotMaybe :: Iso (Maybe a) (Maybe b) (Either () a) (Either () b)
+eotMaybe :: Iso (Maybe a) (Maybe b) (Either a ()) (Either b ())
 eotMaybe = iso
-  (maybe (Left ()) Right)
-  (either (pure Nothing) Just)
+  (maybe (Right ()) Left)
+  (either Just (const Nothing))
 
 {- | The either-of-tuples representation of list-like streams. -}
 eotList
   :: (Cons s s a a, AsEmpty t, Cons t t b b)
-  => Iso s t (Either () (a,s)) (Either () (b,t))
+  => Iso s t (Either (a,s) ()) (Either (b,t) ())
 eotList = iso
-  (maybe (Left ()) Right . uncons)
-  (either (const Empty) (review _Cons))
+  (maybe (Right ()) Left . uncons)
+  (either (review _Cons) (const Empty))
 
 {- | Iterate the application of a partial isomorphism,
 useful for constructing fold/unfold isomorphisms. -}
diff --git a/src/Control/Lens/Wither.hs b/src/Control/Lens/Wither.hs
index 72dd0be..7b5d7c5 100644
--- a/src/Control/Lens/Wither.hs
+++ b/src/Control/Lens/Wither.hs
@@ -37,7 +37,6 @@ import Witherable
 
 {- | `Wither`s extends `Control.Lens.Traversal.Traversal`s by filtering.
 
-
 Every one of the following is a `Wither`.
 
 * `Control.Lens.Iso.Iso`
@@ -48,8 +47,7 @@ Every one of the following is a `Wither`.
 -}
 type Wither s t a b = forall f. Alternative f => (a -> f b) -> s -> f t
 
-{- | If you see `AWither` in a signature for a function,
-the function is expecting a `Wither`. -}
+{- | `AWither` is monomorphically a `Wither`. -}
 type AWither s t a b = (a -> Altar a b b) -> s -> Altar a b t
 
 {- | `Witheroid`s generalize `Wither`s.
diff --git a/src/Control/Monad/Fail/Try.hs b/src/Control/Monad/Fail/Try.hs
new file mode 100644
index 0000000..7420bf4
--- /dev/null
+++ b/src/Control/Monad/Fail/Try.hs
@@ -0,0 +1,46 @@
+{-|
+Module      : Control.Monad.Fail.Try
+Description : try & fail
+Copyright   : (C) 2026 - Eitan Chatav
+License     : BSD-style (see the file LICENSE)
+Maintainer  : Eitan Chatav <eitan.chatav@gmail.com>
+Stability   : provisional
+Portability : non-portable
+-}
+
+module Control.Monad.Fail.Try
+  ( -- * MonadTry
+    MonadTry (..)
+    -- * MonadFail
+  , MonadFail (..)
+    -- * MonadPlus
+  , MonadPlus (..)
+    -- * Alternative
+  , Alternative (..)
+  ) where
+
+import Control.Applicative
+import Control.Monad
+
+{- | `MonadTry` is a failure handling interface,
+with `fail` & `try` and redundant alternation operators.
+
+prop> empty = mzero
+prop> (<|>) = mplus
+
+When a `MonadTry` is also a
+`Control.Lens.Grammar.BackusNaur.BackusNaurForm`,
+then the following invariant should hold.
+
+prop> fail label = rule label empty
+
+-}
+class (MonadFail m, MonadPlus m) => MonadTry m where
+
+  {- | A handler for failures.
+  Used for backtracking state on failure in
+  `Data.Profunctor.Grammar.Parsector.Parsector`.
+  -}
+  try :: m a -> m a
+  default try :: m a -> m a
+  try = id
diff --git a/src/Data/Profunctor/Distributor.hs b/src/Data/Profunctor/Distributor.hs
index 1d2fd37..eec5e2c 100644
--- a/src/Data/Profunctor/Distributor.hs
+++ b/src/Data/Profunctor/Distributor.hs
@@ -10,22 +10,11 @@ Portability : non-portable
 
 module Data.Profunctor.Distributor
   ( -- * Distributor
-    Distributor (..), dialt
+    Distributor (..)
+  , dialt
     -- * Alternator
   , Alternator (..)
   , choice
-  , option
-    -- * Homogeneous
-  , Homogeneous (..)
-    -- * SepBy
-  , SepBy (..)
-  , sepBy
-  , noSep
-  , several
-  , several1
-  , chain
-  , chain1
-  , intercalateP
   ) where
 
 import Control.Applicative hiding (WrappedArrow)
@@ -37,14 +26,9 @@ import Control.Lens.PartialIso
 import Data.Bifunctor.Clown
 import Data.Bifunctor.Joker
 import Data.Bifunctor.Product
-import Data.Complex
 import Data.Foldable hiding (toList)
 import Data.Functor.Adjunction
-import Data.Functor.Compose
 import Data.Functor.Contravariant.Divisible
-import qualified Data.Functor.Product as Functor
-import qualified Data.Functor.Sum as Functor
-import qualified Data.Monoid as Monoid
 import Data.Profunctor hiding (WrappedArrow)
 import Data.Profunctor qualified as Pro (WrappedArrow)
 import Data.Profunctor.Cayley
@@ -52,14 +36,7 @@ import Data.Profunctor.Composition
 import Data.Profunctor.Monad
 import Data.Profunctor.Monoidal
 import Data.Profunctor.Yoneda
-import Data.Proxy
-import Data.Sequence (Seq)
-import Data.Tagged
-import Data.Tree (Tree (..))
-import Data.Vector (Vector)
 import Data.Void
-import GHC.Exts
-import GHC.Generics
 
 -- Distributor --
 
@@ -93,7 +70,7 @@ class Monoidal p => Distributor p where
 
   {- | The zero structure morphism of a `Distributor`.
 
-  `zeroP` has a default for `Alternator`.
+  `zeroP` has a default for `Alternator`s.
 
   prop> zeroP = empty
   -}
@@ -103,7 +80,7 @@ class Monoidal p => Distributor p where
 
   {- | The sum structure morphism of a `Distributor`.
 
-  `>+<` has a default for `Alternator`.
+  `>+<` has a default for `Alternator`s.
 
   prop> x >+< y = alternate (Left x) <|> alternate (Right y)
   -}
@@ -116,11 +93,11 @@ class Monoidal p => Distributor p where
 
   {- | One or none. -}
   optionalP :: p a b -> p (Maybe a) (Maybe b)
-  optionalP p = eotMaybe >~ oneP >+< p
+  optionalP p = eotMaybe >~ p >+< oneP
 
   {- | Zero or more. -}
   manyP :: p a b -> p [a] [b]
-  manyP p = eotList >~ oneP >+< p >*< manyP p
+  manyP p = eotList >~ p >*< manyP p >+< oneP
 
 instance Distributor (->) where
   zeroP = id
@@ -203,119 +180,17 @@ dialt
   -> p a b -> p c d -> p s t
 dialt f g h p q = dimap f (either g h) (p >+< q)
 
-{- | A class of `Homogeneous`
-countable sums of countable products.
--}
-class Traversable t => Homogeneous t where
-  {- | Sequences actions `homogeneously`.
-
-  prop> homogeneously @Maybe = optionalP
-  prop> homogeneously @[] = manyP
-
-  Any `Traversable` & `Data.Distributive.Distributive` countable product
-  can be given a default implementation for the `homogeneously` method.
-
-  prop> homogeneously = ditraverse
-
-  And any user-defined homogeneous algebraic datatype has
-  a default instance for `Homogeneous`, by deriving `Generic1`.
-  -}
-  homogeneously :: Distributor p => p a b -> p (t a) (t b)
-  default homogeneously
-    :: (Generic1 t, Homogeneous (Rep1 t), Distributor p)
-    => p a b -> p (t a) (t b)
-  homogeneously = dimap from1 to1 . homogeneously
-instance Homogeneous Par1 where
-  homogeneously = dimap unPar1 Par1
-instance Homogeneous Identity where
-  homogeneously = dimap runIdentity Identity
-instance Homogeneous Monoid.Dual where
-  homogeneously = dimap Monoid.getDual Monoid.Dual
-instance Homogeneous Monoid.Product where
-  homogeneously = dimap Monoid.getProduct Monoid.Product
-instance Homogeneous Monoid.Sum where
-  homogeneously = dimap Monoid.getSum Monoid.Sum
-instance Homogeneous (Tagged s) where
-  homogeneously = dimap unTagged Tagged
-instance Homogeneous U1 where
-  homogeneously _ = pure U1
-instance Homogeneous (K1 i ()) where
-  homogeneously _ = pure (K1 ())
-instance Homogeneous (Const ()) where
-  homogeneously _ = pure (Const ())
-instance Homogeneous Proxy where
-  homogeneously _ = pure Proxy
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (s :.: t) where
-    homogeneously
-      = dimap unComp1 Comp1
-      . homogeneously . homogeneously
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (Compose s t) where
-    homogeneously
-      = dimap getCompose Compose
-      . homogeneously . homogeneously
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (s :*: t) where
-    homogeneously p = dimap2
-      (\(s :*: _) -> s)
-      (\(_ :*: t) -> t)
-      (:*:)
-      (homogeneously p)
-      (homogeneously p)
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (Functor.Product s t) where
-    homogeneously p = dimap2
-      (\(Functor.Pair s _) -> s)
-      (\(Functor.Pair _ t) -> t)
-      Functor.Pair
-      (homogeneously p)
-      (homogeneously p)
-instance Homogeneous V1 where
-  homogeneously _ = dimap (\case) (\case) zeroP
-instance Homogeneous (K1 i Void) where
-  homogeneously _ = dimap unK1 K1 zeroP
-instance Homogeneous (Const Void) where
-  homogeneously _ = dimap getConst Const zeroP
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (s :+: t) where
-    homogeneously p = dialt
-      (\case {L1 s -> Left s; R1 t -> Right t})
-      L1
-      R1
-      (homogeneously p)
-      (homogeneously p)
-instance (Homogeneous s, Homogeneous t)
-  => Homogeneous (Functor.Sum s t) where
-    homogeneously p = dialt
-      (\case {Functor.InL s -> Left s; Functor.InR t -> Right t})
-      Functor.InL
-      Functor.InR
-      (homogeneously p)
-      (homogeneously p)
-instance Homogeneous t
-  => Homogeneous (M1 i c t) where
-    homogeneously = dimap unM1 M1 . homogeneously
-instance Homogeneous f => Homogeneous (Rec1 f) where
-  homogeneously = dimap unRec1 Rec1 . homogeneously
-instance Homogeneous Maybe where
-  homogeneously = optionalP
-instance Homogeneous [] where
-  homogeneously = manyP
-instance Homogeneous Vector where
-  homogeneously p = eotList >~ oneP >+< p >*< homogeneously p
-instance Homogeneous Seq where
-  homogeneously p = eotList >~ oneP >+< p >*< homogeneously p
-instance Homogeneous Complex where
-  homogeneously p = dimap2 realPart imagPart (:+) p p
-instance Homogeneous Tree where
-  homogeneously p = dimap2 rootLabel subForest Node p (manyP (homogeneously p))
-
 -- Alternator --
 
 {- | The `Alternator` class co-extends `Choice` and `Distributor`,
 as well as `Alternative`, adding the `alternate` method,
-which is a lax monoidal structure morphism on sums.
+which is a lax monoidal structure morphism on sums, with these
+these laws relating them.
+
+prop> left' = alternate . Left
+prop> right' = alternate . Right
+prop> zeroP = empty
+prop> x >+< y = alternate (Left x) <|> alternate (Right y)
 
 For the case of `Functor`s the analog of `alternate` can be defined
 without any other constraint, but the case of `Profunctor`s turns
@@ -324,13 +199,8 @@ out to be slighly more complex.
 class (Choice p, Distributor p, forall x. Alternative (p x))
   => Alternator p where
 
-    {- |
-    prop> left' = alternate . Left
-    prop> right' = alternate . Right
-    prop> zeroP = empty
-    prop> x >+< y = alternate (Left x) <|> alternate (Right y)
-
-    `alternate` has a default for `Cochoice`.
+    {- | The structure morphism for an `Alternator`,
+    `alternate` has a default for `Choice` & `Cochoice` partial distributors.
     -}
     alternate
       :: Either (p a b) (p c d)
@@ -346,16 +216,20 @@ class (Choice p, Distributor p, forall x. Alternative (p x))
 
     {- | One or more. -}
     someP :: p a b -> p [a] [b]
-    someP p = _Cons >? p >*< manyP p
+    someP x = x >:< manyP x
+
+    {- | One or zero with default.
+    
+    prop> optionP _Nothing (_Just >? p) = optionalP p
+
+    -}
+    optionP :: APrism a b () () -> p a b -> p a b
+    optionP def p = p <|> pureP def
 
 -- | Combines all `Alternative` choices in the specified list.
 choice :: (Foldable f, Alternative p) => f (p a) -> p a
 choice = foldl' (<|>) empty
 
--- | Perform an `Alternative` action or return a default value.
-option :: Alternative p => a {- ^ default value -} -> p a -> p a
-option a p = p <|> pure a
-
 instance (Alternator p, Applicative f)
   => Alternator (WrappedPafb f p) where
     alternate =
@@ -382,78 +256,3 @@ instance Alternator p => Alternator (Yoneda p) where
   alternate (Left p) = proreturn (alternate (Left (proextract p)))
   alternate (Right p) = proreturn (alternate (Right (proextract p)))
   someP = proreturn . someP . proextract
-
-{- | Used to sequence multiple times,
-separated by a `separateBy`,
-begun by a `beginBy`,
-and ended by an `endBy`. -}
-data SepBy p = SepBy
-  { beginBy :: p
-  , endBy :: p
-  , separateBy :: p
-  } deriving stock
-    ( Functor, Foldable, Traversable
-    , Eq, Ord, Show, Read
-    )
-
-{- | A `SepBy` smart constructor,
-setting the `separateBy` field,
-with no beginning or ending delimitors,
-except by updating `beginBy` or `endBy` fields. -}
-sepBy :: Monoidal p => p () () -> SepBy (p () ())
-sepBy = SepBy oneP oneP
-
-{- | A `SepBy` smart constructor for no separator,
-beginning or ending delimiters. -}
-noSep :: Monoidal p => SepBy (p () ())
-noSep = sepBy oneP
-
-{- |
-prop> several noSep = manyP
--}
-several
-  :: (IsList s, IsList t, Distributor p)
-  => SepBy (p () ()) -> p (Item s) (Item t) -> p s t
-several (SepBy beg end sep) p = iso toList fromList . eotList >~
-  beg >* (oneP >+< p >*< manyP (sep >* p)) *< end
-
-{- |
-prop> several1 noSep p = someP p
--}
-several1
-  :: (IsList s, IsList t, Distributor p, Choice p)
-  => SepBy (p () ()) -> p (Item s) (Item t) -> p s t
-several1 (SepBy beg end sep) p = iso toList fromList . _Cons >?
-  beg >* (p >*< manyP (sep >* p)) *< end
-
-{- | Use a nilary constructor pattern to sequence zero times, or
-associate a binary constructor pattern to sequence one or more times. -}
-chain
-  :: Alternator p
-  => (forall x. x -> Either x x) -- ^ `Left` or `Right` associate
-  -> APartialIso a b (a,a) (b,b) -- ^ binary constructor pattern
-  -> APrism a b () () -- ^ nilary constructor pattern
-  -> SepBy (p () ()) -> p a b -> p a b
-chain association pat2 pat0 (SepBy beg end sep) p =
-  beg >* (pat0 >? oneP <|> chain1 association pat2 (sepBy sep) p) *< end
-
-{- | Associate a binary constructor pattern to sequence one or more times. -}
-chain1
-  :: (Distributor p, Choice p)
-  => (forall x. x -> Either x x) -- ^ `Left` or `Right` associate
-  -> APartialIso a b (a,a) (b,b) -- ^ binary constructor pattern
-  -> SepBy (p () ()) -> p a b -> p a b
-chain1 association pat (SepBy beg end sep) = leftOrRight chainl1 chainr1
-  where
-    leftOrRight a b = case association () of Left _ -> a; Right _ -> b
-    chainl1 p = difoldl pat >? beg >* p >*< manyP (sep >* p) *< end
-    chainr1 p = difoldr pat >? beg >* manyP (p *< sep) >*< p *< end
-
-{- | `intercalateP` adds a `SepBy` to `replicateP`. -}
-intercalateP
-  :: (Monoidal p, Choice p, AsEmpty s, AsEmpty t, Cons s t a b)
-  => Int -> SepBy (p () ()) -> p a b -> p s t
-intercalateP n (SepBy beg end _) _ | n <= 0 =
-  beg >* lmap (const Empty) asEmpty *< end
-intercalateP n (SepBy beg end comma) p =
-  beg >* p >:< replicateP (n-1) (comma >* p) *< end
diff --git a/src/Data/Profunctor/Filtrator.hs b/src/Data/Profunctor/Filtrator.hs
index 75a1e42..5ea8ef7 100644
--- a/src/Data/Profunctor/Filtrator.hs
+++ b/src/Data/Profunctor/Filtrator.hs
@@ -28,7 +28,8 @@ import Witherable
 
 {- | The `Filtrator` class extends `Cochoice`,
 as well as `Filterable`, adding the `filtrate` method,
-which is an oplax monoidal structure morphism dual to `>+<`.
+which is an oplax monoidal structure morphism dual to
+`>+<`.
 
 prop> filtrate . uncurry (>+<) = id
 prop> uncurry (>+<) . filtrate = id
@@ -41,8 +42,12 @@ class (Cochoice p, forall x. Filterable (p x))
     prop> unright = snd . filtrate
 
     `filtrate` is a distant relative to `Data.Either.partitionEithers`.
+    `filtrate` can be given a default value for `Monadic`
+    `Alternator`s via `mfiltrate`.
 
-    `filtrate` has a default for `Choice`.
+    prop> filtrate = mfiltrate
+
+    `filtrate` has a default for `Choice` & `Cochoice` partial profunctors.
     -}
     filtrate
       :: p (Either a c) (Either b d)
@@ -56,12 +61,13 @@ class (Cochoice p, forall x. Filterable (p x))
       &&&
       dimapMaybe (Just . Right) (either (const Nothing) Just)
 
--- | `mfiltrate` can be used as `filtrate`, for `Monadic` `Alternator`s.
+-- | A `Monadic` `Alternator` has
+-- an equivalent to `filtrate`, given by `mfiltrate`.
 --
--- prop> mfiltrate = filtrate
+-- prop> filtrate = mfiltrate
 mfiltrate
   :: (Monadic p, Alternator p)
-  => p (Either a c) (Either b d)
+  => p (Either a c) (Either b d) -- ^ partition `Either`
   -> (p a b, p c d)
 mfiltrate =
   (lmap Left >=> either pure (const empty))
diff --git a/src/Data/Profunctor/Grammar.hs b/src/Data/Profunctor/Grammar.hs
index aca3466..30279a2 100644
--- a/src/Data/Profunctor/Grammar.hs
+++ b/src/Data/Profunctor/Grammar.hs
@@ -9,13 +9,13 @@ Portability : non-portable
 -}
 
 module Data.Profunctor.Grammar
-  ( -- * Parsor
-    Parsor (..)
+  ( -- * Printor
+    Printor (..)
+  , printP
+    -- * Parsor
+  , Parsor (..)
   , unparseP
   , parseP
-    -- * Printor
-  , Printor (..)
-  , printP
     -- * Grammor
   , Grammor (..)
   ) where
@@ -26,11 +26,11 @@ import Control.Category
 import Control.Lens
 import Control.Lens.Extras
 import Control.Lens.Grammar.BackusNaur
-import Control.Lens.Grammar.Boole
 import Control.Lens.Grammar.Kleene
 import Control.Lens.Grammar.Symbol
 import Control.Lens.Grammar.Token
 import Control.Monad
+import Control.Monad.Fail.Try
 import Data.Coerce
 import Data.Monoid
 import Data.Profunctor
@@ -42,6 +42,15 @@ import Prelude hiding (id, (.))
 import GHC.Exts
 import Witherable
 
+-- | `Printor` is a simple printer `Profunctor`.
+newtype Printor s f a b = Printor {runPrintor :: a -> f (b, s -> s)}
+
+-- | Run the printer on a value, returning a function
+-- that `cons`es tokens at the beginning of an input string,
+-- from right to left.
+printP :: Functor f => Printor s f a b -> a -> f (s -> s)
+printP (Printor f) = fmap snd . f
+
 -- | `Parsor` is a simple invertible parser `Profunctor`.
 newtype Parsor s f a b = Parsor {runParsor :: Maybe a -> s -> f (b,s)}
 
@@ -57,15 +66,6 @@ parseP (Parsor f) = f Nothing
 unparseP :: Functor f => Parsor s f a b -> a -> s -> f s
 unparseP (Parsor f) a = fmap snd . f (Just a)
 
--- | `Printor` is a simple printer `Profunctor`.
-newtype Printor s f a b = Printor {runPrintor :: a -> f (b, s -> s)}
-
--- | Run the printer on a value, returning a function
--- that `cons`es tokens at the beginning of an input string,
--- from right to left.
-printP :: Functor f => Printor s f a b -> a -> f (s -> s)
-printP (Printor f) = fmap snd . f
-
 -- | `Grammor` is a constant `Profunctor`.
 newtype Grammor k a b = Grammor {runGrammor :: k}
 
@@ -120,6 +120,9 @@ instance (Alternative m, Monad m) => Alternator (Parsor s m) where
       Nothing -> fmap (first' Right) (p Nothing s)
       Just (Right a) -> fmap (first' Right) (p (Just a) s)
       Just (Left _) -> empty
+  optionP def p = Parsor $ \ma s -> case ma of
+    Nothing -> runParsor (p <|> pureP def) ma s
+    Just _ -> runParsor (pureP def <|> p) ma s
 instance (Alternative m, Monad m) => Category (Parsor s m) where
   id = Parsor $ \ma s -> case ma of
     Nothing -> empty
@@ -177,6 +180,7 @@ instance
 instance BackusNaurForm (Parsor s m a b)
 instance (Alternative m, Monad m) => MonadFail (Parsor s m a) where
   fail _ = empty
+instance (Alternative m, Monad m) => MonadTry (Parsor s m a)
 instance AsEmpty s => Matching s (Parsor s [] a b) where
   word =~ p = case
     [ () | (_, remaining) <- runParsor p Nothing word
@@ -215,6 +219,7 @@ instance Alternative f => Alternator (Printor s f) where
       either (fmap (first' Left) . p) (\_ -> empty)
     Right (Printor p) -> Printor $
       either (\_ -> empty) (fmap (first' Right) . p)
+  optionP def p = pureP def <|> p
 instance Filterable f => Filtrator (Printor s f) where
   filtrate (Printor p) =
     let
@@ -284,6 +289,7 @@ instance
 instance BackusNaurForm (Printor s m a b)
 instance (Alternative m, Monad m) => MonadFail (Printor s m a) where
   fail _ = empty
+instance (Alternative m, Monad m) => MonadTry (Printor s m a)
 
 -- Grammor instances
 instance Functor (Grammor k a) where fmap _ = coerce
@@ -309,6 +315,7 @@ instance KleeneStarAlgebra k => Distributor (Grammor k) where
 instance KleeneStarAlgebra k => Alternator (Grammor k) where
   alternate = either coerce coerce
   someP (Grammor rex) = Grammor (plusK rex)
+  optionP _ (Grammor rex) = Grammor (optK rex)
 instance Tokenized token k => Tokenized token (Grammor k a b) where
   anyToken = Grammor anyToken
   token = Grammor . token
diff --git a/src/Data/Profunctor/Grammar/Parsector.hs b/src/Data/Profunctor/Grammar/Parsector.hs
new file mode 100644
index 0000000..63568d3
--- /dev/null
+++ b/src/Data/Profunctor/Grammar/Parsector.hs
@@ -0,0 +1,379 @@
+{-|
+Module      : Data.Profunctor.Grammar.Parsector
+Description : grammar distributor with errors
+Copyright   : (C) 2026 - Eitan Chatav
+License     : BSD-style (see the file LICENSE)
+Maintainer  : Eitan Chatav <eitan.chatav@gmail.com>
+Stability   : provisional
+Portability : non-portable
+
+See Leijen,
+[Parsec: Direct Style Monadic Parser Combinators For The Real World]
+(https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper-letter.pdf)
+-}
+
+module Data.Profunctor.Grammar.Parsector
+  ( -- * Parsector
+    Parsector (..)
+  , parsecP
+  , unparsecP
+  , ParsecState (..)
+  , ParsecError (..)
+  ) where
+
+import Control.Applicative
+import Control.Arrow
+import Control.Category
+import Data.Function (fix)
+import Control.Lens
+import Control.Lens.Grammar.BackusNaur
+import Control.Lens.Grammar.Boole
+import Control.Lens.Grammar.Kleene
+import Control.Lens.Grammar.Symbol
+import Control.Lens.Grammar.Token
+import Control.Lens.PartialIso
+import Control.Monad
+import Control.Monad.Fail.Try
+import Data.Profunctor
+import Data.Profunctor.Distributor
+import Data.Profunctor.Filtrator
+import Data.Profunctor.Monoidal
+import Data.Tree
+import GHC.Exts
+import Prelude hiding (id, (.))
+import Witherable
+
+{- | `Parsector` is an invertible @LL(1)@ parser which is intended
+to provide detailed error information, based on [Parsec]
+(https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper-letter.pdf).
+-}
+newtype Parsector s a b = Parsector
+  {runParsector :: forall x. (ParsecState s b -> x) -> ParsecState s a -> x}
+
+{- | Run `Parsector` as a parser: consume tokens from @s@,
+left to right, returning a `ParsecState` whose `parsecResult`
+is either a successful output syntax value or a `ParsecError`. -}
+parsecP
+  :: Categorized (Item s)
+  => Parsector s a b
+  -> s -- ^ input stream
+  -> ParsecState s b
+parsecP p s = runParsector p id (ParsecState False 0 s mempty (Left mempty))
+
+{- | Run `Parsector` as a printer: given a syntax value @a@ and
+an input stream, append tokens to @s@ left to right,
+returning a `ParsecState` whose `parsecResult` is
+either a `ParsecError` or a successful output syntax value,
+in which case, `parsecStream` is the output stream. -}
+unparsecP
+  :: Categorized (Item s)
+  => Parsector s a b
+  -> a -- ^ input syntax
+  -> s -- ^ input stream
+  -> ParsecState s b
+unparsecP p a s = runParsector p id (ParsecState False 0 s mempty (Right a))
+
+{- | `ParsecState` is both the input and output type of the
+underlying function inside `Parsector`.
+@Parsector s a b@ is equivalent to
+
+@ParsecState s a -> ParsecState s b@
+
+So `ParsecState` has a dual interpretation as input and output. -}
+data ParsecState s a = ParsecState
+  { parsecLooked :: !Bool
+    {- ^ @True@ once the parser has consumed at least one token
+    since the last `<|>` / `try` decision point.
+    Controls LL(1) commitment: a failure with `parsecLooked` @True@
+    is propagated immediately without trying alternatives.
+    Reset to @False@ by `try` on failure.
+    -}
+  , parsecOffset :: !Word
+    -- ^ Number of tokens consumed from the start of the stream.
+  , parsecStream :: s -- ^ stream
+  , parsecHint   :: ParsecError s
+    {- ^ Hint: the merged `ParsecError`s from all empty-failing
+    alternatives at the current position.
+    Carried forward on the *success* path by `<|>` and `>>=` so that
+    downstream failures include the full set of expected tokens. -}
+  , parsecResult :: Either (ParsecError s) a
+    {- ^ As an input: Either parse mode or print mode with syntax value.
+    As an output: Either a failure or success with syntax value.
+    -}
+  }
+
+{- | `ParsecError` is the error payload produced by `Parsector`,
+inside a failed `parsecResult` of a `ParsecState` output.
+-}
+data ParsecError s = ParsecError
+  { parsecExpect :: TokenClass (Item s)
+    {- ^ Class of expected token `Item`s at the `parsecOffset`.
+    `tokenClass`es and `Tokenized` combinators specify expectations.
+    `<|>` merges them via disjunction `>||<`.
+    Contrast with the actual `parsecStream`,
+    which is either empty or begins with an unexpected token.
+    -}
+  , parsecLabels :: [Tree String]
+    {- ^ Forest of `rule` labels active at the `parsecOffset`.
+    Each `rule` wraps its inner labels in a new `Node`.
+    `ruleRec` & `fail` also create label nodes.
+    When two empty failures are merged by `<|>`,
+    their forests are concatenated as siblings.
+    Use `drawForest` to display.
+    -}
+  }
+
+-- ParsecError instances
+deriving stock instance
+  ( Categorized (Item s)
+  , Show (Item s), Show (Categorize (Item s))
+  ) => Show (ParsecError s)
+deriving stock instance
+  ( Categorized (Item s)
+  , Read (Item s), Read (Categorize (Item s))
+  ) => Read (ParsecError s)
+deriving stock instance Categorized (Item s) => Eq (ParsecError s)
+deriving stock instance Categorized (Item s) => Ord (ParsecError s)
+instance Categorized (Item s) => Semigroup (ParsecError s) where
+  ParsecError e1 l1 <> ParsecError e2 l2 = ParsecError (e1 >||< e2) (l1 ++ l2)
+instance Categorized (Item s) => Monoid (ParsecError s) where
+  mempty = ParsecError falseB []
+
+-- ParsecState instances
+deriving stock instance Functor (ParsecState s)
+deriving stock instance Foldable (ParsecState s)
+deriving stock instance Traversable (ParsecState s)
+deriving stock instance
+  ( Categorized (Item s)
+  , Show (Item s), Show (Categorize (Item s))
+  , Show a, Show s
+  ) => Show (ParsecState s a)
+deriving stock instance
+  ( Categorized (Item s)
+  , Read (Item s), Read (Categorize (Item s))
+  , Read a, Read s
+  ) => Read (ParsecState s a)
+deriving stock instance
+  ( Categorized (Item s)
+  , Eq a, Eq s
+  ) => Eq (ParsecState s a)
+deriving stock instance
+  ( Categorized (Item s)
+  , Ord a, Ord s
+  ) => Ord (ParsecState s a)
+
+-- Parsector instances
+instance
+  ( Categorized token, Item s ~ token
+  , Cons s s token token, Snoc s s token token
+  ) => Tokenized token (Parsector s token token) where
+  anyToken = tokenClass anyToken
+  token t = tokenClass (token t)
+  oneOf ts = tokenClass (oneOf ts)
+  notOneOf ts = tokenClass (notOneOf ts)
+  asIn cat = tokenClass (asIn cat)
+  notAsIn cat = tokenClass (notAsIn cat)
+instance
+  ( Categorized token, Item s ~ token
+  , Cons s s token token, Snoc s s token token
+  ) => TokenAlgebra token (Parsector s token token) where
+    tokenClass test = Parsector $ \callback query ->
+      let
+        stream = parsecStream query
+        mode = parsecResult query
+        offset = parsecOffset query
+        replyOk tok str = query
+          { parsecLooked = True
+          , parsecHint   = mempty
+          , parsecStream = str
+          , parsecOffset = offset + 1
+          , parsecResult = Right tok
+          }
+        replyErr = query
+          { parsecHint   = mempty
+          , parsecResult = Left (ParsecError test []) }
+      in
+        callback $ case mode of
+          -- print mode
+          Right tok
+            | tokenClass test tok -> replyOk tok (snoc stream tok)
+            | otherwise -> replyErr
+          -- parse mode
+          Left _ -> case uncons stream of
+            Just (tok, rest)
+              | tokenClass test tok -> replyOk tok rest
+              | otherwise -> replyErr
+            Nothing -> replyErr
+instance BackusNaurForm (Parsector s a b) where
+  -- | Wraps inner `parsecLabels` in a new `Node name` on failure.
+  -- Has no effect on success.
+  rule name p = Parsector $ \callback query ->
+    flip (runParsector p) query $ \reply -> callback $
+      case parsecResult reply of
+        Left (ParsecError expect labels) -> reply
+          {parsecResult = Left (ParsecError expect [Node name labels])}
+        Right _ -> reply
+  ruleRec name = rule name . fix
+instance
+  ( Categorized token, Item s ~ token
+  , Cons s s token token, Snoc s s token token
+  ) => TerminalSymbol token (Parsector s () ())
+instance Functor (Parsector s a) where
+  fmap = rmap
+instance Categorized (Item s) => Applicative (Parsector s a) where
+  pure b = Parsector $ \callback query ->
+    callback query { parsecResult = Right b }
+  (<*>) = ap
+
+instance Categorized (Item s) => Monad (Parsector s a) where
+  return = pure
+  p >>= f = Parsector $ \callback query ->
+    flip (runParsector p) query $ \reply ->
+      case parsecResult reply of
+        Left err -> callback reply {parsecResult = Left err}
+        Right b ->
+          let
+            hintP  = parsecHint reply
+            fQuery = reply
+              { parsecLooked = False
+              , parsecHint   = mempty
+              , parsecResult = parsecResult query
+              }
+          in
+            flip (runParsector (f b)) fQuery $ \fReply -> callback $
+              if parsecLooked fReply
+                then fReply
+                else case parsecResult fReply of
+                  Left err -> fReply
+                    { parsecLooked = parsecLooked reply
+                    , parsecResult = Left (hintP <> err)
+                    }
+                  Right _ -> fReply
+                    { parsecLooked = parsecLooked reply
+                    , parsecHint   = hintP <> parsecHint fReply
+                    }
+instance Categorized (Item s) => Alternative (Parsector s a) where
+  -- | Always fails without consuming input; expects nothing.
+  empty = Parsector $ \callback query ->
+    callback query { parsecResult = Left mempty }
+  p <|> q = Parsector $ \callback query ->
+    flip (runParsector p) query $ \replyP -> callback $
+      case parsecResult replyP of
+        -- if p succeeds, take p's branch
+        Right _ -> replyP
+        -- if p failed after consuming (committed), propagate immediately
+        Left _ | parsecLooked replyP -> replyP
+        -- if p failed without consuming, try q
+        Left errP -> flip (runParsector q) query $ \replyQ ->
+          case (parsecLooked replyQ, parsecResult replyQ) of
+            -- q consumed (ok or err): propagate as-is, drop errP
+            (True, _)         -> replyQ
+            -- q empty ok: carry errP forward as hint for downstream
+            (False, Right _)  -> replyQ { parsecHint = errP <> parsecHint replyQ }
+            -- both empty fail: merge errors
+            (False, Left errQ) -> replyP { parsecResult = Left (errP <> errQ) }
+instance Categorized (Item s) => MonadPlus (Parsector s a)
+instance Categorized (Item s) => MonadFail (Parsector s a) where
+  fail msg = rule msg empty
+instance Categorized (Item s) => MonadTry (Parsector s a) where
+  -- | On failure, resets `parsecLooked` to @False@, allowing
+  -- the enclosing `<|>` to try the next alternative even if @p@
+  -- consumed input. Has no effect on success.
+  try p = Parsector $ \callback query ->
+    flip (runParsector p) query $ \reply -> callback $
+      case parsecResult reply of
+        Left _ -> reply { parsecLooked = False }
+        Right _ -> reply
+instance Categorized (Item s) => Filterable (Parsector s a) where
+  mapMaybe = dimapMaybe Just
+instance Category (Parsector s) where
+  id = Parsector id
+  Parsector q . Parsector p = Parsector (p . q)
+instance Categorized (Item s) => Arrow (Parsector s) where
+  arr f = Parsector $ \callback reply -> callback (f <$> reply)
+  (***) = (>*<)
+  first = first'
+  second = second'
+instance Categorized (Item s) => ArrowZero (Parsector s) where
+  zeroArrow = empty
+instance Categorized (Item s) => ArrowPlus (Parsector s) where
+  (<+>) = (<|>)
+instance Categorized (Item s) => ArrowChoice (Parsector s) where
+  (+++) = (>+<)
+  left = left'
+  right = right'
+instance Profunctor (Parsector s) where
+  dimap f g (Parsector p) = Parsector $
+    dimap (lmap (fmap g)) (lmap (fmap f)) p
+instance Strong (Parsector s) where
+  first' p = Parsector $ \callback reply0 ->
+    flip (runParsector p) (fst <$> reply0) $ \reply1 ->
+      callback reply1
+        { parsecResult = (,)
+            <$> parsecResult reply1
+            <*> (snd <$> parsecResult reply0)
+        }
+  second' p = Parsector $ \callback reply0 ->
+    flip (runParsector p) (snd <$> reply0) $ \reply1 ->
+      callback reply1
+        { parsecResult = (,)
+            <$> (fst <$> parsecResult reply0)
+            <*> parsecResult reply1
+        }
+instance Categorized (Item s) => Choice (Parsector s) where
+  left' = alternate . Left
+  right' = alternate . Right
+instance Categorized (Item s) => Distributor (Parsector s)
+instance Categorized (Item s) => Alternator (Parsector s) where
+  alternate (Left p) = Parsector $ \callback query -> callback $
+    let
+      replyOk = query
+        { parsecResult = case parsecResult query of
+            Left err       -> Left err
+            Right (Left a) -> Right a
+            Right (Right _) -> Left mempty
+        }
+      replyErr = query { parsecResult = Left mempty }
+    in
+      case (parsecResult query, parsecResult replyOk) of
+        (Right _, Left _) -> replyErr
+        _________________ ->
+          flip (runParsector p) replyOk $ \reply -> reply
+            { parsecResult = fmap Left (parsecResult reply) }
+  alternate (Right p) = Parsector $ \callback query -> callback $
+    let
+      replyOk = query
+        { parsecResult = case parsecResult query of
+            Left err        -> Left err
+            Right (Left _)  -> Left mempty
+            Right (Right b) -> Right b
+        }
+      replyErr = query { parsecResult = Left mempty }
+    in
+      case (parsecResult query, parsecResult replyOk) of
+        (Right _, Left _) -> replyErr
+        _________________ ->
+          flip (runParsector p) replyOk $ \reply -> reply
+            { parsecResult = fmap Right (parsecResult reply) }
+  optionP def p = Parsector $ \callback query ->
+    case parsecResult query of
+      Left _ -> runParsector (p <|> pureP def) callback query
+      Right _ -> runParsector (pureP def <|> p) callback query
+instance Categorized (Item s) => Cochoice (Parsector s) where
+  unleft = fst . filtrate
+  unright = snd . filtrate
+instance Categorized (Item s) => Filtrator (Parsector s) where
+  filtrate p =
+    ( Parsector $ \callback query ->
+        flip (runParsector p) (Left <$> query) $ \reply ->
+          callback reply
+            { parsecResult =
+                parsecResult reply >>= either Right (const (Left mempty))
+            }
+    , Parsector $ \callback query ->
+        flip (runParsector p) (Right <$> query) $ \reply ->
+          callback reply
+            { parsecResult =
+                parsecResult reply >>= either (const (Left mempty)) Right
+            }
+    )
diff --git a/src/Data/Profunctor/Monadic.hs b/src/Data/Profunctor/Monadic.hs
index 54d4a37..d2e4cee 100644
--- a/src/Data/Profunctor/Monadic.hs
+++ b/src/Data/Profunctor/Monadic.hs
@@ -16,7 +16,8 @@ This module can provide qualified do-notation for `Monadic` profunctors.
 >>> import qualified Data.Profunctor.Monadic as P
 
 See "Control.Lens.Grammar#t:CtxGrammar" for
-an example of how to use "bonding" notation.
+an example of how to use qualified do-notation
+with pattern bonding.
 -}
 
 module Data.Profunctor.Monadic
@@ -25,17 +26,23 @@ module Data.Profunctor.Monadic
   , (>>=)
   , (>>)
   , return
+    -- * MonadicTry
+  , MonadicTry
+  , try
   , fail
   ) where
 
-import Data.Profunctor
-import Prelude hiding ((>>=), (>>))
+import Control.Lens
+import Control.Monad hiding ((>>=), (>>), return)
+import Control.Monad.Fail.Try
+import Data.Profunctor.Monoidal
+import Prelude hiding ((>>=), (>>), return)
 
 {- | A `Profunctor` which is also a `Monad`. -}
 type Monadic p = (Profunctor p, forall x. Monad (p x))
 
 {- | The pair bonding operator @P.@`>>=` is a context-sensitive
-version of `Data.Profunctor.Monoidal.>*<`.
+version of `>*<`.
 
 prop> x >*< y = x P.>>= (\_ -> y)
 -}
@@ -44,9 +51,20 @@ infixl 1 >>=
 p >>= f = do
   b <- lmap fst p
   d <- lmap snd (f b)
-  return (b,d)
+  pure (b,d)
 
 {- | @P.@`>>` sequences actions. -}
 (>>) :: Monadic p => p () c -> p a b -> p a b
 infixl 1 >>
 x >> y = do _ <- lmap (const ()) x; y
+
+{- | @P.@`return` is a `Monadic`-restricted
+version of `pureP`.
+
+prop> pureP = P.return
+-}
+return :: (Monadic p, Choice p) => Prism a b () () -> p a b
+return = pureP
+
+{- | A `Profunctor` which is also a `MonadTry`. -}
+type MonadicTry p = (Profunctor p, forall x. MonadTry (p x))
diff --git a/src/Data/Profunctor/Monoidal.hs b/src/Data/Profunctor/Monoidal.hs
index b1aefa7..615bdc1 100644
--- a/src/Data/Profunctor/Monoidal.hs
+++ b/src/Data/Profunctor/Monoidal.hs
@@ -16,7 +16,7 @@ module Data.Profunctor.Monoidal
   , oneP, (>*<), (>*), (*<)
   , dimap2, foreverP, ditraverse
     -- * Monoidal & Choice
-  , replicateP, (>:<), asEmpty
+  , pureP, asEmpty, (>:<), replicateP, onlyOne
   , meander, eotFunList
   ) where
 
@@ -25,6 +25,7 @@ import Control.Applicative qualified as Ap (WrappedArrow)
 import Control.Arrow
 import Control.Lens hiding (chosen)
 import Control.Lens.Internal.Context
+import Control.Lens.Internal.Prism
 import Control.Lens.Internal.Profunctor
 import Control.Lens.PartialIso
 import Data.Bifunctor.Clown
@@ -39,6 +40,7 @@ import Data.Profunctor.Cayley
 import Data.Profunctor.Composition
 import Data.Profunctor.Monad
 import Data.Profunctor.Yoneda
+import GHC.IsList
 
 -- Monoidal --
 
@@ -93,44 +95,70 @@ infixl 6 *<
 analagous to `liftA2`. -}
 dimap2
   :: Monoidal p
-  => (s -> a)
-  -> (s -> c)
-  -> (b -> d -> t)
+  => (s -> a) -- ^ first projection, e.g. `fst`
+  -> (s -> c) -- ^ second projection, e.g. `snd`
+  -> (b -> d -> t) -- ^ pairing function, e.g. @(,)@
   -> p a b -> p c d -> p s t
 dimap2 f g h p q = liftA2 h (lmap f p) (lmap g q)
 
-{- | `foreverP` repeats an action indefinitely;
+{- | `foreverP` repeats an action a countable infinity of times;
 analagous to `Control.Monad.forever`, extending it to `Monoidal`. -}
 foreverP :: Monoidal p => p () c -> p a b
 foreverP a = let a' = a >* a' in a'
 
-{- | A `Monoidal` & `Choice` nil operator. -}
-asEmpty :: (AsEmpty s, Monoidal p, Choice p) => p s s
-asEmpty = _Empty >? oneP
-
-{- | A `Monoidal` & `Choice` cons operator. -}
-(>:<) :: (Cons s t a b, Monoidal p, Choice p) => p a b -> p s t -> p s t
-x >:< xs = _Cons >? x >*< xs
-infixr 5 >:<
-
 {- | Thanks to Fy on Monoidal Café Discord.
 
 A `Traversable` & `Data.Distributive.Distributive` type
 is a homogeneous countable product.
-That means it is a static length container, so unlike `replicateP`,
-`ditraverse` does not need an `Int` argument.
+That means it is a static countable-length container,
+so unlike `replicateP`, `ditraverse` doesn't need
+an additional argument for number of repetitions.
 -}
 ditraverse
   :: (Traversable t, Distributive t, Monoidal p)
   => p a b -> p (t a) (t b)
 ditraverse p = traverse (\f -> lmap f p) (distribute id)
 
+{- | Lift a single bidirectional element
+into a `Monoidal` & `Choice` structure.
+Bidirectionality is encoded by `APrism`.
+Singularity is encoded by the unit type @()@.
+Bidirectional elements can be generated from
+nilary constructors of algebraic datatypes using `makeNestedPrisms`,
+from terms of a type with an `Eq` instance using `only`,
+from nil elements using `_Empty`,
+or from any `.`-composition of `Control.Lens.Prism.Prism`s
+terminating with a bidirectional element.
+-}
+pureP
+  :: (Monoidal p, Choice p)
+  => APrism a b () () -- ^ bidirectional element
+  -> p a b
+pureP pattern = pattern >? oneP
+
+{- | A `Monoidal` & `Choice` nil combinator. -}
+asEmpty :: (AsEmpty s, Monoidal p, Choice p) => p s s
+asEmpty = pureP _Empty
+
+{- | A `Monoidal` & `Choice` cons combinator. -}
+(>:<) :: (Cons s t a b, Monoidal p, Choice p) => p a b -> p s t -> p s t
+x >:< xs = _Cons >? x >*< xs
+infixr 5 >:<
+
+{- | Use when `IsList` with `onlyOne` `Item`. -}
+onlyOne
+  :: (Monoidal p, Choice p, IsList s)
+  => p (Item s) (Item s) -> p s s
+onlyOne p = iso toList (fromListN 1) >? p >:< asEmpty
+
 {- | `replicateP` is analagous to `Control.Monad.replicateM`,
-for `Monoidal` & `Choice` `Profunctor`s. -}
+for `Monoidal` & `Choice` `Profunctor`s. When the number
+of repetitions is less than or equal to 0, it returns `asEmpty`.
+-}
 replicateP
-  :: (Monoidal p, Choice p, AsEmpty s, AsEmpty t, Cons s t a b)
-  => Int -> p a b -> p s t
-replicateP n _ | n <= 0 = lmap (const Empty) asEmpty
+  :: (Monoidal p, Choice p, AsEmpty s, Cons s s a a)
+  => Int {- ^ number of repetitions -} -> p a a -> p s s
+replicateP n _ | n <= 0 = asEmpty
 replicateP n a = a >:< replicateP (n-1) a
 
 {- | For any `Monoidal`, `Choice` & `Strong` `Profunctor`,
@@ -247,3 +275,14 @@ instance (Profunctor p, Alternative (p a))
     empty = proreturn empty
     ab <|> cd = proreturn (proextract ab <|> proextract cd)
     many = proreturn . many . proextract
+instance Applicative (Market a b s) where
+  pure t = Market (pure t) (pure (Left t))
+  Market f0 g0 <*> Market f1 g1 = Market
+    (\b -> f0 b (f1 b))
+    (\s ->
+      case g0 s of
+        Left bt -> case g1 s of
+          Left b -> Left (bt b)
+          Right a -> Right a
+        Right a -> Right a
+    )
diff --git a/src/Data/Profunctor/Separator.hs b/src/Data/Profunctor/Separator.hs
new file mode 100644
index 0000000..21b4d18
--- /dev/null
+++ b/src/Data/Profunctor/Separator.hs
@@ -0,0 +1,127 @@
+{-|
+Module      : Data.Profunctor.Separator
+Description : separators
+Copyright   : (C) 2026 - Eitan Chatav
+License     : BSD-style (see the file LICENSE)
+Maintainer  : Eitan Chatav <eitan.chatav@gmail.com>
+Stability   : provisional
+Portability : non-portable
+-}
+
+module Data.Profunctor.Separator
+  ( -- * SepBy
+    SepBy (..)
+  , sepBy
+  , noSep
+  , sepWith
+  , beginWith
+  , endWith
+    -- * SepBy Combinators
+  , several
+  , several1
+  , chain
+  , chain1
+  , intercalateP
+  ) where
+
+import Control.Lens
+import Control.Lens.PartialIso
+import Control.Lens.Grammar.Symbol
+import Data.Profunctor.Distributor
+import Data.Profunctor.Monoidal
+import GHC.Exts
+
+{- | Used to sequence multiple times,
+separated by a `separateBy`,
+begun by a `beginBy`,
+and ended by an `endBy`. -}
+data SepBy p = SepBy
+  { beginBy :: p
+  , endBy :: p
+  , separateBy :: p
+  } deriving stock
+    ( Functor, Foldable, Traversable
+    , Eq, Ord, Show, Read
+    )
+
+{- | A `SepBy` smart constructor,
+setting the `separateBy` field.
+Beginning and ending delimitors will be no-ops,
+except by modifier record updates `beginBy` or `endBy`. -}
+sepBy :: Applicative p => p () -> SepBy (p ())
+sepBy = SepBy (pure ()) (pure ())
+
+{- | A `SepBy` smart constructor for no separator,
+beginning or ending delimiters. -}
+noSep :: Applicative p => SepBy (p ())
+noSep = sepBy (pure ())
+
+{- | A `SepBy` smart constructor like `sepBy`,
+with a `terminal` argument.
+Beginning and ending delimitors will be no-ops,
+except by applying smart modifiers `beginWith` or `endWith`. -}
+sepWith
+  :: (Applicative p, TerminalSymbol c (p ()))
+  => [c] -> SepBy (p ())
+sepWith = sepBy . terminal
+
+{- | A `SepBy` smart modifier like `beginBy`,
+with a `terminal` argument. -}
+beginWith :: TerminalSymbol c p => [c] -> SepBy p -> SepBy p
+beginWith str separator = separator {beginBy = terminal str}
+
+{- | A `SepBy` smart modifier like `endBy`,
+with a `terminal` argument. -}
+endWith :: TerminalSymbol c p => [c] -> SepBy p -> SepBy p
+endWith str separator = separator {endBy = terminal str}
+
+{- |
+prop> several noSep = manyP
+-}
+several
+  :: (IsList s, IsList t, Distributor p)
+  => SepBy (p () ()) -> p (Item s) (Item t) -> p s t
+several (SepBy beg end sep) p = iso toList fromList . eotList >~
+  beg >* (p >*< manyP (sep >* p) >+< oneP) *< end
+
+{- |
+prop> several1 noSep = someP
+-}
+several1
+  :: (IsList s, IsList t, Distributor p, Choice p)
+  => SepBy (p () ()) -> p (Item s) (Item t) -> p s t
+several1 (SepBy beg end sep) p = iso toList fromList . _Cons >?
+  beg >* (p >*< manyP (sep >* p)) *< end
+
+{- | Use a nilary constructor pattern to sequence zero times, or
+associate a binary constructor pattern to sequence one or more times. -}
+chain
+  :: Alternator p
+  => (forall x. x -> Either x x) -- ^ `Left` or `Right` associate
+  -> APartialIso a b (a,a) (b,b) -- ^ binary constructor pattern
+  -> APrism a b () () -- ^ nilary constructor pattern
+  -> SepBy (p () ()) -> p a b -> p a b
+chain association pat2 pat0 (SepBy beg end sep) p =
+  beg >* optionP pat0 (chain1 association pat2 (sepBy sep) p) *< end
+
+{- | Associate a binary constructor pattern to sequence one or more times. -}
+chain1
+  :: (Distributor p, Choice p)
+  => (forall x. x -> Either x x) -- ^ `Left` or `Right` associate
+  -> APartialIso a b (a,a) (b,b) -- ^ binary constructor pattern
+  -> SepBy (p () ()) -> p a b -> p a b
+chain1 association pat (SepBy beg end sep) = leftOrRight chainl1 chainr1
+  where
+    leftOrRight a b = case association () of Left _ -> a; Right _ -> b
+    chainl1 p = difoldl pat >? beg >* p >*< manyP (sep >* p) *< end
+    chainr1 p = difoldr pat >? beg >* manyP (p *< sep) >*< p *< end
+
+{- | Add a `SepBy` to `replicateP` using `intercalateP`. -}
+intercalateP
+  :: (Monoidal p, Choice p, AsEmpty s, Cons s s a a)
+  => Int {- ^ number of repetitions -}
+  -> SepBy (p () ()) -> p a a -> p s s
+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
diff --git a/src/Data/Traversable/Homogeneous.hs b/src/Data/Traversable/Homogeneous.hs
new file mode 100644
index 0000000..52589af
--- /dev/null
+++ b/src/Data/Traversable/Homogeneous.hs
@@ -0,0 +1,142 @@
+{-|
+Module      : Data.Traversable.Homogeneous
+Description : homogeneous
+Copyright   : (C) 2026 - Eitan Chatav
+License     : BSD-style (see the file LICENSE)
+Maintainer  : Eitan Chatav <eitan.chatav@gmail.com>
+Stability   : provisional
+Portability : non-portable
+-}
+
+module Data.Traversable.Homogeneous
+  ( -- * Homogeneous
+    Homogeneous (..)
+  ) where
+
+import Control.Applicative
+import Control.Lens hiding (chosen)
+import Control.Lens.PartialIso
+import Data.Complex
+import Data.Functor.Compose
+import qualified Data.Functor.Product as Functor
+import qualified Data.Functor.Sum as Functor
+import qualified Data.Monoid as Monoid
+import Data.Profunctor.Monoidal
+import Data.Proxy
+import Data.Sequence (Seq)
+import Data.Tagged
+import Data.Tree (Tree (..))
+import Data.Vector (Vector)
+import Data.Void
+import GHC.Generics
+
+import Data.Profunctor.Distributor
+
+{- | A class of `Homogeneous`
+countable sums of countable products.
+-}
+class Traversable t => Homogeneous t where
+  {- | Sequences actions `homogeneously`.
+
+  prop> homogeneously @Maybe = optionalP
+  prop> homogeneously @[] = manyP
+
+  Any `Traversable` & `Data.Distributive.Distributive` countable product
+  can be given a default implementation for the `homogeneously` method
+  with `ditraverse`.
+
+  prop> homogeneously = ditraverse
+
+  And any user-defined homogeneous algebraic datatype has
+  a default instance for `Homogeneous`, by deriving `Generic1`.
+  -}
+  homogeneously :: Distributor p => p a b -> p (t a) (t b)
+  default homogeneously
+    :: (Generic1 t, Homogeneous (Rep1 t), Distributor p)
+    => p a b -> p (t a) (t b)
+  homogeneously = dimap from1 to1 . homogeneously
+instance Homogeneous Par1 where
+  homogeneously = dimap unPar1 Par1
+instance Homogeneous Identity where
+  homogeneously = dimap runIdentity Identity
+instance Homogeneous Monoid.Dual where
+  homogeneously = dimap Monoid.getDual Monoid.Dual
+instance Homogeneous Monoid.Product where
+  homogeneously = dimap Monoid.getProduct Monoid.Product
+instance Homogeneous Monoid.Sum where
+  homogeneously = dimap Monoid.getSum Monoid.Sum
+instance Homogeneous (Tagged s) where
+  homogeneously = dimap unTagged Tagged
+instance Homogeneous U1 where
+  homogeneously _ = pure U1
+instance Homogeneous (K1 i ()) where
+  homogeneously _ = pure (K1 ())
+instance Homogeneous (Const ()) where
+  homogeneously _ = pure (Const ())
+instance Homogeneous Proxy where
+  homogeneously _ = pure Proxy
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (s :.: t) where
+    homogeneously
+      = dimap unComp1 Comp1
+      . homogeneously . homogeneously
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (Compose s t) where
+    homogeneously
+      = dimap getCompose Compose
+      . homogeneously . homogeneously
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (s :*: t) where
+    homogeneously p = dimap2
+      (\(s :*: _) -> s)
+      (\(_ :*: t) -> t)
+      (:*:)
+      (homogeneously p)
+      (homogeneously p)
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (Functor.Product s t) where
+    homogeneously p = dimap2
+      (\(Functor.Pair s _) -> s)
+      (\(Functor.Pair _ t) -> t)
+      Functor.Pair
+      (homogeneously p)
+      (homogeneously p)
+instance Homogeneous V1 where
+  homogeneously _ = dimap (\case) (\case) zeroP
+instance Homogeneous (K1 i Void) where
+  homogeneously _ = dimap unK1 K1 zeroP
+instance Homogeneous (Const Void) where
+  homogeneously _ = dimap getConst Const zeroP
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (s :+: t) where
+    homogeneously p = dialt
+      (\case {L1 s -> Left s; R1 t -> Right t})
+      L1
+      R1
+      (homogeneously p)
+      (homogeneously p)
+instance (Homogeneous s, Homogeneous t)
+  => Homogeneous (Functor.Sum s t) where
+    homogeneously p = dialt
+      (\case {Functor.InL s -> Left s; Functor.InR t -> Right t})
+      Functor.InL
+      Functor.InR
+      (homogeneously p)
+      (homogeneously p)
+instance Homogeneous t
+  => Homogeneous (M1 i c t) where
+    homogeneously = dimap unM1 M1 . homogeneously
+instance Homogeneous f => Homogeneous (Rec1 f) where
+  homogeneously = dimap unRec1 Rec1 . homogeneously
+instance Homogeneous Maybe where
+  homogeneously = optionalP
+instance Homogeneous [] where
+  homogeneously = manyP
+instance Homogeneous Vector where
+  homogeneously p = eotList >~ p >*< homogeneously p >+< oneP
+instance Homogeneous Seq where
+  homogeneously p = eotList >~ p >*< homogeneously p >+< oneP
+instance Homogeneous Complex where
+  homogeneously p = dimap2 realPart imagPart (:+) p p
+instance Homogeneous Tree where
+  homogeneously p = dimap2 rootLabel subForest Node p (manyP (homogeneously p))
diff --git a/test/Examples/Arithmetic.hs b/test/Examples/Arithmetic.hs
index 4a40f2d..f7ee1bb 100644
--- a/test/Examples/Arithmetic.hs
+++ b/test/Examples/Arithmetic.hs
@@ -7,12 +7,6 @@ module Examples.Arithmetic
 import Control.Applicative
 import Control.Lens
 import Control.Lens.Grammar
-import Control.Lens.Grammar.BackusNaur
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso
-import Data.Profunctor.Distributor
-import Data.Profunctor.Monoidal
 import Numeric.Natural
 
 data Arith
@@ -27,9 +21,9 @@ arithGrammar :: Grammar Char Arith
 arithGrammar = ruleRec "arith" sumG
   where
     sumG arith = rule "sum" $
-      chain1 Left _Add (sepBy (terminal "+")) (prodG arith)
+      chain1 Left _Add (sepWith "+") (prodG arith)
     prodG arith = rule "product" $
-      chain1 Left _Mul (sepBy (terminal "*")) (factorG arith)
+      chain1 Left _Mul (sepWith "*") (factorG arith)
     factorG arith = rule "factor" $
       number <|> terminal "(" >* arith *< terminal ")"
     number = rule "number" $
diff --git a/test/Examples/Chain.hs b/test/Examples/Chain.hs
new file mode 100644
index 0000000..5d0f964
--- /dev/null
+++ b/test/Examples/Chain.hs
@@ -0,0 +1,36 @@
+module Examples.Chain
+  ( Chain (..)
+  , chainGrammar
+  , chainExamples
+  ) where
+
+import Control.Applicative
+import Control.Lens
+import Control.Lens.Grammar
+
+data Chain
+  = Emp
+  | Char Char
+  | Seq Chain Chain
+  deriving stock (Eq, Ord, Show, Read)
+
+makePrisms ''Chain
+
+chainGrammar :: CtxGrammar Char Chain
+chainGrammar = ruleRec "chain" seqG
+  where
+    seqG chn = rule "seq" $
+      chain Left _Seq _Emp noSep (atomG chn)
+    atomG chn = rule "atom" $
+      _Char >? charG <|> terminal "(" >* chn *< terminal ")"
+    charG = notOneOf "()\\"
+      <|> terminal "\\" >* oneOf "()\\"
+
+chainExamples :: [(Chain, String)]
+chainExamples =
+  [ (Char 'x', "x")
+  , (Seq (Char '1') (Char '2'), "12")
+  , (Seq (Seq (Char 'x') (Char 'y')) (Char 'z'), "xyz")
+  , (Seq (Char 'x') (Seq (Char 'y') (Char 'z')), "x(yz)")
+  , (Emp, "")
+  ]
diff --git a/test/Examples/Json.hs b/test/Examples/Json.hs
index 79cc5f9..e3aec52 100644
--- a/test/Examples/Json.hs
+++ b/test/Examples/Json.hs
@@ -7,13 +7,6 @@ module Examples.Json
 import Control.Applicative
 import Control.Lens
 import Control.Lens.Grammar
-import Control.Lens.Grammar.BackusNaur
-import Control.Lens.Grammar.Boole
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso
-import Data.Profunctor.Distributor
-import Data.Profunctor.Monoidal
 import qualified Data.Map.Strict as Map
 import Data.Map.Strict (Map)
 import Numeric.Natural
@@ -60,7 +53,7 @@ jsonGrammar = ruleRec "json" elementG
 
     -- members = member | member ',' members
     membersG json = rule "members" $
-      several1 (sepBy (terminal ",")) (memberG json)
+      several1 (sepWith ",") (memberG json)
 
     -- member = ws string ws ':' element
     memberG json = rule "member" $
@@ -74,7 +67,7 @@ jsonGrammar = ruleRec "json" elementG
 
     -- elements = element | element ',' elements
     elementsG json = rule "elements" $
-      several1 (sepBy (terminal ",")) (elementG json)
+      several1 (sepWith ",") (elementG json)
 
     -- string = '"' characters '"'
     stringG = rule "string" $
diff --git a/test/Examples/Lambda.hs b/test/Examples/Lambda.hs
index bee41e3..3c43425 100644
--- a/test/Examples/Lambda.hs
+++ b/test/Examples/Lambda.hs
@@ -6,12 +6,6 @@ module Examples.Lambda
 
 import Control.Lens
 import Control.Lens.Grammar
-import Control.Lens.Grammar.BackusNaur
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso
-import Data.Profunctor.Distributor
-import Data.Profunctor.Monoidal
 
 -- | Abstract syntax tree for lambda calculus terms
 data Lambda
@@ -40,7 +34,7 @@ lambdaGrammar = ruleRec "lambda" termG
     -- Application: left-associative chain of atoms
     -- e.g., "f x y" parses as "(f x) y"
     appG term = rule "application" $
-      chain1 Left _App (sepBy (terminal " ")) (atomG term)
+      chain1 Left _App (sepWith " ") (atomG term)
 
     -- Atomic term: variable or parenthesized term
     atomG term = rule "atom" $ choice
diff --git a/test/Examples/LenVec.hs b/test/Examples/LenVec.hs
index a37b608..13483dc 100644
--- a/test/Examples/LenVec.hs
+++ b/test/Examples/LenVec.hs
@@ -5,10 +5,6 @@ module Examples.LenVec
   ) where
 
 import Control.Lens.Grammar
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso
-import Data.Profunctor.Distributor
 import qualified Data.Profunctor.Monadic as P
 import Numeric.Natural
 
@@ -21,7 +17,7 @@ lenvecGrammar :: CtxGrammar Char LenVec
 lenvecGrammar = _LenVec >? P.do
   let
     numberG = iso show read >~ someP (asIn @Char DecimalNumber)
-    vectorG n = intercalateP n (sepBy (terminal ",")) numberG
+    vectorG n = intercalateP n (sepWith ",") numberG
   len <- numberG             -- bonds to _LenVec
   terminal ";"               -- doesn't bond
   vectorG (fromIntegral len) -- bonds to _LenVec
diff --git a/test/Examples/RegString.hs b/test/Examples/RegString.hs
index 3e6a23e..bdd1bdf 100644
--- a/test/Examples/RegString.hs
+++ b/test/Examples/RegString.hs
@@ -3,17 +3,14 @@ module Examples.RegString
   ) where
 
 import Control.Lens.Grammar
-import Control.Lens.Grammar.Boole
-import Control.Lens.Grammar.Kleene
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
 
 regexExamples :: [(RegString, String)]
 regexExamples =
   [ (terminal "abc123etc.", "abc123etc.")
   , (terminal "x" <> terminal "y", "xy")
   , (zeroK, "[]")
-  , (terminal "x" >|< terminal "y", "x|y")
+  , (terminal "xy" >|< terminal "z", "xy|z")
+  , (token 'x' >|< token 'y', "[xy]")
   , (optK (terminal "x"), "x?")
   , (starK (terminal "x"), "x*")
   , (plusK (terminal "x"), "x+")
@@ -29,13 +26,10 @@ regexExamples =
 
   -- Boolean OR (>||<) operations
   , (tokenClass (oneOf "abc" >||< oneOf "xyz"), "[abcxyz]")
-  , (tokenClass (notOneOf "abc" >||< notOneOf "xyz"), "[^]")
   , (tokenClass (oneOf "abc" >||< notOneOf "xyz"), "[abc]|[^xyz]")
   , (tokenClass (notOneOf "abc" >||< oneOf "xyz"), "[^abc]|[xyz]")
   , (tokenClass (asIn UppercaseLetter >||< asIn LowercaseLetter), "\\p{Lu}|\\p{Ll}")
-  , (tokenClass (notAsIn Control >||< notAsIn Space), "[^]")
   , (tokenClass (oneOf "abc" >||< asIn DecimalNumber), "[abc]|\\p{Nd}")
-  , (tokenClass (notOneOf "xyz" >||< notAsIn UppercaseLetter), "[^]")
 
   -- Boolean AND (>&&<) operations
   , (tokenClass (oneOf "abcdef" >&&< oneOf "def123"), "[def]")
@@ -45,7 +39,7 @@ regexExamples =
   , (tokenClass (notOneOf "abc" >&&< notAsIn Control), "[^abc\\P{Cc}]")
   , (tokenClass (asIn UppercaseLetter >&&< notOneOf "XYZ"), "[^XYZ\\p{Lu}]")
   , (tokenClass (notAsIn Control >&&< notAsIn Space), "\\P{Zs|Cc}")
-  , (tokenClass (oneOf "0123456789" >&&< asIn DecimalNumber), "[0123456789]")
+  , (tokenClass (oneOf "0123456789xyz" >&&< asIn DecimalNumber), "[0123456789]")
 
   -- Boolean NOT (notB) operations
   , (tokenClass (notB (oneOf "abc")), "[^abc]")
@@ -55,9 +49,9 @@ regexExamples =
   , (tokenClass (notB (notAsIn Control)), "\\p{Cc}")
   , (tokenClass (notB (notOneOf "abc" >&&< asIn LowercaseLetter)), "[abc]|\\P{Ll}")
 
-  -- fromBool operations
-  , (tokenClass (fromBool True), "[^]")
-  , (tokenClass (fromBool False), "[]")
+  -- trueB & falseB
+  , (tokenClass trueB, "[^]")
+  , (tokenClass falseB, "[]")
 
   -- Complex combinations
   , (tokenClass (notOneOf "abc" >&&< (asIn LowercaseLetter >||< asIn UppercaseLetter)), "[^abc\\p{Ll}]|\\p{Lu}")
diff --git a/test/Examples/SExpr.hs b/test/Examples/SExpr.hs
index 84ebe5b..5cef3e4 100644
--- a/test/Examples/SExpr.hs
+++ b/test/Examples/SExpr.hs
@@ -5,14 +5,7 @@ module Examples.SExpr
   ) where
 
 import Control.Lens hiding (List)
-import Control.Lens.Grammar
-import Control.Lens.Grammar.BackusNaur
-import Control.Lens.Grammar.Boole
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso hiding (List)
-import Data.Profunctor.Distributor
-import Data.Profunctor.Monoidal
+import Control.Lens.Grammar hiding (List)
 
 -- | Abstract syntax tree for S-expressions
 data SExpr
@@ -36,7 +29,7 @@ sexprGrammar = ruleRec "sexpr" $ \sexpr -> choice
     -- List: parenthesized sequence of S-expressions
     -- Elements are separated by whitespace
     listG sexpr = rule "list" $
-      terminal "(" >* several (sepBy (terminal " ")) sexpr *< terminal ")"
+      terminal "(" >* several (sepWith " ") sexpr *< terminal ")"
 
     -- Characters allowed in atoms: letters, digits, and symbols
     atomChars =
diff --git a/test/Examples/SemVer.hs b/test/Examples/SemVer.hs
index ffc5792..c8f2ba5 100644
--- a/test/Examples/SemVer.hs
+++ b/test/Examples/SemVer.hs
@@ -6,13 +6,9 @@ module Examples.SemVer
   ) where
 
 import Control.Applicative
+import Control.Lens
 import Control.Lens.Grammar
-import Control.Lens.Grammar.Symbol
-import Control.Lens.Grammar.Token
-import Control.Lens.PartialIso
-import Data.Profunctor.Distributor
 import qualified Data.Profunctor.Monadic as P
-import Data.Profunctor.Monoidal
 import Numeric.Natural
 
 -- | Semantic version structure following semver.org specification
@@ -42,11 +38,11 @@ semverGrammar = _SemVer
   >?  numberG
   >*< terminal "." >* numberG
   >*< terminal "." >* numberG
-  >*< option [] (terminal "-" >* identifiersG)
-  >*< option [] (terminal "+" >* identifiersG)
+  >*< optionP _Empty (terminal "-" >* identifiersG)
+  >*< optionP _Empty (terminal "+" >* identifiersG)
   where
     numberG = iso show read >~ someP (asIn @Char DecimalNumber)
-    identifiersG = several1 (sepBy (terminal ".")) (someP charG)
+    identifiersG = several1 (sepWith ".") (someP charG)
     charG = asIn LowercaseLetter
       <|> asIn UppercaseLetter
       <|> asIn DecimalNumber
@@ -57,7 +53,7 @@ semverCtxGrammar :: CtxGrammar Char SemVer
 semverCtxGrammar = _SemVer >? P.do
   let
     numberG = iso show read >~ someP (asIn @Char DecimalNumber)
-    identifiersG = several1 (sepBy (terminal ".")) (someP charG)
+    identifiersG = several1 (sepWith ".") (someP charG)
     charG = asIn LowercaseLetter
       <|> asIn UppercaseLetter
       <|> asIn DecimalNumber
@@ -65,8 +61,8 @@ semverCtxGrammar = _SemVer >? P.do
   _ <- numberG
   _ <- terminal "." >* numberG
   _ <- terminal "." >* numberG
-  _ <- option [] (terminal "-" >* identifiersG)
-  option [] (terminal "+" >* identifiersG)
+  _ <- optionP _Empty (terminal "-" >* identifiersG)
+  optionP _Empty (terminal "+" >* identifiersG)
 
 semverExamples :: [(SemVer, String)]
 semverExamples =
diff --git a/test/Main.hs b/test/Main.hs
index 06bb306..6c71fca 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,39 +1,42 @@
 module Main (main) where
 
 import Data.Foldable hiding (toList)
-import Data.Maybe (listToMaybe)
 import Control.Lens.Grammar
+import Control.Monad (when)
+import Data.List (genericLength)
 import Test.DocTest
 import Test.Hspec
 
-import Examples.RegString
 import Examples.Arithmetic
+import Examples.Chain
 import Examples.Json
-import Examples.SExpr
 import Examples.Lambda
 import Examples.LenVec
+import Examples.RegString
 import Examples.SemVer
+import Examples.SExpr
+import Properties.Kleene
 
 main :: IO ()
 main = do
-  doctests
   hspec $ do
-    testGrammar "regexGrammar" regexGrammar regexExamples
-    testGrammar "semverGrammar" semverGrammar semverExamples
-    testGrammar "semverCtxGrammar" semverCtxGrammar semverExamples
-    testGrammar "arithGrammar" arithGrammar arithExamples
-    testGrammar "jsonGrammar" jsonGrammar jsonExamples
-    testGrammar "sexprGrammar" sexprGrammar sexprExamples
-    testGrammar "lambdaGrammar" lambdaGrammar lambdaExamples
-    testGrammar "lenvecGrammar" lenvecGrammar lenvecExamples
+    describe "regexGrammar" $ for_ regexExamples $ testGrammar False regexGrammar
+    describe "semverGrammar" $ for_ semverExamples $ testCtxGrammar True semverGrammar
+    describe "semverCtxGrammar" $ for_ semverExamples $ testCtxGrammar True semverCtxGrammar
+    describe "arithGrammar" $ for_ arithExamples $ testGrammar True arithGrammar
+    describe "jsonGrammar" $ for_ jsonExamples $ testCtxGrammar False jsonGrammar
+    describe "sexprGrammar" $ for_ sexprExamples $ testCtxGrammar True sexprGrammar
+    describe "lambdaGrammar" $ for_ lambdaExamples $ testCtxGrammar True lambdaGrammar
+    describe "lenvecGrammar" $ for_ lenvecExamples $ testCtxGrammar True lenvecGrammar
+    describe "chainGrammar" $ for_ chainExamples $ testCtxGrammar True chainGrammar
+    describe "Kleene" kleeneProperties
+  doctests
 
 doctests :: IO ()
 doctests = do
   let
     modulePaths =
-      [ "src/Control/Lens/Grammar.hs"
-      , "src/Control/Lens/Grammar/Token.hs"
-      ]
+      [ "src/Control/Lens/Grammar.hs" ]
     languageExtensions =
       [ "-XAllowAmbiguousTypes"
       , "-XArrows"
@@ -77,16 +80,36 @@ doctests = do
     putStrLn modulePath
     doctest (modulePath : languageExtensions)
 
-testGrammar :: (Show a, Eq a) => String -> CtxGrammar Char a -> [(a, String)] -> Spec
-testGrammar name grammar examples =
-  describe name $
-    for_ examples $ \(expectedSyntax, expectedString) -> do
-      it ("should parse from " <> expectedString <> " correctly") $ do
-        let actualSyntax = [parsed | (parsed, "") <- parseG grammar expectedString]
-        listToMaybe actualSyntax `shouldBe` Just expectedSyntax
-      it ("should unparse to " <> expectedString <> " correctly") $ do
-        let actualString = unparseG grammar expectedSyntax ""
-        actualString `shouldBe` Just expectedString
-      it ("should print to " <> expectedString <> " correctly") $ do
-        let actualString = ($ "") <$> printG grammar expectedSyntax
-        actualString `shouldBe` Just expectedString
+testGrammar :: (Show a, Eq a) => Bool -> Grammar Char a -> (a, String) -> Spec
+testGrammar isLL1 grammar (expectedSyntax, expectedString) = do
+  testCtxGrammar isLL1 grammar (expectedSyntax, expectedString)
+  it ("should match " <> expectedString <> " correctly") $ do
+    let actualMatch = expectedString =~ regbnfG grammar
+    actualMatch `shouldBe` True
+
+testCtxGrammar :: (Show a, Eq a) => Bool -> CtxGrammar Char a -> (a, String) -> Spec
+testCtxGrammar isLL1 grammar (expectedSyntax, expectedString) = do
+  it ("should parseG from " <> expectedString <> " correctly") $ do
+    let actualSyntax = [parsed | (parsed, "") <- parseG grammar expectedString]
+    actualSyntax `shouldBe` [expectedSyntax]
+  it ("should unparseG to " <> expectedString <> " correctly") $ do
+    let actualString = unparseG grammar expectedSyntax ""
+    actualString `shouldBe` Just expectedString
+  it ("should printG to " <> expectedString <> " correctly") $ do
+    let actualString = ($ "") <$> printG grammar expectedSyntax
+    actualString `shouldBe` Just expectedString
+  when isLL1 $ do
+    it ("should parsecG from " <> expectedString <> " correctly") $ do
+      let actualSyntax = parsecG grammar expectedString
+      let expectedLength = genericLength expectedString
+      let actualLooked = parsecLooked actualSyntax
+      let actualHint   = parsecHint   actualSyntax
+      actualSyntax `shouldBe`
+        (ParsecState actualLooked expectedLength "" actualHint (Right expectedSyntax))
+    it ("should unparsecG to " <> expectedString <> " correctly") $ do
+      let actualString = unparsecG grammar expectedSyntax ""
+      let expectedLength = genericLength expectedString
+      let actualLooked = parsecLooked actualString
+      let actualHint   = parsecHint   actualString
+      actualString `shouldBe`
+        (ParsecState actualLooked expectedLength expectedString actualHint (Right expectedSyntax))
diff --git a/test/Properties/Kleene.hs b/test/Properties/Kleene.hs
new file mode 100644
index 0000000..7aa7ca3
--- /dev/null
+++ b/test/Properties/Kleene.hs
@@ -0,0 +1,120 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+module Properties.Kleene (kleeneProperties) where
+
+import Control.Lens.Grammar
+import Test.Hspec
+import Test.Hspec.QuickCheck (prop)
+import Test.QuickCheck
+
+instance Arbitrary GeneralCategory where
+  arbitrary = arbitraryBoundedEnum
+  shrink = shrinkBoundedEnum
+
+instance Arbitrary (TokenClass Char) where
+  arbitrary = sized go
+    where
+      go 0 = frequency
+        [ (1, pure falseB)
+        , (1, pure trueB)
+        , (4, oneOf <$> (arbitrary :: Gen [Char]))
+        , (4, notOneOf <$> (arbitrary :: Gen [Char]))
+        , (3, asIn <$> arbitrary)
+        , (3, notAsIn <$> arbitrary)
+        ]
+      go n = frequency
+        [ (2, go 0)
+        , (2, (>||<) <$> go (n `div` 2) <*> go (n `div` 2))
+        , (2, (>&&<) <$> go (n `div` 2) <*> go (n `div` 2))
+        , (1, notB <$> go (n - 1))
+        ]
+
+instance Arbitrary (RegEx Char) where
+  arbitrary = sized go
+    where
+      go 0 = frequency
+        [ (1, pure (zeroK :: RegEx Char))
+        , (1, pure (mempty :: RegEx Char))
+        , (6, tokenClass <$> (arbitrary :: Gen (TokenClass Char)))
+        ]
+      go n = frequency
+        [ (2, go 0)
+        , (2, (<>) <$> go (n `div` 2) <*> go (n `div` 2))
+        , (2, (>|<) <$> go (n `div` 2) <*> go (n `div` 2))
+        , (1, starK <$> go (n - 1))
+        , (1, plusK <$> go (n - 1))
+        , (1, optK <$> go (n - 1))
+        ]
+
+kleeneProperties :: Spec
+kleeneProperties = do
+  describe "KleeneStarAlgebra" $ do
+    prop "starK x = optK (plusK x)" $ \(x :: RegEx Char) ->
+      starK x == optK (plusK x)
+    prop "plusK x = x <> starK x" $ \(x :: RegEx Char) ->
+      plusK x == x <> starK x
+    prop "optK x = mempty >|< x" $ \(x :: RegEx Char) ->
+      optK x == (mempty >|< x)
+    prop "x >|< x = x" $ \(x :: RegEx Char) ->
+      (x >|< x) == x
+    prop "zeroK >|< x = x" $ \(x :: RegEx Char) ->
+      (zeroK >|< x) == x
+    prop "x >|< zeroK = x" $ \(x :: RegEx Char) ->
+      (x >|< zeroK) == x
+    prop "x >|< mempty = optK x" $ \(x :: RegEx Char) ->
+      (x >|< mempty) == optK x
+    prop "zeroK <> x = zeroK" $ \(x :: RegEx Char) ->
+      (zeroK <> x) == zeroK
+    prop "x <> zeroK = zeroK" $ \(x :: RegEx Char) ->
+      (x <> zeroK) == zeroK
+    prop "mempty <> x = x" $ \(x :: RegEx Char) ->
+      (mempty <> x) == x
+    prop "x <> mempty = x" $ \(x :: RegEx Char) ->
+      (x <> mempty) == x
+  describe "TokenAlgebra" $ do
+    it "zeroK = tokenClass falseB" $
+      (zeroK :: RegEx Char) `shouldBe` tokenClass falseB
+    prop "tokenClass x >|< tokenClass y = tokenClass (x >||< y)" $
+      \(x :: TokenClass Char) (y :: TokenClass Char) ->
+        ((tokenClass x :: RegEx Char) >|< tokenClass y)
+          == tokenClass (x >||< y)
+  describe "TokenAlgebra RegEx" $ do
+    it "anyToken = tokenClass anyToken" $
+      (anyToken :: RegEx Char) `shouldBe` tokenClass anyToken
+    prop "token c = tokenClass (token c)" $
+      \(c :: Char) ->
+        (token c :: RegEx Char) == tokenClass (token c)
+    prop "oneOf cs = tokenClass (oneOf cs)" $
+      \(cs :: [Char]) ->
+        (oneOf cs :: RegEx Char) == tokenClass (oneOf cs)
+    prop "notOneOf cs = tokenClass (notOneOf cs)" $
+      \(cs :: [Char]) ->
+        (notOneOf cs :: RegEx Char) == tokenClass (notOneOf cs)
+    prop "asIn cat = tokenClass (asIn cat)" $
+      \(cat :: GeneralCategory) ->
+        (asIn cat :: RegEx Char) == tokenClass (asIn cat)
+    prop "notAsIn cat = tokenClass (notAsIn cat)" $
+      \(cat :: GeneralCategory) ->
+        (notAsIn cat :: RegEx Char) == tokenClass (notAsIn cat)
+  describe "BooleanAlgebra TokenClass" $ do
+    it "trueB = anyToken" $
+      (trueB :: TokenClass Char) `shouldBe` anyToken
+    it "trueB = notOneOf []" $
+      (trueB :: TokenClass Char) `shouldBe` notOneOf []
+    it "falseB = oneOf []" $
+      (falseB :: TokenClass Char) `shouldBe` oneOf []
+    prop "notB . oneOf = notOneOf" $
+      \(cs :: [Char]) ->
+        notB (oneOf cs :: TokenClass Char) == notOneOf cs
+    prop "notB . notOneOf = oneOf" $
+      \(cs :: [Char]) ->
+        notB (notOneOf cs :: TokenClass Char) == oneOf cs
+    prop "notB . asIn = notAsIn" $
+      \(cat :: GeneralCategory) ->
+        notB (asIn cat :: TokenClass Char) == notAsIn cat
+    prop "notB . notAsIn = asIn" $
+      \(cat :: GeneralCategory) ->
+        notB (notAsIn cat :: TokenClass Char) == asIn cat
+    prop "x >||< x = x" $ \(x :: TokenClass Char) ->
+      (x >||< x) == x
+    prop "x >&&< x = x" $ \(x :: TokenClass Char) ->
+      (x >&&< x) == x