diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,14 @@
 # Revision history for rec-def
 
+## 0.2 -- 2022-09-22
+
+* The naive propagator does not use `(==)` to detect changes, but a custom
+  operator, to allow faster and less restricted operators.
+* Module structure refactoring
+* No more `R` type constructor, instead individual `RBool` etc. types
+* Addition of `Data.Recursive.Map`
+* A space leak is fixed
+
 ## 0.1 -- 2022-09-03
 
 * First version. Released on an unsuspecting world.
diff --git a/Data/POrder.hs b/Data/POrder.hs
--- a/Data/POrder.hs
+++ b/Data/POrder.hs
@@ -7,24 +7,35 @@
 import Data.Coerce
 import qualified Data.Set as S
 import Numeric.Natural
+import Data.Function
 
--- | This (empty) class indicates that the type @a@ is partially ordered.
--- The class is empty because we do not need any of the operations on runtime.
+-- | This class indicates that the type @a@ is partially ordered by some relation ⊑.
+--
+-- The class does not actually have a method for ⊑, because we do not need it at runtime.
 -- Nevertheless the order better exists for the safety of this API.
 --
 -- This order may be unrelated to the total order given by 'Ord'.
-class Eq a => POrder a
+class POrder a where
+    -- | The `eqOfLe` method checks _related_ elements for equality.
+    --
+    -- Formally: For all @x ⊑ y@, @eqOfLe x y == True@ iff @x == y@.
+    --
+    -- This can be more efficient than testing for equality. For example for
+    -- sets, '(==)' needs to compare the elements, but @eqOfLe@ only needs to
+    -- compare sizes. It is always ok to use '(==)' here.
+    eqOfLe :: a -> a -> Bool
 
--- | A class indicating that the type @a@ is partially ordered and has a bottom
+-- | A class indicating that the type @a@ is has a bottom
 -- element.
-class POrder a => Bottom a where bottom :: a
+class Bottom a where bottom :: a
 
--- | A class indicating that the type @a@ is partially ordered and has a top
+-- | A class indicating that the type @a@ is has a top
 -- element.
 class POrder a => Top a where top :: a
 
 -- | The dual order
-instance POrder a => POrder (Dual a)
+instance POrder a => POrder (Dual a) where
+    eqOfLe (Dual x) (Dual y) = eqOfLe y x
 
 -- | Bottom is the 'top' of @a@
 instance Top a => Bottom (Dual a) where bottom = Dual top
@@ -32,7 +43,7 @@
 -- Annoyingly, we have to give all instances here, to avoid orphans
 
 -- | Arbitrary using the @False < True@ order
-instance POrder Bool
+instance POrder Bool where eqOfLe = (==)
 
 -- | Bottom is 'False'
 instance Bottom Bool where bottom = False
@@ -41,19 +52,23 @@
 instance Top Bool where top = True
 
 -- | Ordered by 'S.subsetOf'
-instance Eq a => POrder (S.Set a)
+instance POrder (S.Set a) where eqOfLe = (==) `on` S.size
 
 -- | Bottom is 'S.empty'
-instance Eq a => Bottom (S.Set a) where bottom = S.empty
+instance Bottom (S.Set a) where bottom = S.empty
 
 -- | Ordered by '(<=)f'
-instance POrder Natural
+instance POrder Natural where eqOfLe = (==)
 
 -- | Bottom is 0
 instance Bottom Natural where bottom = 0
 
 -- | Adds 'Nothing' as a least element to an existing partial order
-instance POrder a => POrder (Maybe a)
+instance POrder a => POrder (Maybe a) where
+    eqOfLe Nothing Nothing = True
+    eqOfLe Nothing (Just _) = False
+    eqOfLe (Just x) (Just y) = eqOfLe x y
+    eqOfLe (Just _) Nothing = error "eqOfLe/Maybe used with unrelated arguments"
 
 -- | Bottom is 'Nothing'
 instance POrder a => Bottom (Maybe a) where bottom = Nothing
diff --git a/Data/Propagator/Class.hs b/Data/Propagator/Class.hs
new file mode 100644
--- /dev/null
+++ b/Data/Propagator/Class.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+
+-- | This module provides the 'Propagator' class
+module Data.Propagator.Class where
+
+import Control.Exception
+
+-- | The Propagator class defines some functions shared by different propagator
+-- implementations. This backs the generic "Data.Propagator.Purify" wrapper.
+class Propagator p x | p -> x where
+    newProp :: IO p
+    newConstProp :: x -> IO p
+    freezeProp :: p -> IO ()
+    readProp :: p -> IO x
+
+data WriteToFrozenPropagatorException = WriteToFrozenPropagatorException
+   deriving Show
+instance Exception WriteToFrozenPropagatorException
diff --git a/Data/Propagator/Naive.hs b/Data/Propagator/Naive.hs
new file mode 100644
--- /dev/null
+++ b/Data/Propagator/Naive.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+-- | A very naive propagator library.
+--
+-- This propagator implementation keeps updating the values accoring to their
+-- definitions as other values change, until a fixed-point is reached.
+--
+-- It is a naive implementation and not very clever. Much more efficient
+-- propagator implementations are possible, and may be used by this library in
+-- the future.
+module Data.Propagator.Naive
+    ( Prop
+    , newProp
+    , newConstProp
+    , freezeProp
+    , readProp
+    , watchProp
+    , setProp
+    , lift1
+    , lift2
+    , liftList
+    )
+    where
+
+import Control.Monad
+import Data.POrder
+import Data.Maybe
+
+import qualified Data.Propagator.Class as Class
+
+-- I want to test this code with dejafu, without carrying it as a dependency
+-- of the main library. So here is a bit of CPP to care for that.
+
+#ifdef DEJAFU
+
+#define Ctxt   MonadConc m =>
+#define Prop_  Prop m
+#define IORef_ IORef m
+#define MVar_  MVar m
+#define M      m
+
+import Control.Concurrent.Classy
+
+#else
+
+#define Ctxt
+#define Prop_  Prop
+#define IORef_ IORef
+#define MVar_  MVar
+#define M      IO
+
+import Control.Exception
+import Control.Concurrent.MVar
+import Data.IORef
+
+#endif
+
+-- | A cell in a propagator network
+data Prop_ a = Prop
+    { val :: IORef_ a
+    , lock :: MVar_ ()
+    , onChange :: IORef_ (Maybe (M ()))
+    }
+
+-- | Creates a cell, initialized to bottom
+newProp :: Ctxt a -> M (Prop_ a)
+newProp x = do
+    m <- newIORef x
+    l <- newMVar ()
+    notify <- newIORef (Just (pure ()))
+    pure $ Prop m l notify
+
+-- | Creates a constant cell, given an initial value
+newConstProp :: Ctxt a -> M (Prop_ a)
+newConstProp x = do
+    m <- newIORef x
+    l <- newMVar ()
+    notify <- newIORef Nothing
+    pure $ Prop m l notify
+
+-- | Reads the current value of the cell
+readProp :: Ctxt Prop_ a -> M a
+readProp (Prop m _ _ ) = readIORef m
+
+-- | Is the current propagator already frozen?
+isFrozen :: Ctxt Prop_ a -> M Bool
+isFrozen (Prop _ _ notify) = do
+    isNothing <$> readIORef notify
+
+-- | Marks the propagator as frozen.
+--
+-- Will prevent further calls to setProp and clears the list of watchers (to
+-- allow GC).
+freezeProp :: Ctxt Prop_ a -> M ()
+freezeProp (Prop _ _ notify) = do
+    writeIORef notify Nothing
+
+-- | Sets a new value calculated from the given action. The action is executed atomically.
+--
+-- Throws if the propagator is already frozen
+--
+-- If the value has changed, all watchers are notified afterwards (not atomically).
+setProp :: Ctxt POrder a => Prop_ a -> M a -> M ()
+setProp p@(Prop m l notify) getX = do
+    frozen <- isFrozen p
+    when frozen $ throw Class.WriteToFrozenPropagatorException
+    () <- takeMVar l
+    old <- readIORef m
+    new <- getX
+    writeIORef m new
+    putMVar l ()
+    unless (old `eqOfLe` new) $
+        readIORef notify >>= \case
+            Nothing -> pure ()
+            Just act -> act
+
+-- | Watch a cell: If the value changes, the given action is executed
+watchProp :: Ctxt Prop_ a -> M () -> M ()
+watchProp (Prop _ _ notify) f =
+    atomicModifyIORef notify $ \case
+        Nothing -> (Nothing, ())
+        Just a -> (Just (f >> a), ())
+
+-- | Whenever the first cell changes, update the second, using the given function
+lift1 :: Ctxt POrder b => (a -> b) -> Prop_ a -> Prop_ b -> M ()
+lift1 f p1 p = do
+    let update = setProp p $ f <$> readProp p1
+    watchProp p1 update
+    update
+
+-- | Whenever any of the first two cells change, update the third, using the given function
+lift2 :: Ctxt POrder c => (a -> b -> c) -> Prop_ a -> Prop_ b -> Prop_ c -> M ()
+lift2 f p1 p2 p = do
+    let update = setProp p $ f <$> readProp p1 <*> readProp p2
+    watchProp p1 update
+    watchProp p2 update
+    update
+
+-- | Whenever any of the cells in the list change, update the other, using the given function
+liftList :: Ctxt POrder b => ([a] -> b) -> [Prop_ a] -> Prop_ b -> M ()
+liftList f ps p = do
+    let update = setProp p $ f <$> mapM readProp ps
+    mapM_ (\p' -> watchProp p' update) ps
+    update
+
+#ifndef DEJAFU
+instance Bottom a => Class.Propagator (Prop_ a) a where
+    newProp = newProp bottom
+    newConstProp = newConstProp
+    freezeProp = freezeProp
+    readProp = readProp
+#endif
diff --git a/Data/Propagator/P2.hs b/Data/Propagator/P2.hs
new file mode 100644
--- /dev/null
+++ b/Data/Propagator/P2.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE CPP #-}
+
+-- | A propagator for the two-point lattice
+--
+module Data.Propagator.P2
+    ( P2
+    , newP2
+    , newTopP2
+    , setTop
+    , whenTop
+    , implies
+    , isTop
+    )
+    where
+
+import Data.Propagator.Class
+
+-- I want to test this code with dejafu, without carrying it as a dependency
+-- of the main library. So here is a bit of CPP to care for that.
+
+#ifdef DEJAFU
+
+#define Ctxt   MonadConc m =>
+#define MaybeTop_  (MaybeTop m)
+#define P2_  (P2 m)
+#define PBool_  PBool m
+#define PDualBool_  PDualBool m
+#define IORef_ IORef m
+#define MVar_  MVar m
+#define M      m
+
+import Control.Concurrent.Classy
+
+#else
+
+#define Ctxt
+#define MaybeTop_  MaybeTop
+#define P2_  P2
+#define PBool_  PBool
+#define PDualBool_  PDualBool
+#define IORef_ IORef
+#define MVar_  MVar
+#define M      IO
+
+import Control.Exception
+import Control.Concurrent.MVar
+import Data.IORef
+
+#endif
+
+data MaybeTop_
+        = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered
+        | SurelyBottom       -- ^ Definitely bottom 
+        | SurelyTop          -- ^ Definitely top
+
+-- | A type for propagators for the two-point lattice, consisting of bottom and top
+newtype P2_ = P2 (MVar_ MaybeTop_)
+
+-- | A new propagator, initialized at bottom
+newP2 :: Ctxt M P2_
+newP2 = P2 <$> newMVar (StillBottom (pure()))
+
+-- | A new propagator, already set to top
+newTopP2 :: Ctxt M P2_
+newTopP2 = P2 <$> newMVar SurelyTop
+
+-- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run
+whenTop :: Ctxt P2_ -> M () -> M ()
+whenTop (P2 p1) act = takeMVar p1 >>= \case
+    SurelyTop        -> putMVar p1 SurelyTop >> act
+    SurelyBottom     -> putMVar p1 SurelyBottom
+    StillBottom act' -> putMVar p1 (StillBottom (act >> act'))
+
+
+-- | Set a propagator to top.
+--
+-- If it was bottom before, runs the actions queued with 'whenTop'. It does so
+-- /after/ setting the propagator to top, so that cycles are broken.
+setTop :: Ctxt P2_ -> M ()
+setTop (P2 p) = takeMVar p >>= \case
+    SurelyTop -> putMVar p SurelyTop
+    SurelyBottom -> throw WriteToFrozenPropagatorException
+    StillBottom act -> do
+        -- Do this first, this breaks cycles
+        putMVar p SurelyTop
+        -- Now notify the dependencies
+        act
+
+-- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.
+implies :: Ctxt P2_ -> P2_ -> M ()
+implies p1 p2 = whenTop p1 (setTop p2)
+
+-- | Queries the current state of the propagator. All related calls to @setTop@
+-- that have executed so far are taken into account.
+isTop :: Ctxt P2_ -> M Bool
+isTop (P2 p) = readMVar p >>= \case
+    SurelyTop -> pure True
+    SurelyBottom -> pure False
+    StillBottom _ -> pure False
+
+-- | Freezes the value. Drops references to watchers.
+freeze :: Ctxt P2_ -> M ()
+freeze (P2 p) = takeMVar p >>= \case
+    SurelyTop -> putMVar p SurelyTop
+    _  -> putMVar p SurelyBottom
+
+#ifndef DEJAFU
+instance Propagator P2_ Bool where
+    newProp = newP2
+    newConstProp False = newP2
+    newConstProp True = newTopP2
+    freezeProp = freeze
+    readProp = isTop
+#endif
diff --git a/Data/Propagator/Purify.hs b/Data/Propagator/Purify.hs
new file mode 100644
--- /dev/null
+++ b/Data/Propagator/Purify.hs
@@ -0,0 +1,110 @@
+{-# OPTIONS_HADDOCK not-home #-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+-- |
+--
+-- This module provides the 'Purify' data type, which wraps a imperative propagator
+-- (for example "Data.Propagator.Naive") in a pure data structure.
+--
+-- It provides functions to declare the inputs to these propagators, which are unsafe on their own, but can be instantiated and wrapped to form safe APIs, e.g. "Data.Recursive.Bool".
+--
+-- This module is labeled as Internal because its safety depends on the behaviour of the
+-- underlying propagator implementation. The assumptions is that
+--
+-- * The defining function passed to `def1` etc. declare a functional relation
+--   between the input propagators and the output propagator.
+-- * Defining functions do not (observably) affect their input propagators.
+-- * Once all the functions passed to `def1` of a propagator and its
+--   dependencies have run, `readProp` will return a correct value, i.e. one
+--   that satisfies the functional relations.
+-- * The order in which the defining functions are executed does not affect the
+--   result.
+-- * Termination depends on the termination of the underlying propagator
+--
+module Data.Propagator.Purify
+    ( Purify
+    , get
+    , mk, def1, def2, defList
+    )
+where
+
+import System.IO.Unsafe
+import Control.Monad.ST
+import Data.Monoid
+import Data.Coerce
+
+import Data.Propagator.Class
+import System.IO.RecThunk
+
+-- | A value of type @Purify p@ is a propagator @p@, gether with a (lazy)
+-- action to define it.
+--
+-- You can use 'get' to extract the value from the propagator.
+--
+-- Do not use the extracted value in the definition of that value, this will
+-- loop just like a recursive definition with plain values would!
+data Purify p = Purify
+        { prop :: p
+        , pre :: Thunk
+        , post :: Thunk
+        }
+
+-- | Any value of type @a@ is also a value of type @Purify p@ if @p@ is a propagator for @a@.
+mk :: Propagator p a => a -> Purify p
+mk x = unsafePerformIO $ do
+    p <- newConstProp x
+    t1 <- doneThunk
+    t2 <- doneThunk
+    pure (Purify p t1 t2)
+
+new :: Propagator p a => [Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
+new ts1 ts2 act = unsafePerformIO $ do
+    p <- newProp
+    t1 <- thunk $ act p >> pure ts1
+    t2 <- thunk $ freezeProp p >> pure ts2
+    pure (Purify p t1 t2)
+
+-- | Defines a value of type @Purify b@ to be a function of the values of @Purify a@.
+--
+-- The action passed should declare that relation to the underlying propagator.
+--
+-- The @Prop a@ propagator must only be used for reading values /from/.
+def1 :: (Propagator pa a, Propagator pb b) =>
+    (pa -> pb -> IO ()) ->
+    Purify pa -> Purify pb
+def1 def r1 = new [pre r1] [post r1] $ \p -> do
+    def (prop r1) p
+
+-- | Defines a value of type @Purify c@ to be a function of the values of @Purify a@ and @Purify b@.
+--
+-- The action passed should declare that relation to the underlying propagator.
+--
+-- The @Prop a@ and @Prop b@ propagators must only be used for reading values /from/.
+def2 :: (Propagator pa a, Propagator pb b, Propagator pc c) =>
+    (pa -> pb -> pc -> IO ()) ->
+    Purify pa -> Purify pb -> Purify pc
+def2 def r1 r2 = new [pre r1, pre r2] [post r1, post r2] $ \p -> do
+    def (prop r1) (prop r2) p
+
+-- | Defines a value of type @Purify b@ to be a function of the values of a list of @Purify a@ values.
+--
+-- The action passed should declare that relation to the underlying propagator.
+--
+-- The @Prop a@ propagators must only be used for reading values /from/.
+defList :: (Propagator pa a, Propagator pb b) =>
+    ([pa] -> pb -> IO ()) ->
+    [Purify pa] -> Purify pb
+defList def rs = new (map pre rs) (map post rs) $ \p -> do
+    def (map prop rs) p
+
+-- | Extract the value from a @Purify a@. This must not be used when /defining/ that value.
+get :: Propagator pa a => Purify pa -> a
+get r = unsafePerformIO $ do
+    force (pre r)
+    force (post r)
+    readProp (prop r)
diff --git a/Data/Recursive/Bool.hs b/Data/Recursive/Bool.hs
--- a/Data/Recursive/Bool.hs
+++ b/Data/Recursive/Bool.hs
@@ -1,12 +1,12 @@
 {-# LANGUAGE TypeApplications #-}
 
-{- | The type @R Bool@ is ike 'Bool', but allows recursive definitions:
+{- | The type @RBool@ is like 'Bool', but allows recursive definitions:
 
 >>> :{
-  let x = rTrue
-      y = x &&& z
-      z = y ||| rFalse
-  in getR x
+  let x = RB.true
+      y = x RB.&& z
+      z = y RB.|| RB.false
+  in RB.get x
 :}
 True
 
@@ -14,88 +14,95 @@
 This finds the least solution, i.e. prefers 'False' over 'True':
 
 >>> :{
-  let x = x &&& y
-      y = y &&& x
-  in (getR x, getR y)
+  let x = x RB.&& y
+      y = y RB.&& x
+  in (RB.get x, RB.get y)
 :}
 (False,False)
 
-Use @R (Dual Bool)@ from "Data.Recursive.DualBool" if you want the greatest solution.
+Use 'Data.Recursive.DualBool.RDualBool' from "Data.Recursive.DualBool" if you want the greatest solution.
 
 -}
-module Data.Recursive.Bool
-  ( R
-  , getR
-  , module Data.Recursive.Bool
-  ) where
+module Data.Recursive.Bool (RBool, module Data.Recursive.Bool) where
 
 
 import Data.Coerce
 import Data.Monoid
 
-import Data.Recursive.R.Internal
-import Data.Recursive.R
-import Data.Recursive.Propagator.P2
+import Data.Recursive.Internal
+import qualified Data.Propagator.Purify as Purify
+import Data.Propagator.P2
 
 -- $setup
+-- >>> :load Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> :module - Data.Recursive.Bool Data.Recursive.DualBool
+--
 -- >>> :set -XFlexibleInstances
 -- >>> import Test.QuickCheck
--- >>> instance Arbitrary (R Bool) where arbitrary = mkR <$> arbitrary
--- >>> instance Show (R Bool) where show = show . getR
--- >>> instance Arbitrary (R (Dual Bool)) where arbitrary = mkR <$> arbitrary
--- >>> instance Show (R (Dual Bool)) where show = show . getR
-
--- | prop> getR rTrue == True
-rTrue :: R Bool
-rTrue = mkR True
-
--- | prop> getR rFalse == False
-rFalse :: R Bool
-rFalse = mkR False
-
-{- Using the naive propagator:
-
-(&&&) :: R Bool -> R Bool -> R Bool
-(&&&) = defR2 $ lift2 (&&)
-
-(|||) :: R Bool -> R Bool -> R Bool
-(|||) = defR2 $ lift2 (||)
+-- >>> import qualified Data.Recursive.Bool as RB
+-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary
+-- >>> instance Show RB.RBool where show = show . RB.get
+--
+-- >>> import qualified Data.Recursive.DualBool as RDB
+-- >>> instance Arbitrary RDB.RDualBool where arbitrary = RDB.mk <$> arbitrary
+-- >>> instance Show RDB.RDualBool where show = show . RDB.get
 
-rand :: [R Bool] -> R Bool
-rand = defRList $ liftList and
+-- | Extracts the value of a 'RBool'
+get :: RBool -> Bool
+get (RBool p) = Purify.get p
 
-ror :: [R Bool] -> R Bool
-ror = defRList $ liftList or
+-- | prop> RB.get (RB.mk b) === b
+mk :: Bool -> RBool
+mk b = RBool $ Purify.mk b
 
-rnot :: R (Dual Bool) -> R Bool
-rnot = defR1 $ lift1 $ coerce not
+-- | prop> RB.get RB.true == True
+true :: RBool
+true = RBool $ Purify.mk True
 
--}
+-- | prop> RB.get RB.false == False
+false :: RBool
+false = RBool $ Purify.mk False
 
--- | prop> getR (r1 &&& r2) === (getR r1 && getR r2)
-(&&&) :: R Bool -> R Bool -> R Bool
-(&&&) = defR2 $ coerce $ \p1 p2 p ->
+-- | prop> RB.get (r1 RB.&& r2) === (RB.get r1 && RB.get r2)
+(&&) :: RBool -> RBool -> RBool
+(&&) = coerce $ Purify.def2 $ \p1 p2 p ->
     whenTop p1 (whenTop p2 (setTop p))
 
--- | prop> getR (r1 ||| r2) === (getR r1 || getR r2)
-(|||) :: R Bool -> R Bool -> R Bool
-(|||) = defR2 $ coerce $ \p1 p2 p -> do
+-- | prop> RB.get (r1 RB.|| r2) === (RB.get r1 || RB.get r2)
+(||) :: RBool -> RBool -> RBool
+(||) = coerce $ Purify.def2 $ \p1 p2 p -> do
     whenTop p1 (setTop p)
     whenTop p2 (setTop p)
 
--- | prop> getR (rand rs) === and (map getR rs)
-rand :: [R Bool] -> R Bool
-rand = defRList $ coerce go
+-- | prop> RB.get (RB.and rs) === and (map RB.get rs)
+and :: [RBool] -> RBool
+and = coerce $ Purify.defList $ go
   where
     go [] p = setTop p
     go (p':ps) p = whenTop p' (go ps p)
 
--- | prop> getR (ror rs) === or (map getR rs)
-ror :: [R Bool] -> R Bool
-ror = defRList $ coerce $ \ps p ->
+-- | prop> RB.get (RB.or rs) === or (map RB.get rs)
+or :: [RBool] -> RBool
+or = coerce $ Purify.defList $  \ps p ->
     mapM_ @[] (`implies` p) ps
 
--- | prop> getR (rnot r1) === not (getRDual r1)
-rnot :: R (Dual Bool) -> R Bool
-rnot = defR1 $ coerce $ \p1 p -> do
+-- | prop> RB.get (RB.not r1) === not (RDB.get r1)
+not :: RDualBool -> RBool
+not = coerce $ Purify.def1 $ \p1 p -> do
+    implies p1 p
+
+-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:
+--
+-- > let x = x in RB.get x
+--
+-- will not work, but
+--
+-- >>> let x = RB.id x in RB.get x
+-- False
+--
+-- does.
+--
+-- prop> RB.get (RB.id r) === RB.get r
+id :: RBool -> RBool
+id = coerce $ Purify.def1 $ \p1 p ->
     implies p1 p
diff --git a/Data/Recursive/DualBool.hs b/Data/Recursive/DualBool.hs
--- a/Data/Recursive/DualBool.hs
+++ b/Data/Recursive/DualBool.hs
@@ -1,14 +1,12 @@
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeApplications #-}
 
-{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:
+{- | The type @RDualBool@ is like 'Bool', but allows recursive definitions:
 
 >>> :{
-  let x = rTrue
-      y = x &&& z
-      z = y ||| rFalse
-  in getRDual x
+  let x = RDB.true
+      y = x RDB.&& z
+      z = y RDB.|| RDB.false
+  in RDB.get x
 :}
 True
 
@@ -16,68 +14,94 @@
 This finds the greatest solution, i.e. prefers 'True' over 'False':
 
 >>> :{
-  let x = x &&& y
-      y = y &&& x
-  in (getRDual x, getRDual y)
+  let x = x RDB.&& y
+      y = y RDB.&& x
+  in (RDB.get x, RDB.get y)
 :}
 (True,True)
 
-Use @R Bool@ from "Data.Recursive.Bool" if you want the least solution.
+Use @RBool@ from "Data.Recursive.Bool" if you want the least solution.
 
 -}
-module Data.Recursive.DualBool
-  ( R
-  , getRDual
-  , module Data.Recursive.DualBool
-  ) where
+module Data.Recursive.DualBool (RDualBool, module Data.Recursive.DualBool) where
 
 import Data.Coerce
 import Data.Monoid
 
-import Data.Recursive.R.Internal
-import Data.Recursive.R
-import Data.Recursive.Propagator.P2
+import Data.Recursive.Internal
+import qualified Data.Propagator.Purify as Purify
+import Data.Propagator.P2
 
 -- $setup
+-- >>> :load Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> :module - Data.Recursive.Bool Data.Recursive.DualBool
+--
 -- >>> :set -XFlexibleInstances
 -- >>> import Test.QuickCheck
--- >>> instance Arbitrary (R Bool) where arbitrary = mkR <$> arbitrary
--- >>> instance Show (R Bool) where show = show . getR
--- >>> instance Arbitrary (R (Dual Bool)) where arbitrary = mkR <$> arbitrary
--- >>> instance Show (R (Dual Bool)) where show = show . getR
+-- >>> import qualified Data.Recursive.Bool as RB
+-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary
+-- >>> instance Show RB.RBool where show = show . RB.get
+--
+-- >>> import qualified Data.Recursive.DualBool as RDB
+-- >>> instance Arbitrary RDB.RDualBool where arbitrary = RDB.mk <$> arbitrary
+-- >>> instance Show RDB.RDualBool where show = show . RDB.get
 
--- | prop> getRDual rTrue == True
-rTrue :: R (Dual Bool)
-rTrue = mkR (Dual True)
+-- | Extracts the value of a 'RDualBool'
+get :: RDualBool -> Bool
+get (RDualBool p) = Prelude.not (Purify.get p)
 
--- | prop> getRDual rFalse == False
-rFalse :: R (Dual Bool)
-rFalse = mkR (Dual False)
+-- | prop> RDB.get (RDB.mk b) === b
+mk :: Bool -> RDualBool
+mk b = RDualBool $ Purify.mk (Prelude.not b)
 
--- | prop> getRDual (r1 ||| r2) === (getRDual r1 || getRDual r2)
-(|||) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)
-(|||) = defR2 $ coerce $ \p1 p2 p ->
-    whenTop p1 (whenTop p2 (setTop p))
+-- | prop> RDB.get RDB.true == True
+true :: RDualBool
+true = RDualBool $ Purify.mk False
 
--- | prop> getRDual (r1 &&& r2) === (getRDual r1 && getRDual r2)
-(&&&) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)
-(&&&) = defR2 $ coerce $ \p1 p2 p -> do
+-- | prop> RDB.get RDB.false == False
+false :: RDualBool
+false = RDualBool $ Purify.mk True
+
+-- | prop> RDB.get (r1 RDB.&& r2) === (RDB.get r1 && RDB.get r2)
+(&&) :: RDualBool -> RDualBool -> RDualBool
+(&&) = coerce $ Purify.def2 $ \p1 p2 p -> do
     whenTop p1 (setTop p)
     whenTop p2 (setTop p)
 
--- | prop> getRDual (ror rs) === or (map getRDual rs)
-ror :: [R (Dual Bool)] -> R (Dual Bool)
-ror = defRList $ coerce go
+-- | prop> RDB.get (r1 RDB.|| r2) === (RDB.get r1 || RDB.get r2)
+(||) :: RDualBool -> RDualBool -> RDualBool
+(||) = coerce $ Purify.def2 $ \p1 p2 p ->
+    whenTop p1 (whenTop p2 (setTop p))
+
+-- | prop> RDB.get (RDB.and rs) === and (map RDB.get rs)
+and :: [RDualBool] -> RDualBool
+and = coerce $ Purify.defList $ \ps p ->
+    mapM_ @[] (`implies` p) ps
+
+-- | prop> RDB.get (RDB.or rs) === or (map RDB.get rs)
+or :: [RDualBool] -> RDualBool
+or = coerce $ Purify.defList go
   where
     go [] p = setTop p
     go (p':ps) p = whenTop p' (go ps p)
 
--- | prop> getRDual (rand rs) === and (map getRDual rs)
-rand :: [R (Dual Bool)] -> R (Dual Bool)
-rand = defRList $ coerce $ \ps p ->
-    mapM_ @[] (`implies` p) ps
+-- | prop> RDB.get (RDB.not r1) === not (RB.get r1)
+not :: RBool -> RDualBool
+not = coerce $ Purify.def1 $ \p1 p -> do
+    implies p1 p
 
--- | prop> getRDual (rnot r1) === not (getR r1)
-rnot :: R Bool -> R (Dual Bool)
-rnot = defR1 $ coerce $ \p1 p -> do
+-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:
+--
+-- > let x = x in RDB.get x
+--
+-- will not work, but
+--
+-- >>> let x = RDB.id x in RDB.get x
+-- True
+--
+-- does.
+--
+-- | prop> RDB.get (RDB.id r) === RDB.get r
+id :: RDualBool -> RDualBool
+id = coerce $ Purify.def1 $ \p1 p ->
     implies p1 p
diff --git a/Data/Recursive/Examples.hs b/Data/Recursive/Examples.hs
--- a/Data/Recursive/Examples.hs
+++ b/Data/Recursive/Examples.hs
@@ -18,37 +18,40 @@
 This library provides data types where this works. You can write the equations
 in that way just fine, and still get a result.
 
-For example, the @R Bool@ type comes with functions that look quite like their
+For example, the 'Data.Recursive.Bool.RBool' type comes with functions that look quite like their
 ordinary counterparts acting on 'Bool'.
 
->>> :t rTrue
-rTrue :: R Bool
->>> :t rFalse
-rFalse :: R Bool
->>> :t (|||)
-(|||) :: R Bool -> R Bool -> R Bool
->>> :t (&&&)
-(&&&) :: R Bool -> R Bool -> R Bool
->>> getR rTrue
+>>> import Data.Recursive.Bool (RBool)
+>>> import qualified Data.Recursive.Bool as RB
+
+>>> :t RB.true
+RB.true :: RBool
+>>> :t RB.false
+RB.false :: RBool
+>>> :t (RB.||)
+(RB.||) :: RBool -> RBool -> RBool
+>>> :t (RB.&&)
+(RB.&&) :: RBool -> RBool -> RBool
+>>> RB.get RB.true
 True
->>> getR rFalse
+>>> RB.get RB.false
 False
->>> getR (rFalse &&& rTrue)
+>>> RB.get (RB.false RB.&& RB.true)
 False
->>> getR (rTrue &&& rTrue)
+>>> RB.get (RB.true RB.&& RB.true)
 True
->>> getR (ror [rTrue,  rFalse, rTrue])
+>>> RB.get (RB.or [RB.true,  RB.false, RB.true])
 True
 
 So far so good, lets see what happens when we try something recursive:
 
->>> let x = ror [y]; y = rand [x, rFalse] in getR x
+>>> let x = RB.or [y]; y = RB.and [x, RB.false] in RB.get x
 False
->>> let x = ror [y]; y = ror [x, rFalse] in getR x
+>>> let x = RB.or [y]; y = RB.or [x, RB.false] in RB.get x
 False
->>> let x = ror [y]; y = ror [x, rTrue] in getR x
+>>> let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x
 True
->>> let x = ror [y]; y = ror [x] in getR x
+>>> let x = RB.or [y]; y = RB.or [x] in RB.get x
 False
 
 == Least or greatest solution
@@ -60,42 +63,45 @@
 We (arbitrary) choose to find the least solution, i.e. prefer @False@ and
 only find @True@ if we have to. This is useful, for example, if you check something recursive for errors.
 
-Sometimes you want the other one. Then you can use @R (Dual Bool)@. The module
-"Data.Recursive.DualBool" exports all the functions for that type too. Because
-of the name class we have imported it qualified here. We can run run the same
-quations, and get different answers:
+Sometimes you want the other one. Then you can use @RDualBool@. The module
+"Data.Recursive.DualBool" exports all the functions for that type too. We can
+run the same equations, and get different answers:
 
->>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x
+>>> import Data.Recursive.DualBool (RDualBool)
+>>> import qualified Data.Recursive.DualBool as RDB
+
+
+>>> let x = RDB.or [y]; y = RDB.and [x, RDB.false] in RDB.get x
 False
->>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.false] in RDB.get x
 True
->>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.true] in RDB.get x
 True
->>> let x = DB.ror [y]; y = DB.ror [x] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x] in RDB.get x
 True
 
 The negation function is also available, and goes from can-be-true to must-be-true and back:
 
->>> :t rnot
-rnot :: R (Dual Bool) -> R Bool
->>> :t DB.rnot
-DB.rnot :: R Bool -> R (Dual Bool)
+>>> :t RB.not
+RB.not :: RDualBool -> RBool
+>>> :t RDB.not
+RDB.not :: RBool -> RDualBool
 
 This allows us to mix the different types in the same computation:
 
 >>> :{
-  let x = rnot y ||| rnot z
-      y = DB.rnot x DB.&&& z
-      z = DB.rTrue
-  in (getR x, getRDual y, getRDual z)
+  let x = RB.not y RB.|| RB.not z
+      y = RDB.not x RDB.&& z
+      z = RDB.true
+  in (RB.get x, RDB.get y, RDB.get z)
  :}
 (False,True,True)
 
 >>> :{
-  let x = rnot y ||| rnot z
-      y = DB.rnot x DB.&&& z
-      z = DB.rFalse
-  in (getR x, getRDual y, getRDual z)
+  let x = RB.not y RB.|| RB.not z
+      y = RDB.not x RDB.&& z
+      z = RDB.false
+  in (RB.get x, RDB.get y, RDB.get z)
  :}
 (True,False,False)
 
@@ -104,27 +110,29 @@
 We do not have to stop with booleans, and can define similar APIs for other
 data stuctures, e.g. sets:
 
-Again we can describe sets recursively, using the monotone functions 'rEmpty',
-'rInsert' and 'rUnion'
+>>> import qualified Data.Recursive.Set as RS
 
+Again we can describe sets recursively, using the monotone functions 'RS.empty',
+'RS.insert' and 'RS.union'
+
 >>> :{
-  let s1 = rInsert 23 s2
-      s2 = rInsert 42 s1
-  in getR s1
+  let s1 = RS.insert 23 s2
+      s2 = RS.insert 42 s1
+  in RS.get s1
  :}
 fromList [23,42]
 
-Here is a slightly larger example, where we can can use this API to elegantly
+Here is a slightly larger example, where we can use this API to elegantly
 calculate the reachable nodes in a graph (represented as a map from vertices to
 their successors), using a typical knot-tying approach. But unless with plain
 'S.Set', it now works even if the graph has cycles:
 
 >>> :{
    reachable :: M.Map Int [Int] -> M.Map Int (S.Set Int)
-   reachable g = fmap getR sets
+   reachable g = fmap RS.get sets
      where
-       sets :: M.Map Int (R (S.Set Int))
-       sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g
+       sets :: M.Map Int (RS.RSet Int)
+       sets = M.mapWithKey (\v vs -> RS.insert v (RS.unions [ sets ! v' | v' <- vs ])) g
  :}
 
 >>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]
@@ -137,37 +145,37 @@
 
 Of course, the magic stops somewhere: Just like with the usual knot-tying
 tricks, you still have to make sure to be lazy enough. In particular, you should
-not peek at the value (e.g. using 'getR') while you are building the graph:
+not peek at the value (e.g. using 'RB.get') while you are building the graph:
 
 >>> :{
     withTimeout $
-      let x = rand [x, if getR y then z else rTrue]
-          y = rand [x, rTrue]
-          z = rFalse
-      in getR y
+      let x = RB.and [x, if RB.get y then z else RB.true]
+          y = RB.and [x, RB.true]
+          z = RB.false
+      in RB.get y
     :}
 *** Exception: timed out
 
 Similarly, you have to make sure you recurse through one of these functions; @let x = x@ still does not work:
 
->>> withTimeout $ let x = x :: R Bool in getR x
+>>> withTimeout $ let x = x :: RBool in RB.get x
 *** Exception: timed out
->>> withTimeout $ let x = x &&& x in getR x
+>>> withTimeout $ let x = x RB.&& x in RB.get x
 False
 
 We belive that the APIs provided here are still “pure”: evaluation order does not affect the results, and you can replace equals with equals, in the sense that
 
-> let s = rInsert 42 s in s
+> let s = RS.insert 42 s in s
 
 is the same as
 
-> let s = rInsert 42 s in rInsert 42 s
+> let s = RS.insert 42 s in RS.insert 42 s
 
 However, the the following two expressions are not equivalent:
 
->>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s
+>>> withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s
 [42]
->>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())
+>>> withTimeout $ S.toList $ let s () = RS.insert 42 (s ()) in RS.get (s ())
 *** Exception: timed out
 
 It is debatable if that is a problem.
@@ -175,11 +183,11 @@
 -}
 module Data.Recursive.Examples () where
 
-import Data.Recursive.R
-import Data.Recursive.Bool
-import qualified Data.Recursive.DualBool as DB
-import Data.Recursive.Set
-import Data.Monoid
+-- Imports for haddock
+
+import qualified Data.Recursive.Bool as RB
+import qualified Data.Recursive.DualBool as RDB
+import qualified Data.Recursive.Set as RS
 
 -- $setup
 --
diff --git a/Data/Recursive/Internal.hs b/Data/Recursive/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Internal.hs
@@ -0,0 +1,32 @@
+{-# OPTIONS_HADDOCK not-home #-}
+{-# LANGUAGE TypeApplications #-}
+
+{- |
+ This modules contains the newtype definitions backing
+
+  * "Data.Recursive.Bool"
+  * "Data.Recursive.DualBool"
+  * "Data.Recursive.Set"
+
+  Access to the newtype contructor can break the guarantees of these modules.
+  Only import this if you want to extend the APIs for these types.
+-}
+module Data.Recursive.Internal where
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+import qualified Data.Propagator.Purify as Purify
+import Data.Propagator.P2
+import Data.Propagator.Naive
+
+-- | Like 'Bool', but admits recursive definitions, preferring the least solution.
+newtype RBool = RBool (Purify.Purify P2)
+
+-- | Like 'Bool', but admits recursive definitions, preferring the greatest solution.
+newtype RDualBool = RDualBool (Purify.Purify P2)
+
+-- | Like 'S.Set', but admits recursive definitions.
+newtype RSet a = RSet (Purify.Purify (Prop (S.Set a)))
+
+-- | Like 'M.Map', but admits recursive definitions.
+data RMap a b = RMap (RSet a) (M.Map a b)
diff --git a/Data/Recursive/Map.hs b/Data/Recursive/Map.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Map.hs
@@ -0,0 +1,190 @@
+{-# LANGUAGE TypeFamilies #-}
+{- | The type 'RMap' @a@ @b@ is like 'M.Map' @a@ @b@, but allows recursive definitions:
+
+>>> :{
+  let m1 = RM.insert 23 "Hello" m2
+      m2 = RM.insert 42 "World" m1
+  in RM.get m1
+ :}
+fromList [(23,"Hello"),(42,"World")]
+
+All functions in this API are monotone with regard to the ordering of maps that
+uses the /discrete/ order on its elements. Furthermore, we only include
+functions where the key set does not depend on the actual values of the maps.
+
+This means that maps defined recursively using functions like 'RM.insertWith'
+can be used to construct cyclic data structures:
+
+>>> :{
+  let m = RM.insertWith (++) 23 "Hi" m
+  in take 20 $ RM.get m M.! 23
+ :}
+"HiHiHiHiHiHiHiHiHiHi"
+
+And because the APIs provided by this package work similar to cyclic data
+structures, we can use them inside these maps:
+
+>>> :{
+  let m = RM.insertWith RS.union 23 (RS.singleton "Hi") m
+  in RM.get m
+ :}
+fromList [(23,fromList ["Hi"])]
+
+I am looking for a concice but useful example for this feature to be put here! 
+
+An alternative would be to order these maps using a pointwise order on the maps
+of elements (and do a simple fixed-point iteration underneath). But then we
+could provide a general 'RM.unionWith' function, because not every function
+passed to it would be monotone.
+
+-}
+module Data.Recursive.Map
+  ( RMap
+  , get
+  , mk
+  , empty
+  , singleton
+  , insert
+  , insertWith
+  , insertWithKey
+  , delete
+  , adjust
+  , adjustWithKey
+  , union
+  , unionWith
+  , unionWithKey
+  , intersection
+  , intersectionWith
+  , intersectionWithKey
+  , member
+  , notMember
+  , disjoint
+  , Data.Recursive.Map.null
+  , fromSet
+  , keysSet
+  , restrictKeys
+  ) where
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Data.Coerce
+import Data.Monoid
+import Control.Monad
+
+import Data.Recursive.Internal
+import qualified Data.Recursive.Set as RS
+
+-- $setup
+-- >>> :load Data.Recursive.Set Data.Recursive.Map Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> :module - Data.Recursive.Set Data.Recursive.Map Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> import qualified Data.Recursive.Set as RS
+-- >>> import qualified Data.Recursive.Map as RM
+-- >>> import qualified Data.Recursive.Bool as RB
+-- >>> import qualified Data.Recursive.DualBool as RDB
+-- >>> import qualified Data.Set as S
+-- >>> import qualified Data.Map as M
+-- >>> :set -XFlexibleInstances
+-- >>> :set -XScopedTypeVariables
+-- >>> import Test.QuickCheck
+-- >>> instance (Ord a, Arbitrary a) => Arbitrary (RS.RSet a) where arbitrary = RS.mk <$> arbitrary
+-- >>> instance (Ord a, Show a) => Show (RS.RSet a) where show = show . RS.get
+-- >>> instance (Ord a, Arbitrary a, Arbitrary b) => Arbitrary (RM.RMap a b) where arbitrary = RM.mk <$> arbitrary
+-- >>> instance (Ord a, Show a, Show b) => Show (RM.RMap a b) where show = show . RM.get
+
+-- | Extracts the value of a 'MSet'
+get :: RMap a b -> M.Map a b
+get (RMap _s m) = m
+
+-- | prop> RM.get (RM.mk m) === m
+mk :: M.Map a b -> RMap a b
+mk m = RMap (RS.mk (M.keysSet m)) m
+
+-- | prop> RM.get RM.empty === M.empty
+empty :: RMap a b
+empty = RMap RS.empty M.empty
+
+-- | prop> RM.get (RM.singleton k v) === M.singleton k v
+singleton :: a -> b -> RMap a b
+singleton k v = RMap (RS.singleton k) (M.singleton k v)
+
+build :: Ord a => RS.RSet a -> M.Map a b -> RMap a b
+build s m = RMap s (M.fromSet (m M.!) (RS.get s))
+
+-- | prop> RM.get (RM.insert k v m) === M.insert k v (RM.get m)
+insert :: Ord a => a -> b -> RMap a b -> RMap a b
+insert k v ~(RMap rs m) = build (RS.insert k rs) (M.insert k v m)
+
+-- | prop> RM.get (RM.insertWith (applyFun2 f) k v m) === M.insertWith (applyFun2 f) k v (RM.get m)
+insertWith :: Ord a => (b -> b -> b) -> a -> b -> RMap a b -> RMap a b
+insertWith f k v ~(RMap rs m) = build (RS.insert k rs) (M.insertWith f k v m)
+
+-- | prop> RM.get (RM.insertWithKey (applyFun3 f) k v m) === M.insertWithKey (applyFun3 f) k v (RM.get m)
+insertWithKey :: Ord a => (a -> b -> b -> b) -> a -> b -> RMap a b -> RMap a b
+insertWithKey f k v ~(RMap rs m) = build (RS.insert k rs) (M.insertWithKey f k v m)
+
+-- | prop> RM.get (RM.delete k m) === M.delete k (RM.get m)
+delete :: Ord a => a -> RMap a b -> RMap a b
+delete k ~(RMap rs m) = build (RS.delete k rs) (M.delete k m)
+
+-- | prop> RM.get (RM.adjust (applyFun f) k m) === M.adjust (applyFun f) k (RM.get m)
+adjust :: Ord a => (b -> b) -> a -> RMap a b -> RMap a b
+adjust f k ~(RMap rs m) = build (RS.id rs) (M.adjust f k m)
+
+-- | prop> RM.get (RM.adjustWithKey (applyFun2 f) k m) === M.adjustWithKey (applyFun2 f) k (RM.get m)
+adjustWithKey :: Ord a => (a -> b -> b) -> a -> RMap a b -> RMap a b
+adjustWithKey f k ~(RMap rs m) = build (RS.id rs) (M.adjustWithKey f k m)
+
+-- | prop> RM.get (RM.union m1 m2) === M.union (RM.get m1) (RM.get m2)
+union :: Ord a => RMap a b -> RMap a b -> RMap a b
+union ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.union m1 m2)
+
+-- | prop> RM.get (RM.unionWith (applyFun2 f) m1 m2) === M.unionWith (applyFun2 f) (RM.get m1) (RM.get m2)
+unionWith :: Ord a => (b -> b -> b) -> RMap a b -> RMap a b -> RMap a b
+unionWith f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.unionWith f m1 m2)
+
+-- | prop> RM.get (RM.unionWithKey (applyFun3 f) m1 m2) === M.unionWithKey (applyFun3 f) (RM.get m1) (RM.get m2)
+unionWithKey :: Ord a => (a -> b -> b -> b) -> RMap a b -> RMap a b -> RMap a b
+unionWithKey f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.unionWithKey f m1 m2)
+
+-- | prop> RM.get (RM.intersection m1 m2) === M.intersection (RM.get m1) (RM.get m2)
+intersection :: Ord a => RMap a b -> RMap a b -> RMap a b
+intersection ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersection m1 m2)
+
+-- | prop> RM.get (RM.intersectionWith (applyFun2 f) m1 m2) === M.intersectionWith (applyFun2 f) (RM.get m1) (RM.get m2)
+intersectionWith :: Ord a => (b -> b -> b) -> RMap a b -> RMap a b -> RMap a b
+intersectionWith f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersectionWith f m1 m2)
+
+-- | prop> RM.get (RM.intersectionWithKey (applyFun3 f) m1 m2) === M.intersectionWithKey (applyFun3 f) (RM.get m1) (RM.get m2)
+intersectionWithKey :: Ord a => (a -> b -> b -> b) -> RMap a b -> RMap a b -> RMap a b
+intersectionWithKey f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersectionWithKey f m1 m2)
+
+
+-- | prop> RM.get (RM.singleton k v) === M.singleton k v
+fromSet :: (a -> b) -> RS.RSet a -> RMap a b
+fromSet f s = RMap s (M.fromSet f (RS.get s))
+
+-- | prop> RS.get (RM.keysSet m) === M.keysSet (RM.get m)
+keysSet :: RMap a b -> RS.RSet a
+keysSet ~(RMap rs m) = RS.id rs
+  -- better use RS.id either here or in fromSet, to avoid unproductive loops
+
+-- | prop> RM.get (RM.restrictKeys m s) === M.restrictKeys (RM.get m) (RS.get s)
+restrictKeys :: Ord a => RMap a b -> RS.RSet a -> RMap a b
+restrictKeys ~(RMap rs m) s2 =
+    build (rs `RS.intersection` s2) (M.restrictKeys m (RS.get s2))
+
+-- | prop> RB.get (RM.member k m) === M.member k (RM.get m)
+member :: Ord a => a -> RMap a b -> RBool
+member x ~(RMap rs m) = RS.member x rs
+
+-- | prop> RDB.get (RM.notMember n r1) === M.notMember n (RM.get r1)
+notMember :: Ord a => a -> RMap a b -> RDualBool
+notMember x ~(RMap rs m) = RS.notMember x rs
+
+-- | prop> RDB.get (RM.disjoint m1 m2) === M.disjoint (RM.get m1) (RM.get m2)
+disjoint :: Ord a => RMap a b -> RMap a b -> RDualBool
+disjoint ~(RMap rs1 _ ) ~(RMap rs2 m2) = RS.disjoint rs1 rs2
+
+-- | prop> RDB.get (RM.null m) === M.null (RM.get m)
+null :: Ord a =>  RMap a b -> RDualBool
+null ~(RMap rs m) = RS.null rs
diff --git a/Data/Recursive/Propagator/Class.hs b/Data/Recursive/Propagator/Class.hs
deleted file mode 100644
--- a/Data/Recursive/Propagator/Class.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FunctionalDependencies #-}
-
--- | This module provides the 'Propagator' and 'HasPropagator' classes.
-module Data.Recursive.Propagator.Class where
-
-import Data.Monoid (Dual(..))
-import qualified Data.Set as S
-import Data.Coerce
-
-import qualified Data.Recursive.Propagator.Naive as Naive
-import Data.Recursive.Propagator.P2
-import Data.POrder
-
--- | The Propagator class defines some functions shared by different propagator
--- implementations. This backs the generic "Data.Recursive.R.Internal" wrapper.
-class Propagator p x | p -> x where
-    -- | The type of values inside the propagator
-    newProp :: IO p
-    newConstProp :: x -> IO p
-    readProp :: p -> IO x
-
-instance Bottom x => Propagator (Naive.Prop x) x where
-    newProp = Naive.newProp bottom
-    newConstProp = Naive.newProp
-    readProp = Naive.readProp
-
-instance Propagator PBool Bool where
-    newProp = coerce newP2
-    newConstProp False = coerce newP2
-    newConstProp True = coerce newTopP2
-    readProp = coerce isTop
-
-instance Propagator PDualBool (Dual Bool) where
-    newProp = coerce newP2
-    newConstProp (Dual True) = coerce newP2
-    newConstProp (Dual False) = coerce newTopP2
-    readProp = coerce $ fmap not . isTop
-
--- | The HasPropagator class is used to pick a propagator implementation for a
--- particular value type.
-class Propagator (Prop x) x => HasPropagator x where
-    type Prop x
-
-instance HasPropagator Bool where
-    type Prop Bool = PBool
-
-instance HasPropagator (Dual Bool) where
-    type Prop (Dual Bool) = PDualBool
-
-instance Eq a => HasPropagator (S.Set a) where
-    type Prop (S.Set a) = Naive.Prop (S.Set a)
diff --git a/Data/Recursive/Propagator/Naive.hs b/Data/Recursive/Propagator/Naive.hs
deleted file mode 100644
--- a/Data/Recursive/Propagator/Naive.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-
--- | A very naive propagator library.
---
--- This propagator implementation keeps updating the values accoring to their
--- definitions as other values change, until a fixed-point is reached.
---
--- It is a naive implementation and not very clever. Much more efficient
--- propagator implementations are possible, and may be used by this library in
--- the future.
-module Data.Recursive.Propagator.Naive
-    ( Prop
-    , newProp
-    , readProp
-    , watchProp
-    , setProp
-    , lift1
-    , lift2
-    , liftList
-    )
-    where
-
-import Control.Monad
-
--- I want to test this code with dejafu, without carrying it as a dependency
--- of the main library. So here is a bit of CPP to care for that.
-
-#ifdef DEJAFU
-
-#define Ctxt   MonadConc m =>
-#define Prop_  Prop m
-#define IORef_ IORef m
-#define MVar_  MVar m
-#define M      m
-
-import Control.Concurrent.Classy
-
-#else
-
-#define Ctxt
-#define Prop_  Prop
-#define IORef_ IORef
-#define MVar_  MVar
-#define M      IO
-
-import Control.Concurrent.MVar
-import Data.IORef
-
-#endif
-
--- | A cell in a propagator network
-data Prop_ a = Prop
-    { val :: IORef_ a
-    , lock :: MVar_ ()
-    , onChange :: IORef_ (M ())
-    }
-
--- | Creates a cell, given an initial value
-newProp :: Ctxt a -> M (Prop_ a)
-newProp x = do
-    m <- newIORef x
-    l <- newMVar ()
-    notify <- newIORef (pure ())
-    pure $ Prop m l notify
-
--- | Reads the current value of the cell
-readProp :: Ctxt Prop_ a -> M a
-readProp (Prop m _ _ ) = readIORef m
-
--- | Sets a new value calculated from the given action. The action is executed atomically.
---
--- If the value has changed, all watchers are notified afterwards (not atomically).
-setProp :: Ctxt Eq a => Prop_ a -> M a -> M ()
-setProp (Prop m l notify) getX = do
-    () <- takeMVar l
-    old <- readIORef m
-    new <- getX
-    writeIORef m new
-    putMVar l ()
-    unless (new == old) $ join (readIORef notify)
-
--- | Watch a cell: If the value changes, the given action is executed
-watchProp :: Ctxt Prop_ a -> M () -> M ()
-watchProp (Prop _ _ notify) f =
-    atomicModifyIORef notify $ \a -> (f >> a, ())
-
--- | Whenever the first cell changes, update the second, using the given function
-lift1 :: Ctxt Eq b => (a -> b) -> Prop_ a -> Prop_ b -> M ()
-lift1 f p1 p = do
-    let update = setProp p $ f <$> readProp p1
-    watchProp p1 update
-    update
-
--- | Whenever any of the first two cells change, update the third, using the given function
-lift2 :: Ctxt Eq c => (a -> b -> c) -> Prop_ a -> Prop_ b -> Prop_ c -> M ()
-lift2 f p1 p2 p = do
-    let update = setProp p $ f <$> readProp p1 <*> readProp p2
-    watchProp p1 update
-    watchProp p2 update
-    update
-
--- | Whenever any of the cells in the list change, update the other, using the given function
-liftList :: Ctxt Eq b => ([a] -> b) -> [Prop_ a] -> Prop_ b -> M ()
-liftList f ps p = do
-    let update = setProp p $ f <$> mapM readProp ps
-    mapM_ (\p' -> watchProp p' update) ps
-    update
diff --git a/Data/Recursive/Propagator/P2.hs b/Data/Recursive/Propagator/P2.hs
deleted file mode 100644
--- a/Data/Recursive/Propagator/P2.hs
+++ /dev/null
@@ -1,101 +0,0 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE CPP #-}
-
--- | A propagator for the two-point lattice
---
-module Data.Recursive.Propagator.P2
-    ( P2
-    , newP2
-    , newTopP2
-    , setTop
-    , whenTop
-    , implies
-    , isTop
-    , PBool(..)
-    , PDualBool(..)
-    )
-    where
-
--- I want to test this code with dejafu, without carrying it as a dependency
--- of the main library. So here is a bit of CPP to care for that.
-
-#ifdef DEJAFU
-
-#define Ctxt   MonadConc m =>
-#define MaybeTop_  (MaybeTop m)
-#define P2_  (P2 m)
-#define PBool_  PBool m
-#define PDualBool_  PDualBool m
-#define IORef_ IORef m
-#define MVar_  MVar m
-#define M      m
-
-import Control.Concurrent.Classy
-
-#else
-
-#define Ctxt
-#define MaybeTop_  MaybeTop
-#define P2_  P2
-#define PBool_  PBool
-#define PDualBool_  PDualBool
-#define IORef_ IORef
-#define MVar_  MVar
-#define M      IO
-
-import Control.Concurrent.MVar
-import Data.IORef
-
-#endif
-
-data MaybeTop_
-        = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered
-        | SurelyTop           -- ^ Definitely top
-
--- | A type for propagators for the two-point lattice, consisting of bottom and top
-newtype P2_ = P2 (MVar_ MaybeTop_)
-
--- | A new propagator, initialized at bottom
-newP2 :: Ctxt M P2_
-newP2 = P2 <$> newMVar (StillBottom (pure()))
-
--- | A new propagator, already set to top
-newTopP2 :: Ctxt M P2_
-newTopP2 = P2 <$> newMVar SurelyTop
-
--- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run
-whenTop :: Ctxt P2_ -> M () -> M ()
-whenTop (P2 p1) act = takeMVar p1 >>= \case
-    SurelyTop        -> putMVar p1 SurelyTop >> act
-    StillBottom act' -> putMVar p1 (StillBottom (act >> act'))
-
-
--- | Set a propagator to top.
---
--- If it was bottom before, runs the actions queued with 'whenTop'. It does so
--- _after_ setting the propagator to top, so that cycles are broken.
-setTop :: Ctxt P2_ -> M ()
-setTop (P2 p) = takeMVar p >>= \case
-    SurelyTop -> putMVar p SurelyTop
-    StillBottom act -> do
-        -- Do this first, this breaks cycles
-        putMVar p SurelyTop
-        -- Now notify the dependencies
-        act
-
--- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.
-implies :: Ctxt P2_ -> P2_ -> M ()
-implies p1 p2 = whenTop p1 (setTop p2)
-
--- | Queries the current state of the propagator. All related calls to @setTop@
--- that have executed so far are taken into account.
-isTop :: Ctxt P2_ -> M Bool
-isTop (P2 p) = readMVar p >>= \case
-    SurelyTop -> pure True
-    StillBottom _ -> pure False
-
--- | A newtype around 'P2' to denote that bottom is 'False' and top is 'True'
-newtype PBool_ = PBool P2_
-
--- | A newtype around 'P2' to denote that bottom is 'True' and top is 'False'
-newtype PDualBool_ = PDualBool P2_
diff --git a/Data/Recursive/R.hs b/Data/Recursive/R.hs
deleted file mode 100644
--- a/Data/Recursive/R.hs
+++ /dev/null
@@ -1,8 +0,0 @@
--- |
--- This module re-exports the safe parts of "Data.Recursive.R.Internal".
---
--- If you import a module like "Data.Recursive.Bool" you do not need to import
--- this module here directly.
-module Data.Recursive.R (R, mkR, getR, getRDual) where
-
-import Data.Recursive.R.Internal
diff --git a/Data/Recursive/R/Internal.hs b/Data/Recursive/R/Internal.hs
deleted file mode 100644
--- a/Data/Recursive/R/Internal.hs
+++ /dev/null
@@ -1,113 +0,0 @@
-{-# OPTIONS_HADDOCK not-home #-}
-
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-
--- |
---
--- This module provides the 'R' data type, which wraps an imperative propagator (e.g. "Data.Recursive.Propagator.Naive") in a pure and (if done right) safe data structure.
---
--- The result of 'getR' is always a solution of the given equations, but for it
--- to be deterministic (and hence for this API to be safe), the following
--- should hold:
---
--- * The @a@ in @R a@ should be partially orderd ('Data.POrder.POrder')
--- * That partial order must respect equality on @a@
--- * It must have a bottom element 'Data.POrder.bottom' ('Data.POrder.Bottom').
--- * The function passed to 'defR1', 'defR2' etc. must be a monotonic function
---   between these partial orders.
---
--- If this does not hold, then the result of 'getR' may not be deterministic.
---
--- Termination depends on whether a soluiton can be found iteratively. This is
--- guaranteed if all partial orders involved satisfy the Ascending Chain Condition.
-
-module Data.Recursive.R.Internal
-    ( R
-    , getR, getRDual
-    , mkR, defR1, defR2, defRList
-    )
-where
-
-import System.IO.Unsafe
-import Control.Monad.ST
-import Data.Monoid
-import Data.Coerce
-
-import Data.Recursive.Propagator.Class
-import System.IO.RecThunk
-
--- | A value of type @R a@ is a @a@, but defined using only specific operations
--- (which you will find in the corresponding module, e.g.
--- "Data.Recursive.Bool"), which allow recursive definitions.
---
--- You can use 'getR' to extract the value.
---
--- Do not use the extracted value in the definition of that value, this will
--- loop just like a recursive definition with plain values would.
-data R a = R (Prop a) Thunk
-
--- | Any value of type @a@ is also a value of type @r a@.
-mkR :: HasPropagator a => a -> R a
-mkR x = unsafePerformIO $ do
-    p <- newConstProp x
-    t <- doneThunk
-    pure (R p t)
-
-newR :: HasPropagator a => (Prop a -> IO [Thunk]) -> R a
-newR act = unsafePerformIO $ do
-    p <- newProp
-    t <- thunk (act p)
-    pure (R p t)
-
--- | Defines a value of type @R b@ to be a function of the values of @R a@.
---
--- The action passed it should declare that relation to the underlying propagator.
---
--- The @Prop a@ propagator must only be used for reading values _from_.
-defR1 :: (HasPropagator a, HasPropagator b) =>
-    (Prop a -> Prop b -> IO ()) ->
-    R a -> R b
-defR1 def r1 = newR $ \p -> do
-    let R p1 t1 = r1
-    def p1 p
-    pure [t1]
-
--- | Defines a value of type @R c@ to be a function of the values of @R a@ and @R b@.
---
--- The action passed it should declare that relation to the underlying propagator.
---
--- The @Prop a@ and @Prop b@ propagators must only be used for reading values _from_.
-defR2 :: (HasPropagator a, HasPropagator b, HasPropagator c) =>
-    (Prop a -> Prop b -> Prop c -> IO ()) ->
-    R a -> R b -> R c
-defR2 def r1 r2 = newR $ \p -> do
-    let R p1 t1 = r1
-    let R p2 t2 = r2
-    def p1 p2 p
-    pure [t1, t2]
-
--- | Defines a value of type @R b@ to be a function of the values of a list of @R a@ values.
---
--- The action passed it should declare that relation to the underlying propagator.
---
--- The @Prop a@ propagators must only be used for reading values _from_.
-defRList :: (HasPropagator a, HasPropagator b) =>
-    ([Prop a] -> Prop b -> IO ()) ->
-    [R a] -> R b
-defRList def rs = newR $ \p -> do
-    def [ p' | R p' _ <- rs] p
-    pure [ t | R _ t <- rs]
-
--- | Extract the value from a @R a@. This must not be used when _defining_ that value.
-getR :: HasPropagator a => R a -> a
-getR (R p t) = unsafePerformIO $ do
-    force t
-    readProp p
-
--- | Convenience variant of 'getR' to also remove the 'Dual' newtype wrapper, mostly for use with "Data.Recursive.DualBool".
-getRDual :: HasPropagator (Dual a) => R (Dual a) -> a
-getRDual = getDual . getR
diff --git a/Data/Recursive/Set.hs b/Data/Recursive/Set.hs
--- a/Data/Recursive/Set.hs
+++ b/Data/Recursive/Set.hs
@@ -1,90 +1,128 @@
 {-# LANGUAGE TypeFamilies #-}
-{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:
+{- | The type @RS.RSet a@ is like 'S.Set' @a@, but allows recursive definitions:
 
 >>> :{
-  let s1 = rInsert 23 s2
-      s2 = rInsert 42 s1
-  in getR s1
+  let s1 = RS.insert 23 s2
+      s2 = RS.insert 42 s1
+  in RS.get s1
  :}
 fromList [23,42]
 
 -}
-module Data.Recursive.Set
-  ( R
-  , mkR
-  , getR
-  , module Data.Recursive.Set
-  ) where
+module Data.Recursive.Set (RSet, module Data.Recursive.Set) where
 
 import qualified Data.Set as S
 import Data.Coerce
 import Data.Monoid
 import Control.Monad
 
-import Data.Recursive.R.Internal
-import Data.Recursive.Propagator.Naive
-import Data.Recursive.Propagator.P2
+import Data.Recursive.Internal
+import qualified Data.Propagator.Purify as Purify
+import Data.Propagator.Naive
+import Data.Propagator.P2
 
 -- $setup
+-- >>> :load Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> :module - Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool
+-- >>> import qualified Data.Recursive.Set as RS
+-- >>> import qualified Data.Recursive.Bool as RB
+-- >>> import qualified Data.Recursive.DualBool as RDB
+-- >>> import qualified Data.Set as S
 -- >>> :set -XFlexibleInstances
 -- >>> :set -XScopedTypeVariables
 -- >>> import Test.QuickCheck
--- >>> instance (Ord a, Arbitrary a) => Arbitrary (R (S.Set a)) where arbitrary = mkR <$> arbitrary
--- >>> instance (Eq a, Show a) => Show (R (S.Set a)) where show = show . getR
+-- >>> instance (Ord a, Arbitrary a) => Arbitrary (RS.RSet a) where arbitrary = RS.mk <$> arbitrary
+-- >>> instance (Ord a, Show a) => Show (RS.RSet a) where show = show . RS.get
 
--- | prop> getR rEmpty === S.empty
-rEmpty :: Eq a => R (S.Set a)
-rEmpty = mkR S.empty
+-- | Extracts the value of a 'RSet a'
+get :: RSet a -> S.Set a
+get (RSet p) = Purify.get p
 
--- | prop> getR (rInsert n r1) === S.insert n (getR r1)
-rInsert :: Ord a => a -> R (S.Set a) -> R (S.Set a)
-rInsert x = defR1 $ lift1 $ S.insert x
+-- | prop> RB.get (RB.mk s) === s
+mk :: S.Set a -> RSet a
+mk s = RSet $ Purify.mk s
 
--- | prop> getR (rDelete n r1) === S.delete n (getR r1)
-rDelete :: Ord a => a -> R (S.Set a) -> R (S.Set a)
-rDelete x = defR1 $ lift1 $ S.delete x
+-- | prop> RS.get RS.empty === S.empty
+empty :: RSet a
+empty = RSet $ Purify.mk S.empty
 
--- | prop> \(Fun _ p) -> getR (rFilter p r1) === S.filter p (getR r1)
-rFilter :: Ord a => (a -> Bool) -> R (S.Set a) -> R (S.Set a)
-rFilter f = defR1 $ lift1 $ S.filter f
+-- | prop> RS.get (RS.singleton x) === S.singleton x
+singleton :: a -> RSet a
+singleton x = RSet $ Purify.mk $ S.singleton x
 
--- | prop> getR (rUnion r1 r2) === S.union (getR r1) (getR r2)
-rUnion :: Ord a => R (S.Set a) -> R (S.Set a) -> R (S.Set a)
-rUnion = defR2 $ lift2 S.union
+-- | prop> RS.get (RS.insert n r1) === S.insert n (RS.get r1)
+insert :: Ord a => a -> RSet a -> RSet a
+insert x = coerce $ Purify.def1 $ lift1 $ S.insert x
 
--- | prop> getR (rUnions rs) === S.unions (map getR rs)
-rUnions :: Ord a => [R (S.Set a)] -> R (S.Set a)
-rUnions = defRList $ liftList S.unions
+-- | prop> RS.get (RS.delete n r1) === S.delete n (RS.get r1)
+delete :: Ord a => a -> RSet a -> RSet a
+delete x = coerce $ Purify.def1 $ lift1 $ S.delete x
 
--- | prop> getR (rIntersection r1 r2) === S.intersection (getR r1) (getR r2)
-rIntersection :: Ord a => R (S.Set a) -> R (S.Set a) -> R (S.Set a)
-rIntersection = defR2 $ lift2 S.intersection
+-- | prop> \(Fun _ p) -> RS.get (RS.filter p r1) === S.filter p (RS.get r1)
+filter :: Ord a => (a -> Bool) -> RSet a -> RSet a
+filter f = coerce $ Purify.def1 $ lift1 $ S.filter f
 
--- | prop> getR (rMember n r1) === S.member n (getR r1)
-rMember :: Ord a => a -> R (S.Set a) -> R Bool
-rMember x = defR1 $ \ps pb -> do
+-- | prop> RS.get (RS.union r1 r2) === S.union (RS.get r1) (RS.get r2)
+union :: Ord a => RSet a -> RSet a -> RSet a
+union = coerce $ Purify.def2 $ lift2 S.union
+
+-- | prop> RS.get (RS.unions rs) === S.unions (map RS.get rs)
+unions :: Ord a => [RSet a] -> RSet a
+unions = coerce $ Purify.defList $ liftList S.unions
+
+-- | prop> RS.get (RS.intersection r1 r2) === S.intersection (RS.get r1) (RS.get r2)
+intersection :: Ord a => RSet a -> RSet a -> RSet a
+intersection = coerce $ Purify.def2 $ lift2 S.intersection
+
+-- | prop> RB.get (RS.member n r1) === S.member n (RS.get r1)
+member :: Ord a => a -> RSet a -> RBool
+member x = coerce $ Purify.def1 $ \ps pb -> do
     let update = do
             s <- readProp ps
-            when (S.member x s) $ coerce setTop pb
+            when (S.member x s) $ setTop pb
     watchProp ps update
     update
 
--- | prop> getRDual (rNotMember n r1) === S.notMember n (getR r1)
-rNotMember :: Ord a => a -> R (S.Set a) -> R (Dual Bool)
-rNotMember x = defR1 $ \ps pb -> do
+-- | prop> RDB.get (RS.notMember n r1) === S.notMember n (RS.get r1)
+notMember :: Ord a => a -> RSet a -> RDualBool
+notMember x = coerce $ Purify.def1 $ \ps pb -> do
     let update = do
             s <- readProp ps
-            when (S.member x s) $ coerce setTop pb
+            when (S.member x s) $ setTop pb
     watchProp ps update
     update
 
--- | prop> getRDual (rDisjoint r1 r2) === S.disjoint (getR r1) (getR r2)
-rDisjoint :: Ord a => R (S.Set a) -> R (S.Set a) -> R (Dual Bool)
-rDisjoint = defR2 $ \ps1 ps2 (PDualBool pb) -> do
+-- | prop> RDB.get (RS.null s) === S.null (RS.get s)
+null :: RSet a -> RDualBool
+null = coerce $ Purify.def1 $ \ps pb -> do
     let update = do
+            s <- readProp ps
+            unless (S.null s) $ setTop pb
+    watchProp ps update
+    update
+
+-- | prop> RDB.get (RS.disjoint r1 r2) === S.disjoint (RS.get r1) (RS.get r2)
+disjoint :: Ord a => RSet a -> RSet a -> RDualBool
+disjoint = coerce $ Purify.def2 $ \ps1 ps2 pb -> do
+    let update = do
             s1 <- readProp ps1
             s2 <- readProp ps2
-            unless (S.disjoint s1 s2) $ coerce setTop pb
+            unless (S.disjoint s1 s2) $ setTop pb
     watchProp ps1 update
     watchProp ps2 update
     update
+
+-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:
+--
+-- > let x = x in RS.get x
+--
+-- will not work, but
+--
+-- >>> let x = RS.id x in RS.get x
+-- fromList []
+--
+-- does.
+--
+-- | prop> RS.get (RS.id s) === RS.get s
+id :: RSet a -> RSet a
+id = coerce $ Purify.def1 $ lift1 (Prelude.id :: S.Set a -> S.Set a)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -5,15 +5,16 @@
 recursively, and still get a result out:
 
     >>> :{
-      let s1 = rInsert 23 s2
-          s2 = rInsert 42 s1
-      in getR s1
+      let s1 = RS.insert 23 s2
+          s2 = RS.insert 42 s1
+      in RS.get s1
      :}
     fromList [23,42]
 
 See the [`examples.hs`](examples.hs) file for more examples.
 
-It also provides (unsafe) building blocks to build such APIs, see `Data.Recursive.R.Internal`.
+It also provides (unsafe) building blocks to build such APIs, see
+`Data.Propagator.Purify`.
 
 Related work
 ------------
diff --git a/System/IO/RecThunk.hs b/System/IO/RecThunk.hs
--- a/System/IO/RecThunk.hs
+++ b/System/IO/RecThunk.hs
@@ -7,7 +7,7 @@
 
 * 'thunk' is lazy in its argument, and does not run it directly
 * the first 'force' triggers execution of the action passed to thunk
-* that action is run at most once, and returuns a list of other thunks
+* that action is run at most once, and returns a list of other thunks
 * 'force' forces these thunks as well, and does not return before all of them have executed
 * Cycles are allowed: The action passed to 'thunk' may return a thunk whose action returns the first thunk.
 
@@ -46,16 +46,17 @@
 
 #ifdef DEJAFU
 
-#define Ctxt   MonadConc m =>
+#define Ctxt   (MonadConc m, MonadIO m) =>
 #define Thunk_  (Thunk m)
 #define ResolvingState_  (ResolvingState m)
 #define KickedThunk_  (KickedThunk m)
-#define ThreadId_  (ThreadId m)
 #define IORef_ IORef m
 #define MVar_  MVar m
 #define M      m
 
 import Control.Concurrent.Classy hiding (wait)
+import Data.Unique
+import Control.Monad.IO.Class
 
 #else
 
@@ -63,7 +64,6 @@
 #define Thunk_  Thunk
 #define ResolvingState_  ResolvingState
 #define KickedThunk_  KickedThunk
-#define ThreadId_  ThreadId
 #define IORef_ IORef
 #define MVar_  MVar
 #define M      IO
@@ -71,14 +71,14 @@
 import Control.Concurrent.MVar
 import Control.Concurrent
 import Data.IORef
+import Data.Unique
+import Control.Monad.IO.Class
 
 #endif
 
-
-
 -- | An @IO@ action that is to be run at most once
 newtype Thunk_ = Thunk (MVar_ (Either (M [Thunk_]) KickedThunk_))
-data ResolvingState_ = NotStarted | ProcessedBy ThreadId_ (MVar_ ()) | Done
+data ResolvingState_ = NotStarted | ProcessedBy Unique (MVar_ ()) | Done
 -- | A 'Thunk' that is being evaluated
 data KickedThunk_ = KickedThunk (MVar_ [KickedThunk_]) (MVar_ ResolvingState_)
 
@@ -118,9 +118,8 @@
         putMVar t (Right kt)
         pure kt
 
-wait :: Ctxt KickedThunk_ -> M ()
-wait (KickedThunk mv_deps mv_s) = do
-    my_id <- myThreadId
+wait :: Ctxt Unique -> KickedThunk_ -> M ()
+wait my_id (KickedThunk mv_deps mv_s) = do
     s <- takeMVar mv_s
     case s of
         -- Thunk and all dependences are done
@@ -138,7 +137,7 @@
             done_mv <- newEmptyMVar
             putMVar mv_s (ProcessedBy my_id done_mv)
             ts <- readMVar mv_deps
-            mapM_ wait ts
+            mapM_ (wait my_id) ts
             -- Mark kicked thunk as done
             _ <- swapMVar mv_s Done
             -- Wake up waiting threads
@@ -150,4 +149,5 @@
 force :: Ctxt Thunk_ -> M ()
 force t = do
     rt <- kick t
-    wait rt
+    my_id <- liftIO newUnique
+    wait my_id rt
diff --git a/dejafu.hs b/dejafu.hs
deleted file mode 100644
--- a/dejafu.hs
+++ /dev/null
@@ -1,203 +0,0 @@
-import Test.DejaFu
-import Control.Concurrent.Classy
-import Control.Concurrent.Classy.Async
-import qualified Data.Set as S
-import System.Random
-import Control.Monad
-import Test.Tasty
-import Test.Tasty.DejaFu
-
-import Data.Recursive.Propagator.Naive
-import Data.Recursive.Propagator.P2
-import System.IO.RecThunk
-
-t n = testGroup n . pure . testAuto
-
-tr n = testGroup n . pure . testAutoWay (randomly (mkStdGen 0) 1000) defaultMemType
-
-main = defaultMain $ testGroup "tests" $
-  [ t "prop 1" $ do
-        p1 <- newProp (S.singleton 1)
-        readProp p1
-
-  , t "prop 2" $ do
-        p1 <- newProp (S.singleton 1)
-        p2 <- newProp S.empty
-        lift1 (S.insert 3) p1 p2
-        mapConcurrently readProp [p1, p2]
-
-  , tr "prop 2 rec" $ withSetup (do
-        p1 <- newProp S.empty
-        p2 <- newProp S.empty
-        pure (p1, p2)) $ \(p1, p2) -> do
-        mapConcurrently id
-            [ lift1 (S.insert 3) p1 p2
-            , lift1 (S.insert 4) p2 p1
-            ]
-        mapConcurrently readProp [p1, p2]
-
-  , tr "prop 2 rec plus" $ withSetup (do
-        p1 <- newProp S.empty
-        p2 <- newProp S.empty
-        p3 <- newProp S.empty
-        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
-        mapConcurrently id
-            [ lift1 (S.insert 3) p1 p2
-            , lift1 (S.insert 4) p2 p1
-            ]
-        mapConcurrently id
-            [ readProp p1
-            , readProp p2
-            , lift1 (S.insert 5) p2 p3 >> readProp p3
-            ]
-
-
-  , tr "prop 3 rec" $ withSetup (do
-        p1 <- newProp S.empty
-        p2 <- newProp S.empty
-        p3 <- newProp S.empty
-        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
-        mapConcurrently id
-            [ lift1 (S.insert 3) p1 p2
-            , lift1 (S.insert 4) p2 p1
-            , lift1 (S.insert 5) p2 p3
-            ]
-        mapConcurrently readProp [p1, p2, p3]
-
-  , tr "prop 3 rec variant" $ withSetup (do
-        p1 <- newProp S.empty
-        p2 <- newProp S.empty
-        p3 <- newProp S.empty
-        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
-        mapConcurrently id
-            [ lift1 (S.insert 4) p1 p2
-            , lift1 (S.insert 5) p2 p3
-            , lift2 (S.union) p2 p3 p1
-            ]
-        mapConcurrently readProp [p1, p2, p3]
-
-  , tr "prop 4 rec" $ withSetup (do
-        p1 <- newProp S.empty
-        p2 <- newProp S.empty
-        p3 <- newProp S.empty
-        p4 <- newProp S.empty
-        pure (p1, p2, p3, p4)) $ \(p1, p2, p3, p4) -> do
-        mapConcurrently id
-            [ lift1 (S.insert 4) p1 p2
-            , lift2 (S.union) p1 p2 p3
-            , liftList (S.unions) [p1,p2,p3] p4
-            , lift1 (S.insert 5) p4 p1
-            ]
-        mapConcurrently readProp [p1, p2, p3, p4]
-  , t "thunk 1" $ do
-        obs1 <- newIORef 0
-        t1 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            pure []
-        force t1
-        readIORef obs1
-  , t "thunk 1 rec" $ do
-        obs1 <- newIORef 0
-        t1ref <- newIORef undefined
-        t1 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            t1 <- readIORef t1ref
-            pure [t1]
-        writeIORef t1ref t1
-        force t1
-        readIORef obs1
-  , t "thunk 2 rec 12" $ do
-        obs1 <- newIORef 0
-        obs2 <- newIORef 0
-        t2ref <- newIORef undefined
-        t1 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            t2 <- readIORef t2ref
-            pure [t2]
-        t2 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            pure [t1]
-        writeIORef t2ref t2
-        mapConcurrently id
-            [ force t1 >> mapM readIORef [obs1, obs2]
-            , force t2 >> mapM readIORef [obs1, obs2]
-            ]
-  , tr "thunk 2 rec 112" $ do
-        obs1 <- newIORef 0
-        obs2 <- newIORef 0
-        t2ref <- newIORef undefined
-        t1 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            t2 <- readIORef t2ref
-            pure [t2]
-        t2 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            pure [t1]
-        writeIORef t2ref t2
-        mapConcurrently id
-            [ force t1 >> mapM readIORef [obs1, obs2]
-            , force t1 >> mapM readIORef [obs1, obs2]
-            , force t2 >> mapM readIORef [obs1, obs2]
-            ]
-  , tr "thunk 2 all-rec 112" $ do
-        obs1 <- newIORef 0
-        obs2 <- newIORef 0
-        t1ref <- newIORef undefined
-        t2ref <- newIORef undefined
-        t1 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            t1 <- readIORef t1ref
-            t2 <- readIORef t2ref
-            pure [t2,t1]
-        writeIORef t1ref t1
-        t2 <- thunk $ do
-            atomicModifyIORef' obs1 (\x -> (succ x, ()))
-            t2 <- readIORef t2ref
-            pure [t1,t2]
-        writeIORef t2ref t2
-        mapConcurrently id
-            [ force t1 >> mapM readIORef [obs1, obs2]
-            , force t1 >> mapM readIORef [obs1, obs2]
-            , force t2 >> mapM readIORef [obs1, obs2]
-            ]
-  , t "P2 1" $ do
-    p1 <- newP2
-    False <- isTop p1
-    setTop p1
-    True <- isTop p1
-    pure ()
-  , t "P2 2" $ do
-    p1 <- newP2
-    p2 <- newP2
-    mapConcurrently id
-        [ do
-            False <- isTop p1
-            setTop p1
-            True <- isTop p1
-            pure ()
-        , do
-            False <- isTop p2
-            p1 `implies` p2
-        ]
-    True <- isTop p2
-    pure ()
-  , t "P2 2 rec bottom" $ do
-    p1 <- newP2
-    p2 <- newP2
-    mapConcurrently id
-        [  p1 `implies` p2
-        ,  p2 `implies` p1
-        ]
-    [False, False] <- mapM isTop [p1,p2]
-    pure ()
-  , t "P2 2 rec top" $ do
-    p1 <- newP2
-    p2 <- newP2
-    mapConcurrently id
-        [  p1 `implies` p2
-        ,  p2 `implies` p1
-        , setTop p1
-        ]
-    [True, True] <- mapM isTop [p1,p2]
-    pure ()
-  ]
diff --git a/doctests.hs b/doctests.hs
deleted file mode 100644
--- a/doctests.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Test.DocTest
-main = doctest ["--fast", "-package=QuickCheck", "Data/"]
diff --git a/examples.hs b/examples.hs
--- a/examples.hs
+++ b/examples.hs
@@ -18,37 +18,40 @@
 This library provides data types where this works. You can write the equations
 in that way just fine, and still get a result.
 
-For example, the @R Bool@ type comes with functions that look quite like their
+For example, the 'Data.Recursive.Bool.RBool' type comes with functions that look quite like their
 ordinary counterparts acting on 'Bool'.
 
->>> :t rTrue
-rTrue :: R Bool
->>> :t rFalse
-rFalse :: R Bool
->>> :t (|||)
-(|||) :: R Bool -> R Bool -> R Bool
->>> :t (&&&)
-(&&&) :: R Bool -> R Bool -> R Bool
->>> getR rTrue
+>>> import Data.Recursive.Bool (RBool)
+>>> import qualified Data.Recursive.Bool as RB
+
+>>> :t RB.true
+RB.true :: RBool
+>>> :t RB.false
+RB.false :: RBool
+>>> :t (RB.||)
+(RB.||) :: RBool -> RBool -> RBool
+>>> :t (RB.&&)
+(RB.&&) :: RBool -> RBool -> RBool
+>>> RB.get RB.true
 True
->>> getR rFalse
+>>> RB.get RB.false
 False
->>> getR (rFalse &&& rTrue)
+>>> RB.get (RB.false RB.&& RB.true)
 False
->>> getR (rTrue &&& rTrue)
+>>> RB.get (RB.true RB.&& RB.true)
 True
->>> getR (ror [rTrue,  rFalse, rTrue])
+>>> RB.get (RB.or [RB.true,  RB.false, RB.true])
 True
 
 So far so good, lets see what happens when we try something recursive:
 
->>> let x = ror [y]; y = rand [x, rFalse] in getR x
+>>> let x = RB.or [y]; y = RB.and [x, RB.false] in RB.get x
 False
->>> let x = ror [y]; y = ror [x, rFalse] in getR x
+>>> let x = RB.or [y]; y = RB.or [x, RB.false] in RB.get x
 False
->>> let x = ror [y]; y = ror [x, rTrue] in getR x
+>>> let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x
 True
->>> let x = ror [y]; y = ror [x] in getR x
+>>> let x = RB.or [y]; y = RB.or [x] in RB.get x
 False
 
 == Least or greatest solution
@@ -60,42 +63,45 @@
 We (arbitrary) choose to find the least solution, i.e. prefer @False@ and
 only find @True@ if we have to. This is useful, for example, if you check something recursive for errors.
 
-Sometimes you want the other one. Then you can use @R (Dual Bool)@. The module
-"Data.Recursive.DualBool" exports all the functions for that type too. Because
-of the name class we have imported it qualified here. We can run run the same
-quations, and get different answers:
+Sometimes you want the other one. Then you can use @RDualBool@. The module
+"Data.Recursive.DualBool" exports all the functions for that type too. We can
+run the same equations, and get different answers:
 
->>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x
+>>> import Data.Recursive.DualBool (RDualBool)
+>>> import qualified Data.Recursive.DualBool as RDB
+
+
+>>> let x = RDB.or [y]; y = RDB.and [x, RDB.false] in RDB.get x
 False
->>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.false] in RDB.get x
 True
->>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.true] in RDB.get x
 True
->>> let x = DB.ror [y]; y = DB.ror [x] in getRDual x
+>>> let x = RDB.or [y]; y = RDB.or [x] in RDB.get x
 True
 
 The negation function is also available, and goes from can-be-true to must-be-true and back:
 
->>> :t rnot
-rnot :: R (Dual Bool) -> R Bool
->>> :t DB.rnot
-DB.rnot :: R Bool -> R (Dual Bool)
+>>> :t RB.not
+RB.not :: RDualBool -> RBool
+>>> :t RDB.not
+RDB.not :: RBool -> RDualBool
 
 This allows us to mix the different types in the same computation:
 
 >>> :{
-  let x = rnot y ||| rnot z
-      y = DB.rnot x DB.&&& z
-      z = DB.rTrue
-  in (getR x, getRDual y, getRDual z)
+  let x = RB.not y RB.|| RB.not z
+      y = RDB.not x RDB.&& z
+      z = RDB.true
+  in (RB.get x, RDB.get y, RDB.get z)
  :}
 (False,True,True)
 
 >>> :{
-  let x = rnot y ||| rnot z
-      y = DB.rnot x DB.&&& z
-      z = DB.rFalse
-  in (getR x, getRDual y, getRDual z)
+  let x = RB.not y RB.|| RB.not z
+      y = RDB.not x RDB.&& z
+      z = RDB.false
+  in (RB.get x, RDB.get y, RDB.get z)
  :}
 (True,False,False)
 
@@ -104,27 +110,29 @@
 We do not have to stop with booleans, and can define similar APIs for other
 data stuctures, e.g. sets:
 
-Again we can describe sets recursively, using the monotone functions 'rEmpty',
-'rInsert' and 'rUnion'
+>>> import qualified Data.Recursive.Set as RS
 
+Again we can describe sets recursively, using the monotone functions 'RS.empty',
+'RS.insert' and 'RS.union'
+
 >>> :{
-  let s1 = rInsert 23 s2
-      s2 = rInsert 42 s1
-  in getR s1
+  let s1 = RS.insert 23 s2
+      s2 = RS.insert 42 s1
+  in RS.get s1
  :}
 fromList [23,42]
 
-Here is a slightly larger example, where we can can use this API to elegantly
+Here is a slightly larger example, where we can use this API to elegantly
 calculate the reachable nodes in a graph (represented as a map from vertices to
 their successors), using a typical knot-tying approach. But unless with plain
 'S.Set', it now works even if the graph has cycles:
 
 >>> :{
    reachable :: M.Map Int [Int] -> M.Map Int (S.Set Int)
-   reachable g = fmap getR sets
+   reachable g = fmap RS.get sets
      where
-       sets :: M.Map Int (R (S.Set Int))
-       sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g
+       sets :: M.Map Int (RS.RSet Int)
+       sets = M.mapWithKey (\v vs -> RS.insert v (RS.unions [ sets ! v' | v' <- vs ])) g
  :}
 
 >>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]
@@ -137,37 +145,37 @@
 
 Of course, the magic stops somewhere: Just like with the usual knot-tying
 tricks, you still have to make sure to be lazy enough. In particular, you should
-not peek at the value (e.g. using 'getR') while you are building the graph:
+not peek at the value (e.g. using 'RB.get') while you are building the graph:
 
 >>> :{
     withTimeout $
-      let x = rand [x, if getR y then z else rTrue]
-          y = rand [x, rTrue]
-          z = rFalse
-      in getR y
+      let x = RB.and [x, if RB.get y then z else RB.true]
+          y = RB.and [x, RB.true]
+          z = RB.false
+      in RB.get y
     :}
 *** Exception: timed out
 
 Similarly, you have to make sure you recurse through one of these functions; @let x = x@ still does not work:
 
->>> withTimeout $ let x = x :: R Bool in getR x
+>>> withTimeout $ let x = x :: RBool in RB.get x
 *** Exception: timed out
->>> withTimeout $ let x = x &&& x in getR x
+>>> withTimeout $ let x = x RB.&& x in RB.get x
 False
 
 We belive that the APIs provided here are still “pure”: evaluation order does not affect the results, and you can replace equals with equals, in the sense that
 
-> let s = rInsert 42 s in s
+> let s = RS.insert 42 s in s
 
 is the same as
 
-> let s = rInsert 42 s in rInsert 42 s
+> let s = RS.insert 42 s in RS.insert 42 s
 
 However, the the following two expressions are not equivalent:
 
->>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s
+>>> withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s
 [42]
->>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())
+>>> withTimeout $ S.toList $ let s () = RS.insert 42 (s ()) in RS.get (s ())
 *** Exception: timed out
 
 It is debatable if that is a problem.
@@ -175,11 +183,11 @@
 -}
 module Data.Recursive.Examples () where
 
-import Data.Recursive.R
-import Data.Recursive.Bool
-import qualified Data.Recursive.DualBool as DB
-import Data.Recursive.Set
-import Data.Monoid
+-- Imports for haddock
+
+import qualified Data.Recursive.Bool as RB
+import qualified Data.Recursive.DualBool as RDB
+import qualified Data.Recursive.Set as RS
 
 -- $setup
 --
diff --git a/rec-def.cabal b/rec-def.cabal
--- a/rec-def.cabal
+++ b/rec-def.cabal
@@ -1,14 +1,14 @@
 cabal-version:      2.4
 name:               rec-def
-version:            0.1
-synopsis:           Recusively defined values
+version:            0.2
+synopsis:           Recursively defined values
 description:
    This library provides safe APIs that allow you to define and calculate
    values recursively, and still get a result out:
    .
-   > let s1 = rInsert 23 s2
-   >     s2 = rInsert 42 s1
-   > in getR s1
+   > let s1 = RS.insert 23 s2
+   >     s2 = RS.insert 42 s1
+   > in RS.get s1
    .
    will not loop, but rather produces the set @fromList [23,42]@
    .
@@ -16,18 +16,19 @@
    .
    * "Data.Recursive.Bool"
    * "Data.Recursive.Set"
+   * "Data.Recursive.Map"
    * "Data.Recursive.DualBool"
    .
-   More APIs (e.g. for 'Natural') can be added over time, as need and good
+   More APIs (e.g. for maps or 'Natural') can be added over time, as need and good
    use-cases arise.
 
    .
    For the (unsafe) building blocks to build such APIs, see
    .
-   * "Data.Recursive.R.Internal" for the wrapper that turns an IO-implemented
+   * "Data.Propagator.Purify" for the wrapper that turns an IO-implemented
      propagator into a pure data structure
-   * "Data.Recursive.Propagator.Naive" for a naive propagator implementation
-   * "Data.Recursive.Propagator.P2" for a smarter propagator implementation for
+   * "Data.Propagator.Naive" for a naive propagator implementation
+   * "Data.Propagator.P2" for a smarter propagator implementation for
      the two-point lattice, i.e. 'Bool'
    .
    The library is not (yet) focussed on performance, and uses a rather naive
@@ -56,13 +57,14 @@
     exposed-modules: Data.Recursive.Bool
     exposed-modules: Data.Recursive.DualBool
     exposed-modules: Data.Recursive.Set
+    exposed-modules: Data.Recursive.Map
+    exposed-modules: Data.Recursive.Internal
     exposed-modules: Data.POrder
     exposed-modules: System.IO.RecThunk
-    exposed-modules: Data.Recursive.R
-    exposed-modules: Data.Recursive.R.Internal
-    exposed-modules: Data.Recursive.Propagator.Naive
-    exposed-modules: Data.Recursive.Propagator.Class
-    exposed-modules: Data.Recursive.Propagator.P2
+    exposed-modules: Data.Propagator.Purify
+    exposed-modules: Data.Propagator.Naive
+    exposed-modules: Data.Propagator.Class
+    exposed-modules: Data.Propagator.P2
 
     build-depends:    base >= 4.9 && < 5
     build-depends:    containers >= 0.5.11 && < 0.7
@@ -74,6 +76,7 @@
     main-is:          doctests.hs
     default-language: Haskell2010
     ghc-options:      -threaded
+    hs-source-dirs:   tests
 
     build-depends:    rec-def
     build-depends:    base >= 4.9 && < 5
@@ -81,13 +84,24 @@
     build-depends:    QuickCheck
     build-depends:    template-haskell
 
+test-suite spaceleak
+    type:             exitcode-stdio-1.0
+    main-is:          spaceleak.hs
+    hs-source-dirs:   tests
+    default-language: Haskell2010
+    build-depends:    rec-def
+    build-depends:    base >= 4.9 && < 5
+    build-depends:    containers >= 0.5.11 && < 0.7
 
 test-suite dejafu
     type:             exitcode-stdio-1.0
     other-modules:    System.IO.RecThunk
-    other-modules:    Data.Recursive.Propagator.Naive
-    other-modules:    Data.Recursive.Propagator.P2
+    other-modules:    Data.POrder
+    other-modules:    Data.Propagator.Class
+    other-modules:    Data.Propagator.Naive
+    other-modules:    Data.Propagator.P2
     main-is:          dejafu.hs
+    hs-source-dirs:   tests .
     default-language: Haskell2010
     ghc-options:      -threaded
     cpp-options:      -DDEJAFU
@@ -97,7 +111,7 @@
     build-depends:    concurrency ^>= 1.11.0.2
     build-depends:    dejafu ^>= 2.4.0.3
     build-depends:    tasty
-    build-depends:    tasty-dejafu
+    build-depends:    tasty-dejafu ^>= 2.1.0.0
     build-depends:    random
 
 source-repository head
diff --git a/tests/dejafu.hs b/tests/dejafu.hs
new file mode 100644
--- /dev/null
+++ b/tests/dejafu.hs
@@ -0,0 +1,203 @@
+import Test.DejaFu
+import Control.Concurrent.Classy
+import Control.Concurrent.Classy.Async
+import qualified Data.Set as S
+import System.Random
+import Control.Monad
+import Test.Tasty
+import Test.Tasty.DejaFu
+
+import Data.Propagator.Naive
+import Data.Propagator.P2
+import System.IO.RecThunk
+
+t n = testAuto n
+
+tr n = testAutoWay (randomly (mkStdGen 0) 1000) defaultMemType n
+
+main = defaultMain $ testGroup "tests" $
+  [ t "prop 1" $ do
+        p1 <- newProp (S.singleton 1)
+        readProp p1
+
+  , t "prop 2" $ do
+        p1 <- newProp (S.singleton 1)
+        p2 <- newProp S.empty
+        lift1 (S.insert 3) p1 p2
+        mapConcurrently readProp [p1, p2]
+
+  , tr "prop 2 rec" $ withSetup (do
+        p1 <- newProp S.empty
+        p2 <- newProp S.empty
+        pure (p1, p2)) $ \(p1, p2) -> do
+        mapConcurrently id
+            [ lift1 (S.insert 3) p1 p2
+            , lift1 (S.insert 4) p2 p1
+            ]
+        mapConcurrently readProp [p1, p2]
+
+  , tr "prop 2 rec plus" $ withSetup (do
+        p1 <- newProp S.empty
+        p2 <- newProp S.empty
+        p3 <- newProp S.empty
+        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
+        mapConcurrently id
+            [ lift1 (S.insert 3) p1 p2
+            , lift1 (S.insert 4) p2 p1
+            ]
+        mapConcurrently id
+            [ readProp p1
+            , readProp p2
+            , lift1 (S.insert 5) p2 p3 >> readProp p3
+            ]
+
+
+  , tr "prop 3 rec" $ withSetup (do
+        p1 <- newProp S.empty
+        p2 <- newProp S.empty
+        p3 <- newProp S.empty
+        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
+        mapConcurrently id
+            [ lift1 (S.insert 3) p1 p2
+            , lift1 (S.insert 4) p2 p1
+            , lift1 (S.insert 5) p2 p3
+            ]
+        mapConcurrently readProp [p1, p2, p3]
+
+  , tr "prop 3 rec variant" $ withSetup (do
+        p1 <- newProp S.empty
+        p2 <- newProp S.empty
+        p3 <- newProp S.empty
+        pure (p1, p2, p3)) $ \(p1, p2, p3) -> do
+        mapConcurrently id
+            [ lift1 (S.insert 4) p1 p2
+            , lift1 (S.insert 5) p2 p3
+            , lift2 (S.union) p2 p3 p1
+            ]
+        mapConcurrently readProp [p1, p2, p3]
+
+  , tr "prop 4 rec" $ withSetup (do
+        p1 <- newProp S.empty
+        p2 <- newProp S.empty
+        p3 <- newProp S.empty
+        p4 <- newProp S.empty
+        pure (p1, p2, p3, p4)) $ \(p1, p2, p3, p4) -> do
+        mapConcurrently id
+            [ lift1 (S.insert 4) p1 p2
+            , lift2 (S.union) p1 p2 p3
+            , liftList (S.unions) [p1,p2,p3] p4
+            , lift1 (S.insert 5) p4 p1
+            ]
+        mapConcurrently readProp [p1, p2, p3, p4]
+  , t "thunk 1" $ do
+        obs1 <- newIORef 0
+        t1 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            pure []
+        force t1
+        readIORef obs1
+  , t "thunk 1 rec" $ do
+        obs1 <- newIORef 0
+        t1ref <- newIORef undefined
+        t1 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            t1 <- readIORef t1ref
+            pure [t1]
+        writeIORef t1ref t1
+        force t1
+        readIORef obs1
+  , t "thunk 2 rec 12" $ do
+        obs1 <- newIORef 0
+        obs2 <- newIORef 0
+        t2ref <- newIORef undefined
+        t1 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            t2 <- readIORef t2ref
+            pure [t2]
+        t2 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            pure [t1]
+        writeIORef t2ref t2
+        mapConcurrently id
+            [ force t1 >> mapM readIORef [obs1, obs2]
+            , force t2 >> mapM readIORef [obs1, obs2]
+            ]
+  , tr "thunk 2 rec 112" $ do
+        obs1 <- newIORef 0
+        obs2 <- newIORef 0
+        t2ref <- newIORef undefined
+        t1 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            t2 <- readIORef t2ref
+            pure [t2]
+        t2 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            pure [t1]
+        writeIORef t2ref t2
+        mapConcurrently id
+            [ force t1 >> mapM readIORef [obs1, obs2]
+            , force t1 >> mapM readIORef [obs1, obs2]
+            , force t2 >> mapM readIORef [obs1, obs2]
+            ]
+  , tr "thunk 2 all-rec 112" $ do
+        obs1 <- newIORef 0
+        obs2 <- newIORef 0
+        t1ref <- newIORef undefined
+        t2ref <- newIORef undefined
+        t1 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            t1 <- readIORef t1ref
+            t2 <- readIORef t2ref
+            pure [t2,t1]
+        writeIORef t1ref t1
+        t2 <- thunk $ do
+            atomicModifyIORef' obs1 (\x -> (succ x, ()))
+            t2 <- readIORef t2ref
+            pure [t1,t2]
+        writeIORef t2ref t2
+        mapConcurrently id
+            [ force t1 >> mapM readIORef [obs1, obs2]
+            , force t1 >> mapM readIORef [obs1, obs2]
+            , force t2 >> mapM readIORef [obs1, obs2]
+            ]
+  , t "P2 1" $ do
+    p1 <- newP2
+    False <- isTop p1
+    setTop p1
+    True <- isTop p1
+    pure ()
+  , t "P2 2" $ do
+    p1 <- newP2
+    p2 <- newP2
+    mapConcurrently id
+        [ do
+            False <- isTop p1
+            setTop p1
+            True <- isTop p1
+            pure ()
+        , do
+            False <- isTop p2
+            p1 `implies` p2
+        ]
+    True <- isTop p2
+    pure ()
+  , t "P2 2 rec bottom" $ do
+    p1 <- newP2
+    p2 <- newP2
+    mapConcurrently id
+        [  p1 `implies` p2
+        ,  p2 `implies` p1
+        ]
+    [False, False] <- mapM isTop [p1,p2]
+    pure ()
+  , t "P2 2 rec top" $ do
+    p1 <- newP2
+    p2 <- newP2
+    mapConcurrently id
+        [  p1 `implies` p2
+        ,  p2 `implies` p1
+        , setTop p1
+        ]
+    [True, True] <- mapM isTop [p1,p2]
+    pure ()
+  ]
diff --git a/tests/doctests.hs b/tests/doctests.hs
new file mode 100644
--- /dev/null
+++ b/tests/doctests.hs
@@ -0,0 +1,8 @@
+import Test.DocTest
+main = do
+    -- Why do I have to call them separately?
+    doctest ["--fast", "-package=QuickCheck","Data/Recursive/Bool.hs"]
+    doctest ["--fast", "-package=QuickCheck","Data/Recursive/DualBool.hs"]
+    doctest ["--fast", "-package=QuickCheck","Data/Recursive/Set.hs"]
+    doctest ["--fast", "-package=QuickCheck","Data/Recursive/Map.hs"]
+    doctest ["--fast", "-package=QuickCheck","Data/Recursive/Examples.hs"]
diff --git a/tests/spaceleak.hs b/tests/spaceleak.hs
new file mode 100644
--- /dev/null
+++ b/tests/spaceleak.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NumericUnderscores #-}
+
+{-|
+This test checks that resolved cells do no longer hold on to references to
+dependent cells, to avoid space leaks, especially with the “constant global”
+cells like 'RS.empty'.
+-}
+
+module Main where
+
+import qualified Data.Set as S
+import qualified Data.Recursive.Set as RS
+import Data.Recursive.Internal
+import Data.Propagator.Purify
+
+import Data.IORef
+import System.Mem.Weak
+import System.Mem
+import System.Exit
+import System.Environment
+import Control.Concurrent
+
+main = do
+    n <- length <$> getArgs
+
+    putStrLn "Test 1: Normal GC (sanity check)"
+    gc <- newIORef False
+    let x = 1000_000_001 + n
+    addFinalizer x $ do
+        putStrLn "Finalizer running"
+        writeIORef gc True
+    let s = RS.insert x s
+    print (RS.get s)
+
+    putStrLn "Running GC"
+    performMajorGC
+    threadDelay 1_000_000
+
+    readIORef gc >>= \case
+        True -> putStrLn "GC seems to be working"
+        False -> putStrLn "This really ought to work" >> exitFailure
+
+
+    putStrLn "Test 2: Dependency on RS.empty"
+    gc <- newIORef False
+    let x = 1000_000_002 + n
+    addFinalizer x $ do
+        putStrLn "Finalizer running"
+        writeIORef gc True
+    let s = RS.insert x RS.empty
+    print (RS.get s)
+
+    putStrLn "Running GC"
+    performMajorGC
+    threadDelay 1_000_000
+
+    readIORef gc >>= \case
+        True -> putStrLn "Good!"
+        False -> putStrLn "We got a leak" >> exitFailure
+
+    putStrLn "Test 3: Dependency on constant set"
+    gc <- newIORef False
+    let x0 = 1000_000_003 + n
+    let s' = RS.mk (S.singleton x0)
+    let x1 = 1000_000_004 + n
+    addFinalizer x1 $ do
+        putStrLn "Finalizer running"
+        writeIORef gc True
+    let s = RS.insert x1 s'
+    print (RS.get s)
+
+    putStrLn "Running GC"
+    performMajorGC
+    threadDelay 1_000_000
+
+    readIORef gc >>= \case
+        True -> putStrLn "Good!"
+        False -> putStrLn "We got a leak" >> exitFailure
+
+    putStrLn "Test 4: Dependency on recursive set"
+    gc <- newIORef False
+    let x0 = 1000_000_005 + n
+    let sr = RS.insert x0 sr
+    let x1 = 1000_000_007 + n
+    addFinalizer x1 $ do
+        putStrLn "Finalizer running"
+        writeIORef gc True
+    let s = RS.insert x1 sr
+    print (RS.get s)
+
+    putStrLn "Running GC"
+    performMajorGC
+    threadDelay 1_000_000
+
+    readIORef gc >>= \case
+        True -> putStrLn "Good!"
+        False -> putStrLn "We got a leak" >> exitFailure
+
+    -- This is needed, else RS.empty itself is GC’ed
+    putStrLn "Keeping a few things alive"
+    print (RS.get s')
+    print (RS.get sr)
+    print (RS.get RS.empty :: S.Set Int)
+