From 109aeb93db7531f5d4aa6f9ff49d2dcca1de582f Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:12:37 +0100
Subject: [PATCH 1/7] Add n-way unions to the public API

---
 src/Database/LSMTree.hs          | 11 +++++++++++
 src/Database/LSMTree/Monoidal.hs | 19 +++++++++++++++++++
 src/Database/LSMTree/Normal.hs   | 16 ++++++++++++++++
 3 files changed, 46 insertions(+)

diff --git a/src/Database/LSMTree.hs b/src/Database/LSMTree.hs
index 56a2ba854..e2c916bba 100644
--- a/src/Database/LSMTree.hs
+++ b/src/Database/LSMTree.hs
@@ -80,6 +80,7 @@ module Database.LSMTree (
 
     -- * Table union
   , union
+  , unions
 
     -- * Serialisation
   , SerialiseKey
@@ -530,6 +531,16 @@ union :: forall m k v b.
   -> m (Table m k v b)
 union = error "union: not yet implemented" $ union @m @k @v @b
 
+{-# SPECIALISE unions ::
+     ResolveValue v
+  => V.Vector (Table IO k v b)
+  -> IO (Table IO k v b) #-}
+unions :: forall m k v b.
+     (IOLike m, ResolveValue v)
+  => V.Vector (Table m k v b)
+  -> m (Table m k v b)
+unions = error "unions: not yet implemented" $ unions @m @k @v
+
 {-------------------------------------------------------------------------------
   Monoidal value resolution
 -------------------------------------------------------------------------------}
diff --git a/src/Database/LSMTree/Monoidal.hs b/src/Database/LSMTree/Monoidal.hs
index 233ffec07..e846b5794 100644
--- a/src/Database/LSMTree/Monoidal.hs
+++ b/src/Database/LSMTree/Monoidal.hs
@@ -97,6 +97,7 @@ module Database.LSMTree.Monoidal (
 
     -- * Table union
   , union
+  , unions
 
     -- * Concurrency
     -- $concurrency
@@ -672,6 +673,24 @@ union :: forall m k v.
   -> m (Table m k v)
 union = error "union: not yet implemented" $ union @m @k @v
 
+{-# SPECIALISE unions ::
+     ResolveValue v
+  => V.Vector (Table IO k v)
+  -> IO (Table IO k v) #-}
+-- | Like 'union', but for @n@ tables.
+--
+-- A good mental model of this operation is @'Data.Map.Lazy.unionsWith' (<>)@ on
+-- @'Data.Map.Lazy.Map' k v@.
+--
+-- Exceptions:
+--
+-- * Unioning 0 tables is an exception.
+unions :: forall m k v.
+     (IOLike m, ResolveValue v)
+  => V.Vector (Table m k v)
+  -> m (Table m k v)
+unions = error "unions: not yet implemented" $ unions @m @k @v
+
 {-------------------------------------------------------------------------------
   Monoidal value resolution
 -------------------------------------------------------------------------------}
diff --git a/src/Database/LSMTree/Normal.hs b/src/Database/LSMTree/Normal.hs
index 1d801d494..5adda9b5a 100644
--- a/src/Database/LSMTree/Normal.hs
+++ b/src/Database/LSMTree/Normal.hs
@@ -98,6 +98,7 @@ module Database.LSMTree.Normal (
 
     -- * Table union
   , union
+  , unions
 
     -- * Concurrency #concurrency#
     -- $concurrency
@@ -787,3 +788,18 @@ union :: forall m k v b.
   -> Table m k v b
   -> m (Table m k v b)
 union = error "union: not yet implemented" $ union @m @k @v
+
+{-# SPECIALISE unions :: V.Vector (Table IO k v b) -> IO (Table IO k v b) #-}
+-- | Like 'union', but for @n@ tables.
+--
+-- A good mental model of this operation is @'Data.Map.Lazy.unions'@ on
+-- @'Data.Map.Lazy.Map' k v@.
+--
+-- Exceptions:
+--
+-- * Unioning 0 tables is an exception.
+unions :: forall m k v b.
+     IOLike m
+  => V.Vector (Table m k v b)
+  -> m (Table m k v b)
+unions = error "union: not yet implemented" $ union @m @k @v

From ff7b1d2187970a9b0ac83eae0bfa9edd620ffda0 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:12:55 +0100
Subject: [PATCH 2/7] Implement n-way unions in the model

---
 test/Database/LSMTree/Model/Session.hs | 21 +++++++++++++++++++++
 test/Database/LSMTree/Model/Table.hs   | 23 +++++++++++------------
 2 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/test/Database/LSMTree/Model/Session.hs b/test/Database/LSMTree/Model/Session.hs
index 800d96a79..ed9df828c 100644
--- a/test/Database/LSMTree/Model/Session.hs
+++ b/test/Database/LSMTree/Model/Session.hs
@@ -73,6 +73,7 @@ module Database.LSMTree.Model.Session (
   , duplicate
     -- * Table union
   , union
+  , unions
   ) where
 
 import           Control.Monad (when)
@@ -204,6 +205,8 @@ data Err =
   | ErrSnapshotWrongType
   | ErrBlobRefInvalidated
   | ErrCursorClosed
+    -- | Passed zero tables to 'unions'
+  | ErrUnionsZeroTables
   deriving stock (Show, Eq)
 
 {-------------------------------------------------------------------------------
@@ -628,3 +631,21 @@ union r th1 th2 = do
   (_, t1) <- guardTableIsOpen th1
   (_, t2) <- guardTableIsOpen th2
   newTableWith TableConfig $ Model.union r t1 t2
+
+unions ::
+     ( MonadState Model m
+     , MonadError Err m
+     , C k v b
+     )
+  => ResolveSerialisedValue v
+  -> V.Vector (Table k v b)
+  -> m (Table k v b)
+unions r tables
+  | n == 0 = throwError ErrUnionsZeroTables
+  | otherwise = do
+      tables' <- V.forM tables $ \table -> do
+        (_, table') <- guardTableIsOpen table
+        pure table'
+      newTableWith TableConfig $ Model.unions r tables'
+  where
+    n = V.length tables
diff --git a/test/Database/LSMTree/Model/Table.hs b/test/Database/LSMTree/Model/Table.hs
index 516d265a8..74d9d11ca 100644
--- a/test/Database/LSMTree/Model/Table.hs
+++ b/test/Database/LSMTree/Model/Table.hs
@@ -38,6 +38,7 @@ module Database.LSMTree.Model.Table (
   , duplicate
     -- * Table union
   , union
+  , unions
     -- * Testing
   , size
   ) where
@@ -301,24 +302,22 @@ readCursor n c =
     )
 
 {-------------------------------------------------------------------------------
-  Merging tables
+  Table union
 -------------------------------------------------------------------------------}
 
--- | Merge full tables, creating a new table.
---
--- NOTE: close tables using 'close' as soon as they are
--- unused.
---
--- Multiple tables of the same type but with different configuration parameters
--- can live in the same session. However, some operations, like
+-- | Union two full tables, creating a new table.
 union ::
      ResolveSerialisedValue v
   -> Table k v b
   -> Table k v b
   -> Table k v b
 union r (Table xs) (Table ys) =
-    Table (Map.unionWith f xs ys)
-  where
-    f (v1, bMay1) (v2, bMay2) =
-      (resolveSerialised r v1 v2, getFirst (First bMay1 <> First bMay2))
+    Table (Map.unionWith (resolveValueAndBlob r) xs ys)
 
+-- | Like 'union', but for @n@ tables.
+unions ::
+     ResolveSerialisedValue v
+  -> V.Vector (Table k v b)
+  -> Table k v b
+unions r tables =
+    Table (Map.unionsWith (resolveValueAndBlob r) (V.map values tables))

From 4d2e8ecf30ff2a685a98c67bc366e1130e69b854 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:13:19 +0100
Subject: [PATCH 3/7] Remove underscores from some identifiers

Originally, I had put underscores in the field names so that they wouldn't show
up in "unused identifier" compiler errors. But, since they're exported now
anyway, we can get rid of the underscores
---
 test/Database/LSMTree/Model/IO.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/test/Database/LSMTree/Model/IO.hs b/test/Database/LSMTree/Model/IO.hs
index 946069830..8553ca531 100644
--- a/test/Database/LSMTree/Model/IO.hs
+++ b/test/Database/LSMTree/Model/IO.hs
@@ -24,18 +24,18 @@ import qualified Database.LSMTree.Model.Session as Model
 newtype Session m = Session (StrictTVar m (Maybe Model.Model))
 
 data Table m k v b = Table {
-    _thSession :: !(Session m)
-  , _thTable   :: !(Model.Table k v b)
+    thSession :: !(Session m)
+  , thTable   :: !(Model.Table k v b)
   }
 
 data BlobRef m b = BlobRef {
-    _brSession :: !(Session m)
-  , _brBlobRef :: !(Model.BlobRef b)
+    brSession :: !(Session m)
+  , brBlobRef :: !(Model.BlobRef b)
   }
 
 data Cursor m k v b = Cursor {
-    _cSession :: !(Session m)
-  , _cCursor  :: !(Model.Cursor k v b)
+    cSession :: !(Session m)
+  , cCursor  :: !(Model.Cursor k v b)
   }
 
 newtype Err = Err (Model.Err)
@@ -76,7 +76,7 @@ instance Class.IsTable Table where
 
     rangeLookup (Table s t) x1 = fmap (fmap (BlobRef s)) <$>
       runInOpenSession s (Model.rangeLookup x1 t)
-    retrieveBlobs _ s x1 = runInOpenSession s (Model.retrieveBlobs (fmap _brBlobRef x1))
+    retrieveBlobs _ s x1 = runInOpenSession s (Model.retrieveBlobs (fmap brBlobRef x1))
 
     newCursor k (Table s t) = Cursor s <$> runInOpenSession s (Model.newCursor k t)
     closeCursor _ (Cursor s c) = runInOpenSession s (Model.closeCursor c)

From b3f669d3d74df9e0f0bdb21fa2e485bb73808fa0 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:14:27 +0100
Subject: [PATCH 4/7] Add n-way unions to the public API class

---
 test/Database/LSMTree/Class.hs    | 16 ++++++++++++++++
 test/Database/LSMTree/Model/IO.hs |  6 ++++++
 2 files changed, 22 insertions(+)

diff --git a/test/Database/LSMTree/Class.hs b/test/Database/LSMTree/Class.hs
index 8c6ce5cb0..e0b44ee63 100644
--- a/test/Database/LSMTree/Class.hs
+++ b/test/Database/LSMTree/Class.hs
@@ -8,6 +8,7 @@ module Database.LSMTree.Class (
   , withTableFromSnapshot
   , withTableDuplicate
   , withTableUnion
+  , withTableUnions
   , withCursor
   , module Common
   , module Types
@@ -162,6 +163,13 @@ class (IsSession (Session h)) => IsTable h where
         -> h m k v b
         -> m (h m k v b)
 
+    unions ::
+           ( IOLike m
+           , C k v b
+           )
+        => V.Vector (h m k v b)
+        -> m (h m k v b)
+
 withTableNew :: forall h m k v b a.
     (IOLike m, IsTable h, C k v b)
   => Session h m
@@ -194,6 +202,13 @@ withTableUnion :: forall h m k v b a.
   -> m a
 withTableUnion table1 table2 = bracket (table1 `union` table2) close
 
+withTableUnions :: forall h m k v b a.
+     (IOLike m, IsTable h, C k v b)
+  => V.Vector (h m k v b)
+  -> (h m k v b -> m a)
+  -> m a
+withTableUnions tables = bracket (unions tables) close
+
 withCursor :: forall h m k v b a.
      (IOLike m, IsTable h, C k v b)
   => Maybe k
@@ -232,3 +247,4 @@ instance IsTable R.Table where
 
     duplicate = R.duplicate
     union = R.union
+    unions = R.unions
diff --git a/test/Database/LSMTree/Model/IO.hs b/test/Database/LSMTree/Model/IO.hs
index 8553ca531..a207f26a0 100644
--- a/test/Database/LSMTree/Model/IO.hs
+++ b/test/Database/LSMTree/Model/IO.hs
@@ -17,6 +17,7 @@ module Database.LSMTree.Model.IO (
 import           Control.Concurrent.Class.MonadSTM.Strict
 import           Control.Exception (Exception)
 import           Control.Monad.Class.MonadThrow (MonadThrow (..))
+import qualified Data.Vector as V
 import qualified Database.LSMTree.Class as Class
 import           Database.LSMTree.Model.Session (TableConfig (..))
 import qualified Database.LSMTree.Model.Session as Model
@@ -90,3 +91,8 @@ instance Class.IsTable Table where
 
     union (Table s1 t1) (Table _s2 t2) =
       Table s1 <$> runInOpenSession s1 (Model.union Model.getResolve t1 t2)
+
+    unions ts =
+        Table s <$> runInOpenSession s (Model.unions Model.getResolve (V.map thTable ts))
+      where
+        Table s _ = V.head ts

From 3280e49ea070e669754f6c0ef05e09bbec2460a3 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:21:01 +0100
Subject: [PATCH 5/7] Add n-way unions to the state machine tests

---
 test/Test/Database/LSMTree/StateMachine.hs | 42 +++++++++++++++++++++-
 1 file changed, 41 insertions(+), 1 deletion(-)

diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs
index 6922ac039..ab8c38136 100644
--- a/test/Test/Database/LSMTree/StateMachine.hs
+++ b/test/Test/Database/LSMTree/StateMachine.hs
@@ -490,6 +490,9 @@ instance ( Show (Class.TableConfig h)
           => Var h (WrapTable h IO k v b)
           -> Var h (WrapTable h IO k v b)
           -> Act h (WrapTable h IO k v b)
+    Unions :: C k v b
+           => V.Vector (Var h (WrapTable h IO k v b))
+           -> Act h (WrapTable h IO k v b)
 
   initialState    = Lockstep.Defaults.initialState initModelState
   nextState       = Lockstep.Defaults.nextState
@@ -552,6 +555,8 @@ instance ( Eq (Class.TableConfig h)
           Just var1 == cast var2
       go (Union var1_1 var1_2) (Union var2_1 var2_2) =
           Just var1_1 == cast var2_1 && Just var1_2 == cast var2_2
+      go (Unions vars1) (Unions vars2) =
+          Just vars1 == cast vars2
       go _  _ = False
 
       _coveredAllCases :: LockstepAction (ModelState h) a -> ()
@@ -574,6 +579,7 @@ instance ( Eq (Class.TableConfig h)
           ListSnapshots{} -> ()
           Duplicate{} -> ()
           Union{} -> ()
+          Unions{} -> ()
 
 {-------------------------------------------------------------------------------
   InLockstep
@@ -681,6 +687,7 @@ instance ( Eq (Class.TableConfig h)
       ListSnapshots                   -> []
       Duplicate tableVar              -> [SomeGVar tableVar]
       Union table1Var table2Var       -> [SomeGVar table1Var, SomeGVar table2Var]
+      Unions tableVars                -> [SomeGVar tableVar | tableVar <- V.toList tableVars]
 
   arbitraryWithVars ::
        ModelVarContext (ModelState h)
@@ -794,6 +801,7 @@ instance ( Eq (Class.TableConfig h)
       ListSnapshots{}  -> OEither $ bimap OId (OList . fmap OId) result
       Duplicate{}      -> OEither $ bimap OId (const OTable) result
       Union{}          -> OEither $ bimap OId (const OTable) result
+      Unions{}         -> OEither $ bimap OId (const OTable) result
 
   showRealResponse ::
        Proxy (RealMonad h IO)
@@ -818,6 +826,7 @@ instance ( Eq (Class.TableConfig h)
       ListSnapshots    -> Just Dict
       Duplicate{}      -> Nothing
       Union{}          -> Nothing
+      Unions{}         -> Nothing
 
 instance ( Eq (Class.TableConfig h)
          , Class.IsTable h
@@ -852,6 +861,7 @@ instance ( Eq (Class.TableConfig h)
       ListSnapshots{}  -> OEither $ bimap OId (OList . fmap OId) result
       Duplicate{}      -> OEither $ bimap OId (const OTable) result
       Union{}          -> OEither $ bimap OId (const OTable) result
+      Unions{}         -> OEither $ bimap OId (const OTable) result
 
   showRealResponse ::
        Proxy (RealMonad h (IOSim s))
@@ -876,6 +886,7 @@ instance ( Eq (Class.TableConfig h)
       ListSnapshots    -> Just Dict
       Duplicate{}      -> Nothing
       Union{}          -> Nothing
+      Unions{}         -> Nothing
 
 {-------------------------------------------------------------------------------
   RunModel
@@ -965,6 +976,9 @@ runModel lookUp = \case
     Union table1Var table2Var ->
       wrap MTable
       . Model.runModelM (Model.union Model.getResolve (getTable $ lookUp table1Var) (getTable $ lookUp table2Var))
+    Unions tableVars ->
+      wrap MTable
+      . Model.runModelM (Model.unions Model.getResolve (V.map (getTable . lookUp) tableVars))
   where
     getTable ::
          ModelValue (ModelState h) (WrapTable h IO k v b)
@@ -1043,6 +1057,8 @@ runIO action lookUp = ReaderT $ \(session, handler) -> do
           WrapTable <$> Class.duplicate (unwrapTable $ lookUp' tableVar)
         Union table1Var table2Var -> catchErr handler $
           WrapTable <$> Class.union (unwrapTable $ lookUp' table1Var) (unwrapTable $ lookUp' table2Var)
+        Unions tableVars -> catchErr handler $
+          WrapTable <$> Class.unions (V.map (unwrapTable . lookUp') tableVars)
 
     lookUp' :: Var h x -> Realized IO x
     lookUp' = lookUpGVar (Proxy @(RealMonad h IO)) lookUp
@@ -1097,6 +1113,8 @@ runIOSim action lookUp = ReaderT $ \(session, handler) ->
           WrapTable <$> Class.duplicate (unwrapTable $ lookUp' tableVar)
         Union table1Var table2Var -> catchErr handler $
           WrapTable <$> Class.union (unwrapTable $ lookUp' table1Var) (unwrapTable $ lookUp' table2Var)
+        Unions tableVars -> catchErr handler $
+          WrapTable <$> Class.unions (V.map (unwrapTable . lookUp') tableVars)
 
     lookUp' :: Var h x -> Realized (IOSim s) x
     lookUp' = lookUpGVar (Proxy @(RealMonad h (IOSim s))) lookUp
@@ -1155,6 +1173,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         OpenSnapshot{} -> ()
         Duplicate{} -> ()
         Union{} -> ()
+        Unions{} -> ()
 
     genTableVar = QC.elements tableVars
 
@@ -1244,6 +1263,10 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         | length tableVars <= 5 -- no more than 5 tables at once
         , False -- TODO: enable once table union is implemented
         ]
+     ++ [ (2,  fmap Some $ Unions <$> genUnionsTableVars)
+        | length tableVars <= 5 -- no more than 5 tables at once
+        , False -- TODO: enable once table unions is implemented
+        ]
 
     genActionsCursor :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
     genActionsCursor
@@ -1296,6 +1319,20 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
     genBlob :: Gen (Maybe b)
     genBlob = QC.arbitrary
 
+    -- Generate at least a 2-way union, and at most a 3-way union.
+    --
+    -- Unit tests for 0-way and 1-way unions are included in the UnitTests
+    -- module. n-way unions for n>3 lead to larger unions, which are less likely
+    -- to be finished before the end of an action sequence.
+    genUnionsTableVars :: Gen (V.Vector (Var h (WrapTable h IO k v b)))
+    genUnionsTableVars = do
+        tableVar1 <- genTableVar
+        tableVar2 <- genTableVar
+        mtableVar3 <- QC.liftArbitrary genTableVar
+        pure $ V.fromList $ catMaybes [
+            Just tableVar1, Just tableVar2, mtableVar3
+          ]
+
 shrinkActionWithVars ::
      forall h a. (
        Eq (Class.TableConfig h)
@@ -1510,6 +1547,9 @@ updateStats action lookUp modelBefore _modelAfter result =
         Union{}
           | MEither (Right (MTable table)) <- result -> initCount table
           | otherwise                                      -> stats
+        Unions{}
+          | MEither (Right (MTable table)) <- result -> initCount table
+          | otherwise                                      -> stats
 
         -- Note that for the other actions we don't count success vs failure.
         -- We don't need that level of detail. We just want to see the
@@ -1532,7 +1572,7 @@ updateStats action lookUp modelBefore _modelAfter result =
         CloseCursor{}         -> stats
         ReadCursor{}          -> stats
         RetrieveBlobs{}       -> stats
-        CreateSnapshot{}            -> stats
+        CreateSnapshot{}      -> stats
         DeleteSnapshot{}      -> stats
         ListSnapshots{}       -> stats
       where

From 4b53deaa7d0a63b0d50fb4ab17eb26abe1f84c0b Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Fri, 6 Dec 2024 15:21:39 +0100
Subject: [PATCH 6/7] Add a TODO to the statemachine tests related to parent
 tables and unions

---
 test/Test/Database/LSMTree/StateMachine.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs
index ab8c38136..eff10bce0 100644
--- a/test/Test/Database/LSMTree/StateMachine.hs
+++ b/test/Test/Database/LSMTree/StateMachine.hs
@@ -1630,6 +1630,10 @@ updateStats action lookUp modelBefore _modelAfter result =
                                          uptblId
                                          (parentTable stats)
               }
+        -- TODO: also include tables resulting from Union and Unions here. This
+        -- means that tables should be able to have *multiple* ultimate parent
+        -- tables, which is currently not possible: parentTable only stores a
+        -- single ultimate parent table per table.
         _ -> stats
 
     updDupTableActionLog stats | MEither (Right _) <- result =

From ad5d621b89cb0c82c01de1899dd241e3f76a1bf3 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Tue, 10 Dec 2024 16:47:48 +0100
Subject: [PATCH 7/7] Add unit tests for 0-way and 1-way unions

---
 test/Test/Database/LSMTree/UnitTests.hs | 61 ++++++++++++++++++++++---
 1 file changed, 55 insertions(+), 6 deletions(-)

diff --git a/test/Test/Database/LSMTree/UnitTests.hs b/test/Test/Database/LSMTree/UnitTests.hs
index bcb20cb2e..ee3ff6aea 100644
--- a/test/Test/Database/LSMTree/UnitTests.hs
+++ b/test/Test/Database/LSMTree/UnitTests.hs
@@ -5,6 +5,7 @@
 
 module Test.Database.LSMTree.UnitTests (tests) where
 
+import           Control.Monad (void)
 import           Control.Tracer (nullTracer)
 import           Data.ByteString (ByteString)
 import qualified Data.ByteString.Char8 as BS
@@ -15,22 +16,32 @@ import qualified System.FS.API as FS
 
 import           Database.LSMTree as R
 
-import           Control.Exception (Exception, try)
+import           Control.Exception (Exception, bracket, try)
 import           Database.LSMTree.Extras.Generators (KeyForIndexCompact)
 import qualified Test.QuickCheck as QC
 import           Test.Tasty (TestTree, testGroup)
 import           Test.Tasty.HUnit
+import           Test.Tasty.QuickCheck (Property, testProperty)
 import           Test.Util.FS (withTempIOHasBlockIO)
 
 
 tests :: TestTree
 tests =
     testGroup "Test.Database.LSMTree.UnitTests"
-      [ testCaseSteps "unit_blobs"         unit_blobs
-      , testCase      "unit_closed_table"  unit_closed_table
-      , testCase      "unit_closed_cursor" unit_closed_cursor
-      , testCase      "unit_twoTableTypes" unit_twoTableTypes
-      , testCase      "unit_snapshots"     unit_snapshots
+      [ testCaseSteps "unit_blobs"          unit_blobs
+      , testCase      "unit_closed_table"   unit_closed_table
+      , testCase      "unit_closed_cursor"  unit_closed_cursor
+      , testCase      "unit_twoTableTypes"  unit_twoTableTypes
+      , testCase      "unit_snapshots"      unit_snapshots
+
+        -- Properties
+
+      , testProperty "prop_unions_0" $
+          -- TODO: enable once unions are implemented
+          QC.expectFailure prop_unions_0
+      , testProperty "prop_unions_1" $
+          -- TODO: enable once unions are implemented
+          QC.expectFailure prop_unions_1
       ]
 
 unit_blobs :: (String -> IO ()) -> Assertion
@@ -146,6 +157,44 @@ unit_snapshots =
     snap1 = "table1"
     snap2 = "table2"
 
+-- | Unions of 0 tables fail with an exception
+prop_unions_0 :: Property
+prop_unions_0 =
+    QC.once $ QC.ioProperty $
+    assertException err $
+      void $ unions @_ @Key1 @Value1 @Blob1 V.empty
+  where
+    -- TODO: fill in once unions has an implementation
+    err :: LSMTreeError
+    err = error "unit_unions_0: unions has no implementation yet"
+
+-- | Unions of 1 table are equivalent to duplicate
+prop_unions_1 :: Property
+prop_unions_1 =
+    QC.once $ QC.ioProperty $
+    withTempIOHasBlockIO "test" $ \hfs hbio ->
+    withSession nullTracer hfs hbio (FS.mkFsPath []) $ \sess ->
+    withTable @_ @Key1 @Value1 @Blob1 sess defaultTableConfig $ \table -> do
+      inserts table [(Key1 17, Value1 42, Nothing)]
+
+      bracket (unions $ V.singleton table) close $ \table' ->
+        bracket (duplicate table) close $ \table'' -> do
+          inserts table [(Key1 17, Value1 43, Nothing)]
+          inserts table [(Key1 17, Value1 44, Nothing)]
+
+          -- The original table is unmodified
+          r <- lookups table [Key1 17]
+          V.map ignoreBlobRef r @?= [Found (Value1 42)]
+
+          -- The unioned table sees an updated value
+          r' <- lookups table' [Key1 17]
+          V.map ignoreBlobRef r' @?= [Found (Value1 43)]
+
+          -- The duplicated table sees a different updated value
+          r'' <- lookups table'' [Key1 17]
+          V.map ignoreBlobRef r'' @?= [Found (Value1 44)]
+
+
 ignoreBlobRef :: Functor f => f (BlobRef m b) -> f ()
 ignoreBlobRef = fmap (const ())