diff --git a/diff-containers/diff-containers.cabal b/diff-containers/diff-containers.cabal
index 89075a7..94dd4d0 100644
--- a/diff-containers/diff-containers.cabal
+++ b/diff-containers/diff-containers.cabal
@@ -52,6 +52,7 @@ test-suite test
   build-depends:      base              >=4.9 && <4.17
                     , containers
                     , diff-containers
+                    , groups
                     , nonempty-containers
                     , QuickCheck
                     , simple-semigroupoids
diff --git a/diff-containers/src/Data/Map/Diff/Strict.hs b/diff-containers/src/Data/Map/Diff/Strict.hs
index d3e17ff..bbffe85 100644
--- a/diff-containers/src/Data/Map/Diff/Strict.hs
+++ b/diff-containers/src/Data/Map/Diff/Strict.hs
@@ -1,3 +1,28 @@
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+
+-- | Differences on @'Map'@s with a @'Group'@ instance.
+--
+-- === Positivity and normality
+--
+-- It is an unfortunate side effect of facilitating a @'Group'@ instance for
+-- @'Diff'@s that we can get into situations where applying diffs will fail or
+-- produce wrong results due to diffs containing internally unresolved sums and
+-- subtractions. The responsibility of downstream code is to ensure that diffs
+-- that are applied are both /positive/ (@'isPositive'@) and /normal/
+-- @('isNormal')@. If that is the case, then applying diffs will never go wrong.
+--
+-- * Positivity: a positive diff contains only Inserts and Deletes.
+-- * Normality: a normal diff (i.e., a diff that is in normal form) has resolved
+--   all sums and subtrations internally. This is the case if there are no
+--   consecutive diff entries in a diff history that can still be cancelled out.
+--
+-- Note: a positive diff is by definition also a normal diff. Normality is a
+-- weaker property than positivity.
+--
+-- A number of definitions in this modules are annotated with PRECONDITION,
+-- INVARIANT and POSTCONDITION. Use these and the type class laws for
+-- @'Semigroup'@, @'Monoid'@ and @'Group'@ (which hold given preconditions) to
+-- ensure that applied diffs are always both positive and normal.
 module Data.Map.Diff.Strict (
     -- * Types
     Diff
@@ -18,6 +43,9 @@ module Data.Map.Diff.Strict (
     -- ** Size
   , null
   , size
+    -- ** Positivity and normality
+  , isNormal
+  , isPositive
     -- * Applying diffs
   , applyDiff
   , applyDiffForKeys
@@ -30,4 +58,7 @@ module Data.Map.Diff.Strict (
 
 import           Prelude hiding (null)
 
+import           Data.Group (Group)
+import           Data.Map.Strict (Map)
+
 import           Data.Map.Diff.Strict.Internal
diff --git a/diff-containers/src/Data/Map/Diff/Strict/Internal.hs b/diff-containers/src/Data/Map/Diff/Strict/Internal.hs
index a12ad7b..5edd931 100644
--- a/diff-containers/src/Data/Map/Diff/Strict/Internal.hs
+++ b/diff-containers/src/Data/Map/Diff/Strict/Internal.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE ViewPatterns               #-}
 
+-- | See the module documentation for "Data.Map.Diff.Strict".
 module Data.Map.Diff.Strict.Internal (
     -- * Types
     Diff (..)
@@ -42,6 +43,11 @@ module Data.Map.Diff.Strict.Internal (
     -- ** Size
   , null
   , size
+    -- ** Positivity and normality
+  , isNormal
+  , isNormalDiffHistory
+  , isPositive
+  , isPositiveDiffHistory
     -- * @'Group'@ instances
   , areInverses
   , invertDiffEntry
@@ -103,7 +109,11 @@ newtype NEDiffHistory v = NEDiffHistory { getNEDiffHistory :: NESeq (DiffEntry v
 data DiffEntry v =
       Insert !v
     | Delete !v
+      -- | Considered unsafe to act on. Consider throwing an error when pattern
+      -- matching on this constructor.
     | UnsafeAntiInsert !v
+      -- | Considered unsafe to act on. Consider throwing an error when pattern
+      -- matching on this constructor.
     | UnsafeAntiDelete !v
   deriving stock (Generic, Show, Eq, Functor)
   deriving anyclass (NoThunks)
@@ -129,6 +139,9 @@ nonEmptyDiffHistory (DiffHistory sq) = NEDiffHistory <$> NESeq.nonEmptySeq sq
 ------------------------------------------------------------------------------}
 
 -- | Compute the difference between @'Map'@s.
+--
+-- POSTCONDITION: diffing computes a @'Diff'@ that is both normal and
+-- positive.
 diff :: (Ord k, Eq v) => Map k v -> Map k v -> Diff k v
 diff m1 m2 = Diff $
     Merge.merge
@@ -199,10 +212,52 @@ null (Diff m) = Map.null m
 size :: Diff k v -> Int
 size (Diff m) = Map.size m
 
+-- | A positive diff contains only @'Insert'@s and @'Delete'@s. A negative diff
+-- can also contain @'UnsafeAntiInsert'@s and @'UnsafeAntiDelete'@s, which makes
+-- applying diffs unsafe.
+--
+-- Note: a positive diff is by definition also a normal diff.
+isPositive :: Diff k v -> Bool
+isPositive (Diff m) = all (isPositiveDiffHistory . toDiffHistory) m
+
+-- | Check if a diff history is positive, which means it can only contain
+-- @'Insert'@s and @'Delete'@s.
+--
+-- Note: a positive diff history is by definition also a normal diff history.
+isPositiveDiffHistory :: DiffHistory v -> Bool
+isPositiveDiffHistory (DiffHistory vs) = all p vs
+  where
+    p (Insert _)           = True
+    p (Delete _)           = True
+    p (UnsafeAntiInsert _) = False
+    p (UnsafeAntiDelete _) = False
+
+-- | A diff that is in normal form has resolved all sums and subtractions
+-- internally. Applying a non-normal diff is considered unsafe.
+isNormal :: Eq v => Diff k v -> Bool
+isNormal (Diff d) = all (isNormalDiffHistory . toDiffHistory) d
+
+-- | Check if a diff history is in normal form, where no succesive elements are
+-- inverses of each other.
+--
+-- If two succesive diff entries are inverses, they can be cancelled out. In
+-- other words, we can normalise the diff history further by cancelling out the
+-- diff entries. If so, we can conclude that the input diff history is not in
+-- normal form.
+isNormalDiffHistory :: Eq v => DiffHistory v -> Bool
+isNormalDiffHistory (DiffHistory vs) = case vs of
+  Empty     -> True
+  _ :<| des -> not $ any (uncurry areInverses) (Seq.zip vs des)
+
 {------------------------------------------------------------------------------
   @'Group'@ instances
 ------------------------------------------------------------------------------}
 
+-- | Summing of diffs.
+--
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: Summing preserves both positivity and normality.
 instance (Ord k, Eq v) => Semigroup (Diff k v) where
   Diff m1 <> Diff m2 = Diff $
     Merge.merge
@@ -214,9 +269,19 @@ instance (Ord k, Eq v) => Semigroup (Diff k v) where
       m1
       m2
 
+-- | Identity diffs.
+--
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: @'mempty'@ is both positive and normal.
 instance (Ord k, Eq v) => Monoid (Diff k v) where
   mempty = Diff mempty
 
+-- | Inverting diffs.
+--
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: @'invert'@ preserves normality.
 instance (Ord k, Eq v) => Group (Diff k v) where
   invert (Diff m) = Diff $
     fmap (unsafeFromDiffHistory . invert . toDiffHistory) m
@@ -224,12 +289,21 @@ instance (Ord k, Eq v) => Group (Diff k v) where
 -- | @h1 <> h2@ sums @h1@ and @h2@ by cancelling out as many consecutive diff
 -- entries as possible, and appending the remainders.
 --
--- Diff entries that are each other's inverse can cancel out: @'Delete'@ cancels
--- out any @'Insert' x@, and vice versa.
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: Summing preserves both positivity and normality.
+--
+-- Diff entries that are each other's inverse (irrespective of their order) can
+-- cancel out:
+--
+-- * @'UnsafeAntiInsert' x@ cancels out any @'Insert' y@ if @x == y@.
+--
+-- * @'UnsafeAntiDelete' x@ cancels out any @'Delete' y@ if @x == y@.
 --
 -- Note: We do not cancel out consecutive elements in @h1@ and @h2@
 -- individually. It is only at the border between @h1@ and @h2@ that we cancel
--- out elements.
+-- out elements. This means that @'mappend'@ing two diff histories does not by
+-- definition return a normal diff.
 instance Eq v => Semigroup (DiffHistory v) where
   DiffHistory s1 <> DiffHistory s2 = DiffHistory $ s1 `mappend'` s2
     where
@@ -240,16 +314,27 @@ instance Eq v => Semigroup (DiffHistory v) where
         | areInverses x y                    = mappend' xs ys
       mappend' xs ys                         = xs Seq.>< ys
 
+-- | Identity diff histories.
+--
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: @'mempty'@ is both positive and normal.
 instance Eq v => Monoid (DiffHistory v) where
   mempty = DiffHistory mempty
 
+-- | Inverting diff histories.
+--
+-- PRECONDITION: Normality is required for type class laws to hold.
+--
+-- INVARIANT: @'invert'@ preserves normality.
 instance Eq v => Group (DiffHistory v) where
   invert (DiffHistory s) = DiffHistory $ Seq.reverse . fmap invertDiffEntry $ s
 
 -- | @`invertDiffEntry` e@ inverts a @'DiffEntry' e@ to its counterpart.
 --
--- Note: We invert @DiffEntry@s, but it is not a @Group@: We do not have an
--- identity element, so it is not a @Monoid@ or @Semigroup@.
+-- Note: We invert @'DiffEntry'@s, but a @'DiffEntry'@ is not a @'Group'@: we do
+-- not have an identity element, so @'DiffEntry'@ is not a @'Monoid'@ or
+-- @'Semigroup'@.
 invertDiffEntry :: DiffEntry v -> DiffEntry v
 invertDiffEntry = \case
   Insert x           -> UnsafeAntiInsert x
@@ -257,10 +342,8 @@ invertDiffEntry = \case
   UnsafeAntiInsert x -> Insert x
   UnsafeAntiDelete x -> Delete x
 
--- | @'areInverses e1 e2@ checks whether @e1@ and @e2@ are each other's inverse.
---
--- For simplicity, we simply compare the inverse of the first argument to the
--- second argument. That is, inversion should be invertible.
+-- | @'areInverses' e1 e2@ checks whether @e1@ and @e2@ are each other's
+-- inverse.
 areInverses :: Eq v => DiffEntry v -> DiffEntry v -> Bool
 areInverses e1 e2 = invertDiffEntry e1 == e2
 
@@ -269,6 +352,10 @@ areInverses e1 e2 = invertDiffEntry e1 == e2
 ------------------------------------------------------------------------------}
 
 -- | Applies a diff to a @'Map'@.
+--
+-- PRECONDITION: The diff that is to be applied is both normal and positive.
+--
+-- POSTCONDITION: The result is @'Right' m@ for some @m@.
 applyDiff ::
      Ord k
   => Map k v
@@ -297,6 +384,10 @@ applyDiff m (Diff diffs) =
       UnsafeAntiDelete _ -> Left ()
 
 -- | Applies a diff to a @'Map'@ for a specific set of keys.
+--
+-- PRECONDITION: The diff that is to be applied is both normal and positive.
+--
+-- POSTCONDITION: The result is @'Right' m@ for some @m@.
 applyDiffForKeys ::
      Ord k
   => Map k v
@@ -309,6 +400,10 @@ applyDiffForKeys m ks (Diff diffs) =
     (Diff $ diffs `Map.restrictKeys` (Map.keysSet m `Set.union` ks))
 
 -- | Applies a diff to a @'Map'@, throws an error if applying the diff failed.
+--
+-- PRECONDITION: The diff that is to be applied is both normal and positive.
+--
+-- POSTCONDITION: No error is thrown.
 unsafeApplyDiff ::
      Ord k
   => Map k v
@@ -319,6 +414,10 @@ unsafeApplyDiff m d = fromRight (error "applyDiff failed") $
 
 -- | Applies a diff to a @'Map'@ for a specific set of keys, throws an error if
 -- applying the diff failed.
+--
+-- PRECONDITION: The diff that is to be applied is both normal and positive.
+--
+-- POSTCONDITION: No error is thrown.
 unsafeApplyDiffForKeys ::
      Ord k
   => Map k v
diff --git a/diff-containers/test/Test/Data/Map/Diff/Strict.hs b/diff-containers/test/Test/Data/Map/Diff/Strict.hs
index ac147b7..2e67d8a 100644
--- a/diff-containers/test/Test/Data/Map/Diff/Strict.hs
+++ b/diff-containers/test/Test/Data/Map/Diff/Strict.hs
@@ -2,12 +2,15 @@
 {-# LANGUAGE GeneralisedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving         #-}
 {-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE ViewPatterns               #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Data.Map.Diff.Strict (tests) where
 
+import           Data.Either
 import           Data.Foldable
+import           Data.Group (Group (..))
 import           Data.Map.Strict (Map)
 import           Data.Maybe
 import           Data.Proxy (Proxy (Proxy))
@@ -43,41 +46,131 @@ import           Test.Util
 -- small values often.
 tests :: TestTree
 tests = testGroup "Data.Map.Diff.Strict" [
-      localOption (QuickCheckTests 1000) $
-      testGroupWithProxy (Proxy @(DiffHistory (OftenSmall Int))) [
+      localOption (QuickCheckTests 10000) $
+      testGroupWithProxy (Proxy @(NormalDiffHistory (OftenSmall Int))) [
           testSemigroupLaws
         , testMonoidLaws
         , testGroupLaws
         ]
     , localOption (QuickCheckTests 1000) $
-      testGroupWithProxy (Proxy @(Diff (OftenSmall Int) (OftenSmall Int))) [
+      testGroupWithProxy (Proxy @(NormalDiff (OftenSmall Int) (OftenSmall Int))) [
           testSemigroupLaws
         , testMonoidLaws
         , testGroupLaws
         ]
+    , testGroup "Diffing" [
+          localOption (QuickCheckTests 10000) $
+          testProperty "prop_diffingIsPositive" $
+            prop_diffingIsPositive @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 10000) $
+          testProperty "prop_diffingIsNormal" $
+            prop_diffingIsNormal @(OftenSmall Int) @(OftenSmall Int)
+        ]
     , localOption (QuickCheckTests 10000) $
-      testProperty "prop_diffingIsPositive" $
-        prop_diffingIsPositive @(OftenSmall Int) @(OftenSmall Int)
-    , localOption (QuickCheckTests 10000) $
-      testProperty "prop_diffThenApply" $
-        prop_diffThenApply @(OftenSmall Int) @(OftenSmall Int)
-    , localOption (QuickCheckTests 10000) $
-      testProperty "prop_applyMempty" $
-        prop_applyMempty @(OftenSmall Int) @(OftenSmall Int)
-    , localOption (QuickCheckMaxRatio 100) $
-      localOption (QuickCheckTests 1000) $
-      testProperty "prop_applyAllAndApplySum" $
-        prop_applyAllAndApplySum @(OftenSmall Int) @(OftenSmall Int)
-    , localOption (QuickCheckMaxRatio 100) $
-      localOption (QuickCheckTests 1000) $
-      testProperty "prop_unsafeApplyAllAndUnsafeApplySum" $
-        prop_unsafeApplyAllAndUnsafeApplySum @(OftenSmall Int) @(OftenSmall Int)
+      testGroup "Positive implies normal" [
+          testProperty "prop_positiveDiffImpliesNormalDiff" $
+            prop_positiveDiffImpliesNormalDiff @(OftenSmall Int) @(OftenSmall Int)
+        , testProperty "prop_positiveDiffHistoryImpliesNormalDiffHistory" $
+            prop_positiveDiffHistoryImpliesNormalDiffHistory @(OftenSmall Int)
+        ]
+    , testGroup "Preserving positivity and normality" [
+          localOption (QuickCheckTests 1000) $
+          testProperty "prop_summingDiffsPreservesPositivity" $
+            prop_summingDiffsPreservesPositivity @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 10000) $
+          testProperty "prop_summingDiffHistoriesPreservesPositivity" $
+            prop_summingDiffHistoriesPreservesPositivity @(OftenSmall Int)
+        , localOption (QuickCheckTests 10000) $
+          testProperty "prop_summingDiffsPreservesNormality" $
+            prop_summingDiffsPreservesNormality @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 100000) $
+          testProperty "prop_summingDiffHistoriesPreservesNormality" $
+            prop_summingDiffHistoriesPreservesNormality @(OftenSmall Int)
+        , localOption (QuickCheckTests 10000) $
+          testProperty "prop_invertingDiffsPreservesNormality" $
+            prop_invertingDiffsPreservesNormality @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 100000) $
+          testProperty "prop_invertingDiffHistoriesPreservesNormality" $
+            prop_invertingDiffHistoriesPreservesNormality @(OftenSmall Int)
+        ]
+    , testGroup "Positivity and normality for identity elements" [
+          testProperty "prop_emptyDiffIsPositive" prop_emptyDiffIsPositive
+        , testProperty "prop_emptyDiffHistoryIsPositive" prop_emptyDiffHistoryIsPositive
+        , testProperty "prop_emptyDiffIsNormal" prop_emptyDiffIsNormal
+        , testProperty "prop_emptyDiffHistoryIsNormal" prop_emptyDiffHistoryIsNormal
+        ]
+    , testGroup "Applying diffs" [
+          localOption (QuickCheckTests 10000) $
+          testProperty "prop_diffThenApply" $
+            prop_diffThenApply @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 10000) $
+          testProperty "prop_applyMempty" $
+            prop_applyMempty @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 100) $
+          testProperty "prop_applyAllAndApplySum" $
+            prop_applyAllAndApplySum @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 1000) $
+          testProperty "prop_normalAndPositiveDiffsNeverFailApply" $
+            prop_normalAndPositiveDiffsNeverFailApply @(OftenSmall Int) @(OftenSmall Int)
+        , localOption (QuickCheckTests 1000) $
+          testProperty "prop_normalAndPositiveDiffsNeverFailUnsafeApply" $
+            prop_normalAndPositiveDiffsNeverFailUnsafeApply @(OftenSmall Int) @(OftenSmall Int)
+        ]
+    , testGroup "Generators" [
+          testGroup "All diffs and diff histories" [
+              testProperty "arbitrary/shrunk Diff is not always positive" $ expectFailure $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(Diff (OftenSmall Int) (OftenSmall Int))
+                  isPositive
+            , testProperty "arbitrary/shrunk DiffHistory is not always positive" $ expectFailure $
+                prop_arbitrarySatisfiesProperty
+                  @(DiffHistory (OftenSmall Int))
+                  isPositiveDiffHistory
+            , testProperty "arbitrary/shrunk Diff is not always normal" $ expectFailure $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(Diff (OftenSmall Int) (OftenSmall Int))
+                  isNormal
+            , testProperty "arbitrary/shrunk DiffHistory is not always normal" $ expectFailure $
+                prop_arbitrarySatisfiesProperty
+                  @(DiffHistory (OftenSmall Int))
+                  isNormalDiffHistory
+            ]
+        , testGroup "Normal diffs and diff histories" [
+              testProperty "arbitrary/shrunk NormalDiff is always in normal form" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(NormalDiff (OftenSmall Int) (OftenSmall Int))
+                  (isNormal . getNormalDiff)
+            , testProperty "arbitrary/shrunk NormalDiff is always in normal form" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(NormalDiffHistory (OftenSmall Int))
+                  (isNormalDiffHistory . getNormalDiffHistory)
+            ]
+        , testGroup "Positive diffs and diff histories" [
+              testProperty "arbitrary/shrunk PositiveDiff is always positive" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(PositiveDiff (OftenSmall Int) (OftenSmall Int))
+                  (isPositive . getPositiveDiff)
+            , testProperty "arbitrary/shrunk PositiveDiffHistory is always positive" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(PositiveDiffHistory (OftenSmall Int))
+                  (isPositiveDiffHistory . getPositiveDiffHistory)
+            , testProperty "arbitrary/shrunk PositiveDiff is always normal" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(PositiveDiff (OftenSmall Int) (OftenSmall Int))
+                  (isNormal . getPositiveDiff)
+            , testProperty "arbitrary/shrunk PositiveDiffHistory is always normal" $
+                prop_arbitraryAndShrinkSatisfyProperty
+                  @(PositiveDiffHistory (OftenSmall Int))
+                  (isNormalDiffHistory . getPositiveDiffHistory)
+            ]
+        ]
     ]
 
 {------------------------------------------------------------------------------
   Simple properties
 ------------------------------------------------------------------------------}
 
+-- | A @'Diff'@ computed from two @'Map'@s is positive.
 prop_diffingIsPositive ::
      (Ord k, Eq v)
   => Map k v
@@ -85,6 +178,116 @@ prop_diffingIsPositive ::
   -> Property
 prop_diffingIsPositive m1 m2 = property $ isPositive (diff m1 m2)
 
+-- | A @'Diff'@ computed from two @'Map'@s is normal.
+prop_diffingIsNormal ::
+     (Ord k, Eq v)
+  => Map k v
+  -> Map k v
+  -> Property
+prop_diffingIsNormal m1 m2 = property $ isNormal (diff m1 m2)
+
+--
+-- Positive implies normal
+--
+
+-- | A positive diff is implied to be normal.
+prop_positiveDiffImpliesNormalDiff ::
+     Eq v
+  => PositiveDiff k v
+  -> Property
+prop_positiveDiffImpliesNormalDiff (PositiveDiff d) =
+  property $ isNormal d
+
+-- | A positive diff history is implied to be normal.
+prop_positiveDiffHistoryImpliesNormalDiffHistory ::
+     Eq v
+  => PositiveDiffHistory v
+  -> Property
+prop_positiveDiffHistoryImpliesNormalDiffHistory (PositiveDiffHistory h) =
+  property $ isNormalDiffHistory h
+
+--
+-- Preserving positivity and normality
+--
+
+-- | Test the invariant that summing @'Diff'@s preserves positivity.
+prop_summingDiffsPreservesPositivity ::
+     (Ord k, Eq v)
+  => PositiveDiff k v
+  -> PositiveDiff k v
+  -> Property
+prop_summingDiffsPreservesPositivity (PositiveDiff d1) (PositiveDiff d2) =
+  property $ isPositive (d1 <> d2)
+
+-- | Test the invariant that summing @'DiffHistory'@s preserves positivity.
+prop_summingDiffHistoriesPreservesPositivity ::
+     Eq v
+  => PositiveDiffHistory v
+  -> PositiveDiffHistory v
+  -> Property
+prop_summingDiffHistoriesPreservesPositivity (PositiveDiffHistory h1) (PositiveDiffHistory h2) =
+  property $ isPositiveDiffHistory (h1 <> h2)
+
+-- | Test the invariant that summing @'Diff'@s preserves normality.
+prop_summingDiffsPreservesNormality ::
+     (Ord k, Eq v)
+  => NormalDiff k v
+  -> NormalDiff k v
+  -> Property
+prop_summingDiffsPreservesNormality (NormalDiff d1) (NormalDiff d2) =
+  property $ isNormal (d1 <> d2)
+
+-- | Test the invariant that summing @'DiffHistory'@s preserves normality.
+prop_summingDiffHistoriesPreservesNormality ::
+     Eq v
+  => NormalDiffHistory v
+  -> NormalDiffHistory v
+  -> Property
+prop_summingDiffHistoriesPreservesNormality (NormalDiffHistory h1) (NormalDiffHistory h2) =
+  property $ isNormalDiffHistory (h1 <> h2)
+
+-- | Test the invariant that inverting @'Diff'@s preserves normality.
+prop_invertingDiffsPreservesNormality ::
+     (Ord k, Eq v)
+  => NormalDiff k v
+  -> Property
+prop_invertingDiffsPreservesNormality (NormalDiff d) =
+  property $ isNormal (invert d)
+
+-- | Test the invariant that inverting @'DiffHistory'@s preserves normality.
+prop_invertingDiffHistoriesPreservesNormality ::
+     Eq v
+  => NormalDiffHistory v
+  -> Property
+prop_invertingDiffHistoriesPreservesNormality (NormalDiffHistory h) =
+  property $ isNormalDiffHistory (invert h)
+
+--
+-- Positivity and normality for identity elements
+--
+
+-- | Test the invariant that the identity @'Diff'@ element is positive.
+prop_emptyDiffIsPositive :: Property
+prop_emptyDiffIsPositive = once $ isPositive (mempty :: Diff Int Int)
+
+-- | Test the invariant that the identity @'DiffHistory'@ element is positive.
+prop_emptyDiffHistoryIsPositive :: Property
+prop_emptyDiffHistoryIsPositive = once $ isPositiveDiffHistory (mempty :: DiffHistory Int)
+
+-- | Test the invariant that the identity @'Diff'@ element is normal.
+prop_emptyDiffIsNormal :: Property
+prop_emptyDiffIsNormal = once $ isNormal (mempty :: Diff Int Int)
+
+-- | Test the invariant that the identity @'DiffHistory'@ element is normal.
+prop_emptyDiffHistoryIsNormal:: Property
+prop_emptyDiffHistoryIsNormal = once $ isNormalDiffHistory (mempty :: DiffHistory Int)
+
+--
+-- Applying diffs
+--
+
+-- | Applying a @'Diff'@ computed from a source and target @'Map'@ should
+-- produce the target @'Map'@.
 prop_diffThenApply ::
      (Show k, Show v, Ord k, Eq v)
   => Map k v
@@ -92,74 +295,86 @@ prop_diffThenApply ::
   -> Property
 prop_diffThenApply m1 m2 = applyDiff m1 (diff m1 m2) === Right m2
 
+-- | Applying an empty @'Diff'@ is the identity function.
 prop_applyMempty ::
      (Show k, Show v, Ord k, Eq v)
   => Map k v
   -> Property
 prop_applyMempty m = applyDiff m mempty === Right m
 
+-- | Applying a sum of normal and positive @'Diff'@s is equivalent to applying
+-- each (normal and positive) @'Diff'@ separately (in order).
 prop_applyAllAndApplySum ::
      (Show k, Show v, Ord k, Eq v)
   => Map k v
-  -> [Diff k v]
+  -> [PositiveDiff k v]
   -> Property
-prop_applyAllAndApplySum m ds =
-  all isPositive ds ==> foldlM applyDiff m ds === applyDiff m (mconcat ds)
+prop_applyAllAndApplySum m (fmap getPositiveDiff -> ds) =
+  foldlM applyDiff m ds === applyDiff m (mconcat ds)
 
-prop_unsafeApplyAllAndUnsafeApplySum ::
-     (Show k, Show v, Ord k, Eq v)
+-- | Applying a diff that is both positive and normal will never fail.
+prop_normalAndPositiveDiffsNeverFailApply ::
+     Ord k
   => Map k v
-  -> [Diff k v]
+  -> PositiveDiff k v
   -> Property
-prop_unsafeApplyAllAndUnsafeApplySum m ds =
-  all isPositive ds ==> foldl' unsafeApplyDiff m ds === unsafeApplyDiff m (mconcat ds)
+prop_normalAndPositiveDiffsNeverFailApply m (PositiveDiff d) =
+  property $ isRight (applyDiff m d)
 
-{------------------------------------------------------------------------------
-  Preconditions
-------------------------------------------------------------------------------}
+-- | Unsafely applying a diff that is both positive and normal will never throw
+-- an error.
+prop_normalAndPositiveDiffsNeverFailUnsafeApply ::
+     Ord k
+  => Map k v
+  -> PositiveDiff k v
+  -> Property
+prop_normalAndPositiveDiffsNeverFailUnsafeApply m (PositiveDiff d) =
+  property $ unsafeApplyDiff m d `seq` ()
 
--- | Check if a diff history is in normal form, where no succesive elements are
--- inverses of each other.
 --
--- If two succesive diff entries are inverses, they can be cancelled out. In
--- other words, we can normalise the diff history further by cancelling out the
--- diff entries. If so, we can conclude that the input diff history is not in
--- normal form.
-isNormal :: Eq v => DiffHistory v -> Bool
-isNormal (DiffHistory vs) =
-    snd $ foldl' f (Nothing, True) vs
-  where
-    f (prevMay, b) cur = case prevMay of
-      Nothing   -> (Just cur, b)
-      Just prev -> (Just cur, b && not (areInverses prev cur))
-
-isPositive :: Diff k v -> Bool
-isPositive (Diff m) = all (isPositiveDiffHistory . toDiffHistory) m
-
-isPositiveDiffHistory :: DiffHistory v -> Bool
-isPositiveDiffHistory (DiffHistory vs) = all p vs
-  where
-    p (Insert _)           = True
-    p (Delete _)           = True
-    p (UnsafeAntiInsert _) = False
-    p (UnsafeAntiDelete _) = False
+-- Generators
+--
+
+-- | Check whether values generated by an @'Arbitrary'@ instance satisfy a
+-- property.
+prop_arbitrarySatisfiesProperty ::
+     (Show a, Arbitrary a)
+  => (a -> Bool)
+  -> Property
+prop_arbitrarySatisfiesProperty p = forAll arbitrary (property . p)
+
+-- | Check whether values shrunk by an @'Arbitrary'@ instance
+-- satisfy a property.
+prop_shrinkSatisfiesProperty ::
+     (Show a, Arbitrary a)
+  => (a -> Bool)
+  -> Property
+prop_shrinkSatisfiesProperty p = forAll arbitrary (property . all p . shrink)
+
+
+-- | Check whether values generated and shrunk by an @'Arbitrary'@ instance
+-- satisfy a property.
+prop_arbitraryAndShrinkSatisfyProperty ::
+     (Show a, Arbitrary a)
+  => (a -> Bool)
+  -> Property
+prop_arbitraryAndShrinkSatisfyProperty p =
+  prop_arbitrarySatisfiesProperty p .&&. prop_shrinkSatisfiesProperty p
 
 {------------------------------------------------------------------------------
-  Types
+  Plain @'Arbitrary'@ instances
 ------------------------------------------------------------------------------}
 
-deriving newtype instance (Ord k, Eq v, Arbitrary k, Arbitrary v)
+deriving newtype instance (Ord k, Arbitrary k, Arbitrary v)
                        => Arbitrary (Diff k v)
 
-instance (Arbitrary v, Eq v) => Arbitrary (NEDiffHistory v) where
-  arbitrary = (NEDiffHistory <$> ((:<||) <$> arbitrary <*> arbitrary))
-    `suchThat` (isNormal . toDiffHistory)
+instance Arbitrary v => Arbitrary (NEDiffHistory v) where
+  arbitrary = NEDiffHistory <$> ((:<||) <$> arbitrary <*> arbitrary)
   shrink (NEDiffHistory h) =
     fmap NEDiffHistory $ mapMaybe NESeq.nonEmptySeq $ shrink (NESeq.toSeq h)
 
-instance (Arbitrary v, Eq v) => Arbitrary (DiffHistory v) where
-  arbitrary = (DiffHistory <$> arbitrary)
-    `suchThat` isNormal
+instance Arbitrary v => Arbitrary (DiffHistory v) where
+  arbitrary = DiffHistory <$> arbitrary
   shrink (DiffHistory s) = DiffHistory <$> shrink s
 
 instance Arbitrary v => Arbitrary (DiffEntry v) where
@@ -174,3 +389,61 @@ instance Arbitrary v => Arbitrary (DiffEntry v) where
     Delete x           -> Delete <$> shrink x
     UnsafeAntiInsert x -> UnsafeAntiInsert <$> shrink x
     UnsafeAntiDelete x -> UnsafeAntiDelete <$> shrink x
+
+{------------------------------------------------------------------------------
+  Modifiers: positivity
+------------------------------------------------------------------------------}
+
+-- | A @'Diff'@ for which @'isPositive'@ holds.
+newtype PositiveDiff k v = PositiveDiff { getPositiveDiff :: Diff k v }
+  deriving stock (Show, Eq)
+  deriving newtype (Semigroup, Monoid, Group)
+
+instance (Ord k, Arbitrary k, Arbitrary v)
+      => Arbitrary (PositiveDiff k v) where
+  arbitrary =
+    PositiveDiff <$> arbitrary `suchThat` isPositive
+  shrink (PositiveDiff d) =
+    [PositiveDiff d' | d' <- shrink d, isPositive d']
+
+-- | A @'DiffHistory'@ for which @'isPositiveDiffHistory'@ holds.
+newtype PositiveDiffHistory v = PositiveDiffHistory {
+    getPositiveDiffHistory :: DiffHistory v
+  }
+  deriving stock (Show, Eq)
+  deriving newtype (Semigroup, Monoid, Group)
+
+instance Arbitrary v => Arbitrary (PositiveDiffHistory v) where
+  arbitrary =
+    PositiveDiffHistory <$> arbitrary `suchThat` isPositiveDiffHistory
+  shrink (PositiveDiffHistory h) =
+    [PositiveDiffHistory h' | h' <- shrink h, isPositiveDiffHistory h']
+
+{------------------------------------------------------------------------------
+  Modifiers: normality
+------------------------------------------------------------------------------}
+
+-- | A @'Diff'@ for which @'isNormal'@ holds.
+newtype NormalDiff k v = NormalDiff { getNormalDiff :: Diff k v }
+  deriving stock (Show, Eq)
+  deriving newtype (Semigroup, Monoid, Group)
+
+instance (Ord k, Eq v, Arbitrary k, Arbitrary v)
+      => Arbitrary (NormalDiff k v) where
+  arbitrary =
+    NormalDiff <$> arbitrary `suchThat` isNormal
+  shrink (NormalDiff d) =
+    [NormalDiff d' | d' <- shrink d, isNormal d']
+
+-- | A @'DiffHistory'@ for which @'isNormalDiffHistory'@ holds.
+newtype NormalDiffHistory v = NormalDiffHistory {
+    getNormalDiffHistory :: DiffHistory v
+  }
+  deriving stock (Show, Eq)
+  deriving newtype (Semigroup, Monoid, Group)
+
+instance (Arbitrary v, Eq v) => Arbitrary (NormalDiffHistory v) where
+  arbitrary =
+    NormalDiffHistory <$> arbitrary `suchThat` isNormalDiffHistory
+  shrink (NormalDiffHistory h) =
+    [NormalDiffHistory h' | h' <- shrink h, isNormalDiffHistory h']