diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -113,6 +113,17 @@ let lwwResolved = lww (\(t1, _) (t2, _) -> compare t1 t2) "actor" conflictDvv ``` +### Partial Ordering and Causality + +DVVs implement a **Partial Order** to represent the causal relationship between versions. This is exposed via the `PartialOrd` typeclass (from `lattices` or `Algebra.PartialOrd`). + +- **`leq` (Less than or Equal):** `A <= B` means that `A` is a causal ancestor of (or equal to) `B`. In other words, `B` "knows" everything `A` knows. + - Implementation: For every actor in `A`'s history, `B`'s history must have a counter greater than or equal to `A`'s. +- **Strict Inequality:** `A < B` means `A <= B` AND `A /= B`. `A` happened strictly before `B`. +- **Concurrent (Incomparable):** If neither `A <= B` nor `B <= A` holds, then `A` and `B` are **concurrent** (`||`). This indicates a conflict that needs to be resolved. + +The `sync` operation computes the Least Upper Bound (LUB) of two DVVs, effectively merging their histories and preserving all concurrent values (siblings) until they are reconciled. + ## Type Safety This library uses `HashMap` internally for efficiency and requires actor IDs to be instances of `Hashable`. The `DVV` type is also an instance of `Functor`, `Foldable`, and `Traversable`, making it easy to manipulate the stored values. diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,2 +1,5 @@ +# 0.1.1.0 [James R. Thompson](mailto:jamesthompsonoxford@gmail.com) January 2026 +Fix broken ordering instances + # 0.1.0.0 [James R. Thompson](mailto:jamesthompsonoxford@gmail.com) January 2026 Initial library for basic DVV definitions and operations. diff --git a/dvv.cabal b/dvv.cabal --- a/dvv.cabal +++ b/dvv.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: dvv -version: 0.1.0.0 +version: 0.1.1.0 license: MIT license-file: LICENSE copyright: 2026-Present, James R. Thompson @@ -35,7 +35,8 @@ build-depends: base >=4.14 && <5, unordered-containers >=0.2.0.0 && <0.3, - hashable >=1.4.0.0 && <1.6 + hashable >=1.4.0.0 && <1.6, + lattices >=2.0 && <2.3 test-suite dvv-test type: exitcode-stdio-1.0 @@ -55,4 +56,5 @@ hspec, QuickCheck, unordered-containers, - hashable + hashable, + lattices diff --git a/src/Data/DVV.hs b/src/Data/DVV.hs --- a/src/Data/DVV.hs +++ b/src/Data/DVV.hs @@ -3,41 +3,44 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE ScopedTypeVariables #-} --- | --- Module : Data.DVV --- Description : Dotted Version Vectors for causal tracking and conflict detection --- Copyright : (c) James R. Thompson --- License : BSD3 --- Stability : experimental --- --- Dotted Version Vectors (DVVs) provide a mechanism for tracking causality --- and detecting conflicts in distributed systems. This implementation supports --- efficient synchronization, event recording, and conflict resolution. -module Data.DVV - ( -- * Core Types - Count, - Dot (..), - VersionVector, - DVV (..), +{- | +Module : Data.DVV +Description : Dotted Version Vectors for causal tracking and conflict detection +Copyright : (c) James R. Thompson +License : BSD3 +Stability : experimental - -- * Operations - sync, - context, - event, - values, - prune, - reconcile, - lww, +Dotted Version Vectors (DVVs) provide a mechanism for tracking causality +and detecting conflicts in distributed systems. This implementation supports +efficient synchronization, event recording, and conflict resolution. +-} +module Data.DVV ( + -- * Core Types + Count, + Dot (..), + VersionVector (..), + DVV (..), - -- * Analysis - size, - ) + -- * Operations + sync, + context, + event, + values, + prune, + reconcile, + lww, + + -- * Analysis + mkVersionVector, + size, +) where +import Algebra.PartialOrd (PartialOrd (..)) import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as Map import Data.Hashable (Hashable (hashWithSalt)) -import Data.List (foldl', foldl1') +import Data.List (foldl', foldl1', sortBy) import Data.Maybe (fromMaybe) import Data.Word (Word64) import GHC.Generics (Generic) @@ -47,30 +50,104 @@ -- | A Dot is a pair of a replica ID and a logical counter. data Dot actorID = Dot !actorID !Count - deriving stock (Eq, Show, Ord, Functor, Foldable, Traversable, Generic) + deriving stock (Eq, Show, Functor, Generic) --- | Dot is a pair of an actor (identifier) and a logical counter, --- but we hash using the actor value only. +{- | Dots are partially ordered: two dots are comparable if and only if they +share the same actor ID, in which case they are ordered by their counter. +-} +instance (Eq actorID) => PartialOrd (Dot actorID) where + leq (Dot a1 c1) (Dot a2 c2) = a1 == a2 && c1 <= c2 + comparable (Dot a1 _) (Dot a2 _) = a1 == a2 + +{- | Dot is a pair of an actor (identifier) and a logical counter, +but we hash using the actor value only. +-} instance (Hashable actorID) => Hashable (Dot actorID) where hashWithSalt salt (Dot actorID _) = hashWithSalt salt actorID --- | A Version Vector is a mapping from actor IDs to their latest known counter. --- Requires keys to be Hashable. -type VersionVector actorID = HashMap actorID Count +{- | A Version Vector is a mapping from actor IDs to their latest known counter. +It stores a list of counts to actors for efficient leq checks. +Requires keys to be Hashable. +-} +data VersionVector actorID = VersionVector + { vvMap :: HashMap actorID Count + , vvDesc :: [(Count, actorID)] + } + deriving stock (Show, Generic) --- | A Dotted Version Vector (DVV) consisting of a Causal History (Version Vector) --- and a set of concurrent values associated with Dots. --- --- Note: A Singleton has no causal history, its counter is implicitly 1. --- --- @actorID@ is the type of actor IDs. Must be Hashable. --- @value@ is the type of the value stored. +instance (Eq actorID) => Eq (VersionVector actorID) where + (VersionVector m1 _) == (VersionVector m2 _) = m1 == m2 + +instance (Hashable actorID, Eq actorID) => PartialOrd (VersionVector actorID) where + leq (VersionVector _ sortedList) (VersionVector m2 _) = + all (\(c, a) -> c <= Map.findWithDefault 0 a m2) sortedList + +-- | Helper to construct valid VersionVector +mkVersionVector :: HashMap actorID Count -> VersionVector actorID +mkVersionVector m = + VersionVector + m + ( sortDesc fst $ + map (\(a, c) -> (c, a)) (Map.toList m) + ) + where + sortDesc keyFn = sortBy (\x y -> compare (keyFn y) (keyFn x)) + +{- | A Dotted Version Vector (DVV) consisting of a Causal History (Version Vector) +and a set of concurrent values associated with Dots. + +Note: A Singleton has no causal history, its counter is implicitly 1. + +@actorID@ is the type of actor IDs. Must be Hashable. +@value@ is the type of the value stored. +-} data DVV actorID value = EmptyDVV | SingletonDVV !actorID !value | DVV !(VersionVector actorID) !(HashMap (Dot actorID) value) - deriving stock (Eq, Show, Ord, Functor, Foldable, Traversable, Generic) + deriving stock (Eq, Show, Generic) +isSeenBy :: + (Ord actorID, Hashable actorID) => + Dot actorID -> + DVV actorID value -> + Bool +isSeenBy (Dot i n) dvv = + case dvv of + EmptyDVV -> False + SingletonDVV a _ -> + -- A dot is seen by a singleton if it's the same dot (or 0) + Dot i n == Dot a 1 + DVV vv dots -> + -- 1. Check if the counter is within the compacted summary + n <= Map.findWithDefault 0 i (vvMap vv) + || + -- 2. OR check if this specific dot is in the active set + Map.member (Dot i n) dots + +-- | DVV partial order is defined by the partial order of their causal histories. +instance (Hashable actorID, Eq value, Ord actorID) => PartialOrd (DVV actorID value) where + leq EmptyDVV _ = True + leq _ EmptyDVV = False + leq (SingletonDVV i1 _) d2 = Dot i1 1 `isSeenBy` d2 -- counters start at 1 + leq (DVV vv1 dots1) d2 = + let vv2 = case d2 of + DVV v _ -> v + _ -> mkVersionVector Map.empty -- EmptyDVV and SingletonDVV have no causal history + in leq vv1 vv2 && all (`isSeenBy` d2) (Map.keys dots1) + +instance (Hashable actorID, Ord value, Ord actorID) => Ord (DVV actorID value) where + compare a b + | a == b = EQ + | leq a b = LT + | leq b a = GT + | otherwise = + let (vv1, _) = extractComponents a + (vv2, _) = extractComponents b + in if not (leq vv1 vv2) + then LT + else GT + -- | Extract all values currently in the DVV. values :: DVV actorID value -> [value] values EmptyDVV = [] @@ -82,20 +159,21 @@ (Hashable actorID) => DVV actorID value -> VersionVector actorID -context EmptyDVV = Map.empty -context (SingletonDVV actor _) = Map.singleton actor 1 +context EmptyDVV = mkVersionVector Map.empty +context (SingletonDVV actor _) = mkVersionVector (Map.singleton actor 1) context (DVV causalHistory vals) = - foldl' updateVec causalHistory (Map.keys vals) - where - updateVec m (Dot actor counter) = Map.insertWith max actor counter m + let finalMap = foldl' updateVec (vvMap causalHistory) (Map.keys vals) + in mkVersionVector finalMap + where + updateVec m (Dot actor counter) = Map.insertWith max actor counter m -- | Safely extracts the components of any DVV state into a standard history map and values map. extractComponents :: (Hashable actorID) => DVV actorID value -> (VersionVector actorID, HashMap (Dot actorID) value) -extractComponents EmptyDVV = (Map.empty, Map.empty) -extractComponents (SingletonDVV actor val) = (Map.empty, Map.singleton (Dot actor 1) val) +extractComponents EmptyDVV = (mkVersionVector Map.empty, Map.empty) +extractComponents (SingletonDVV actor val) = (mkVersionVector Map.empty, Map.singleton (Dot actor 1) val) extractComponents (DVV vec vals) = (vec, vals) -- | Synchronize (merge) two DVVs. @@ -120,7 +198,7 @@ HashMap (Dot actorID) value -> DVV actorID value merge vL valsL vR valsR = - let newVec = Map.unionWith max vL vR + let newVec = Map.unionWith max (vvMap vL) (vvMap vR) -- Use unionWith to handle duplicate dots consistently (pick min for determinism) candidates = Map.unionWith min valsL valsR isActive (Dot actor counter) _ = @@ -131,7 +209,7 @@ in case Map.toList newVals of [] -> EmptyDVV [(Dot actor 1, val)] | Map.null newVec -> SingletonDVV actor val - _ -> DVV newVec newVals + _ -> DVV (mkVersionVector newVec) newVals -- | Record a new event (update). event :: @@ -146,21 +224,21 @@ value -> DVV actorID value event currentState maybeContext actorID newValue = - let ctx = fromMaybe Map.empty maybeContext + let ctx = fromMaybe (mkVersionVector Map.empty) maybeContext (causalHistory, vals) = extractComponents currentState - currentMax = Map.lookup actorID (context currentState) + currentMax = Map.lookup actorID (vvMap (context currentState)) nextCount = maybe 1 (+ 1) currentMax newDot = Dot actorID nextCount filterOld (Dot i c) _ = - case Map.lookup i ctx of + case Map.lookup i (vvMap ctx) of Nothing -> True Just cnt -> c > cnt filteredVals = Map.filterWithKey filterOld vals - newVec = Map.unionWith max causalHistory ctx + newVec = Map.unionWith max (vvMap causalHistory) (vvMap ctx) finalVals = Map.insert newDot newValue filteredVals - in DVV newVec finalVals + in DVV (mkVersionVector newVec) finalVals -- | Prune the causal history (Version Vector). prune :: @@ -172,8 +250,8 @@ prune _ EmptyDVV = EmptyDVV prune _ s@(SingletonDVV _ _) = s prune threshold (DVV causalHistory vals) = - let newVec = Map.filter (>= threshold) causalHistory - in DVV newVec vals + let newVec = Map.filter (>= threshold) (vvMap causalHistory) + in DVV (mkVersionVector newVec) vals -- | Reconcile multiple siblings into a single value using a merge strategy. reconcile :: @@ -191,17 +269,22 @@ | size dvv <= 1 = dvv | otherwise = let allVals = values dvv + -- Foldl1' is safe because of guard size > 1 implies >= 2 elements (at least 2, actually size 0/1 handled) + -- But size counts elements. Empty=0, Singleton=1, DVV may have 0 in map? + -- DVV constructor usually ensures non-empty map if used correctly, or use EmptyDVV. + -- But let's follow existing logic. mergedVal = foldl1' mergeFn allVals ctx = context dvv in event dvv (Just ctx) actorID mergedVal --- | Last-Write-Wins (LWW) reconciliation. --- --- Reduces multiple concurrent values (siblings) into a single "winning" value based on the provided --- comparison function. This operation creates a new event (dot) for the winning value that --- supersedes all current values in the DVV. --- --- If there are zero or one values, the DVV is returned unchanged. +{- | Last-Write-Wins (LWW) reconciliation. + +Reduces multiple concurrent values (siblings) into a single "winning" value based on the provided +comparison function. This operation creates a new event (dot) for the winning value that +supersedes all current values in the DVV. + +If there are zero or one values, the DVV is returned unchanged. +-} lww :: (Hashable actorID) => -- | A function to compare two values. 'GT' indicates the first value wins. @@ -212,10 +295,10 @@ DVV actorID value -> DVV actorID value lww compareFn = reconcile pickBest - where - pickBest v1 v2 = case compareFn v1 v2 of - GT -> v1 - _ -> v2 + where + pickBest v1 v2 = case compareFn v1 v2 of + GT -> v1 + _ -> v2 -- | Return the number of elements (siblings) in the DVV. size :: DVV actorID value -> Int diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -2,8 +2,9 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} +import Algebra.PartialOrd (PartialOrd (..)) import Control.Monad (foldM) import Data.DVV import qualified Data.HashMap.Strict as Map @@ -23,13 +24,13 @@ let d = EmptyDVV :: DVV ID Value size d `shouldBe` 0 values d `shouldBe` [] - context d `shouldBe` Map.empty + context d `shouldBe` mkVersionVector Map.empty it "should yield the correct size, values, and context for a singleton DVV" $ do let d = SingletonDVV "A" "v1" :: DVV ID Value size d `shouldBe` 1 values d `shouldBe` ["v1"] - context d `shouldBe` Map.fromList [("A", 1)] + context d `shouldBe` mkVersionVector (Map.fromList [("A", 1)]) it "should handle events correctly (update)" $ do -- A starts with v1 @@ -37,19 +38,19 @@ -- A updates with v2, knowing about d0 let ctx0 = context d0 - d1 = event d0 (Just ctx0) "A" "v2" + let d1 = event d0 (Just ctx0) "A" "v2" size d1 `shouldBe` 1 values d1 `shouldBe` ["v2"] - context d1 `shouldBe` Map.fromList [("A", 2)] + context d1 `shouldBe` mkVersionVector (Map.fromList [("A", 2)]) -- A updates again with v3 let ctx1 = context d1 - d2 = event d1 (Just ctx1) "A" "v3" + let d2 = event d1 (Just ctx1) "A" "v3" size d2 `shouldBe` 1 values d2 `shouldBe` ["v3"] - context d2 `shouldBe` Map.fromList [("A", 3)] + context d2 `shouldBe` mkVersionVector (Map.fromList [("A", 3)]) it "should handle concurrent updates (siblings)" $ do -- A starts with v1 @@ -63,7 +64,7 @@ size dSync `shouldBe` 2 values dSync `shouldContain` ["v1"] values dSync `shouldContain` ["v2"] - context dSync `shouldBe` Map.fromList [("A", 1), ("B", 1)] + context dSync `shouldBe` mkVersionVector (Map.fromList [("A", 1), ("B", 1)]) it "should resolve siblings with event superseding" $ do -- Start with synced state having {A:1, v1} and {B:1, v2} @@ -78,7 +79,7 @@ size dFinal `shouldBe` 1 values dFinal `shouldBe` ["v3"] -- Dot should be A:2. Context should be {A: 2, B: 1} - context dFinal `shouldBe` Map.fromList [("A", 2), ("B", 1)] + context dFinal `shouldBe` mkVersionVector (Map.fromList [("A", 2), ("B", 1)]) it "should keep concurrent updates if context is missing information" $ do -- B makes an update v1 @@ -98,7 +99,7 @@ size dFinal `shouldBe` 2 values dFinal `shouldContain` ["v1"] values dFinal `shouldContain` ["v3"] - context dFinal `shouldBe` Map.fromList [("A", 2), ("B", 1)] + context dFinal `shouldBe` mkVersionVector (Map.fromList [("A", 2), ("B", 1)]) it "should handle multiple siblings from different actors" $ do let dA = SingletonDVV "A" "v1" :: DVV ID Value @@ -109,7 +110,8 @@ dABC = sync dAB dC size dABC `shouldBe` 3 - context dABC `shouldBe` Map.fromList [("A", 1), ("B", 1), ("C", 1)] + context dABC + `shouldBe` mkVersionVector (Map.fromList [("A", 1), ("B", 1), ("C", 1)]) it "should prune old history" $ do -- Create a DVV with history {A: 10, B: 5} @@ -120,7 +122,7 @@ dSync = sync d10 dB5 - context dSync `shouldBe` Map.fromList [("A", 10), ("B", 5)] + context dSync `shouldBe` mkVersionVector (Map.fromList [("A", 10), ("B", 5)]) -- To test prune properly, we need history that IS NOT supported by a value. -- Make A supersede B:5 first (so B:5 is removed from values), but B:5 remains in history. @@ -128,12 +130,12 @@ -- Now A:11. B:5 is superseded (removed from values). -- Values: {A:11}. Vector: {A:11, B:5} (merged context). - context dVoidB `shouldBe` Map.fromList [("A", 11), ("B", 5)] + context dVoidB `shouldBe` mkVersionVector (Map.fromList [("A", 11), ("B", 5)]) let dPruned = prune 8 dVoidB -- Now B:5 < 8, so it should be removed from vector. -- A:11 >= 8, keeps A:11. - context dPruned `shouldBe` Map.fromList [("A", 11)] + context dPruned `shouldBe` mkVersionVector (Map.fromList [("A", 11)]) it "should reconcile siblings into a single value with new dot" $ do let dA = SingletonDVV "A" "v1" :: DVV ID Value @@ -150,7 +152,8 @@ val `shouldSatisfy` (\v -> v == "v1v2" || v == "v2v1") -- Context should now include C:1 - context dReconciled `shouldBe` Map.fromList [("A", 1), ("B", 1), ("C", 1)] + context dReconciled + `shouldBe` mkVersionVector (Map.fromList [("A", 1), ("B", 1), ("C", 1)]) it "should use Last-Write-Wins (lww) to pick a winner" $ do let dA = SingletonDVV "A" "apple" :: DVV ID Value @@ -166,7 +169,7 @@ -- Reconcile advances the dot for the actor performing the reconcile (A). -- Previous A was 1. New dot is A:2. -- B remains at 1 (as history). - context dLWW `shouldBe` Map.fromList [("A", 2), ("B", 1)] + context dLWW `shouldBe` mkVersionVector (Map.fromList [("A", 2), ("B", 1)]) describe "DVV QuickCheck Properties" $ do it "sync is idempotent: sync d d == d (semantically)" $ @@ -190,15 +193,17 @@ property $ \(d1 :: DVV ID Value) (d2 :: DVV ID Value) -> let ctx1 = context d1 ctxSync = context (sync d1 d2) - in all (\(k, v) -> Map.lookup k ctxSync >= Just v) (Map.toList ctx1) + in all + (\(k, v) -> Map.lookup k (vvMap ctxSync) >= Just v) + (Map.toList (vvMap ctx1)) it "event increases context counter for the actor" $ property $ \(d :: DVV ID Value) (actor :: ID) (val :: Value) -> let ctx = context d d' = event d (Just ctx) actor val ctx' = context d' - oldCount = Map.findWithDefault 0 actor ctx - newCount = Map.findWithDefault 0 actor ctx' + oldCount = Map.findWithDefault 0 actor (vvMap ctx) + newCount = Map.findWithDefault 0 actor (vvMap ctx') in newCount `shouldBe` (oldCount + 1) it "event with full context produces exactly one value" $ @@ -231,11 +236,134 @@ property $ \(d :: DVV ID Value) -> case d of EmptyDVV -> True - SingletonDVV actor _ -> Map.member actor (context d) + SingletonDVV actor _ -> Map.member actor (vvMap (context d)) DVV _ vals -> - let ctx = context d + let ctx = vvMap (context d) actors = [actor | Dot actor _ <- Map.keys vals] in all (`Map.member` ctx) actors + + describe "PartialOrd and Ord Properties" $ do + it "Dot PartialOrd is only defined for same actor" $ do + let d1 = Dot "A" 10 :: Dot ID + d2 = Dot "B" 10 :: Dot ID + d3 = Dot "A" 11 :: Dot ID + comparable d1 d2 `shouldBe` False + leq d1 d3 `shouldBe` True + leq d3 d1 `shouldBe` False + + it "DVV PartialOrd follows causality (happensBefore)" $ do + let d1 = SingletonDVV "A" "v1" :: DVV ID Value + d2 = event d1 (Just $ context d1) "A" "v2" + d3 = SingletonDVV "B" "v3" :: DVV ID Value + leq d1 d2 `shouldBe` True + leq d2 d1 `shouldBe` False + comparable d1 d3 `shouldBe` False -- incomparable + it "DVV Ord is consistent with PartialOrd" $ + property $ \(d1 :: DVV ID Value) (d2 :: DVV ID Value) -> + if leq d1 d2 + then if d1 == d2 then compare d1 d2 == EQ else compare d1 d2 == LT + else + if leq d2 d1 + then compare d1 d2 == GT + else compare d1 d2 /= EQ + + it "Replicates Erlang less_test scenarios" $ do + -- A = update(new_list(v1),[a]), + let a = SingletonDVV "a" "v1" :: DVV ID Value + let ctxA = context a + + -- B = update(new_list(join(A),[v2]), a), + -- Effectively: event on A (to get context) with "a" -> "v2" + let b = event a (Just ctxA) "a" "v2" + + -- B2 = update(new_list(join(A),[v2]), b), + -- Event on A, actor "b" + let b2 = event a (Just ctxA) "b" "v2" + + -- B3 = update(new_list(join(A),[v2]), z), + -- Event on A, actor "z" + let b3 = event a (Just ctxA) "z" "v2" + + -- C = update(new_list(join(B),[v3]), A, c), + let ctxB = context b + let c = event b (Just ctxB) "c" "v3" + + -- D = update(new_list(join(C),[v4]), B2, d), + -- Base is C's context. Update with actor "d". Context B2. + -- C has {a:2, c:1}. B2 has {a:1, b:1}. + -- C does not know b:1. + -- B2 knows b:1. + -- New DVV will merge contexts: {a:2, b:1, c:1}. + -- Value v4 (d:1). + -- Supersedes values in C and B2? + -- C vals: {a:2, c:1} (if dots kept). v3. + -- B2 vals: {b:1} v2. + -- New val: v4 (d:1). + -- Contexts merged. + -- Check if v3 (c:1) is superseded by {a:2, b:1, c:1} + d:1? + -- c:1 is in context. Yes. + -- v2 (b:1) is in context. Yes. + -- So D should have only v4. + + -- We construct D by simulating this "update from C base with B2 context": + -- We assume we start with C (as it provides the base history 'join(C)'). + -- But we add B2's context. + let ctxB2 = context b2 + let d = event c (Just ctxB2) "d" "v4" + -- event merges ctxB2 into C's history. + -- currentMax for "d" in C is 0. Next 1. + -- Result DVV history: union(C, B2) = {a:2, b:1, c:1, d:1}. + -- Values: v4. + + -- Assertions + -- less(A, B) -> A <= B and A != B. + leq a b `shouldBe` True + a /= b `shouldBe` True + + -- less(A, C) + leq a c `shouldBe` True + a /= c `shouldBe` True + + -- less(B, C) + leq b c `shouldBe` True + b /= c `shouldBe` True + + -- less(B, D) + leq b d `shouldBe` True + b /= d `shouldBe` True + + -- less(B2, D) + leq b2 d `shouldBe` True + b2 /= d `shouldBe` True + + -- less(A, D) + leq a d `shouldBe` True + a /= d `shouldBe` True + + -- not less(B2, C) -> B2 not <= C + leq b2 c `shouldBe` False + + -- not less(B, B2) + leq b b2 `shouldBe` False + + -- not less(B2, B) + leq b2 b `shouldBe` False + + -- not less(A, A) (strict) -> leq is True, but Eq. + -- Erlang less is strict. + leq a a `shouldBe` True + + -- not less(C, C) + leq c c `shouldBe` True + + -- not less(D, B2) + leq d b2 `shouldBe` False + + -- not less(B3, D) + -- B3 {a:1, z:1}. D {a:2, b:1, c:1, d:1}. + -- D does NOT know z:1. + -- So B3 not <= D. + leq b3 d `shouldBe` False -- QuickCheck Arbitrary instances