diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for rec-def
+
+## 0.1 -- 2022-09-03
+
+* First version. Released on an unsuspecting world.
diff --git a/Data/POrder.hs b/Data/POrder.hs
new file mode 100644
--- /dev/null
+++ b/Data/POrder.hs
@@ -0,0 +1,59 @@
+-- | This module provides the 'POrder' and related classes
+module Data.POrder where
+
+import System.IO.Unsafe
+import Control.Monad.ST
+import Data.Monoid
+import Data.Coerce
+import qualified Data.Set as S
+import Numeric.Natural
+
+-- | 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.
+-- 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
+
+-- | A class indicating that the type @a@ is partially ordered and has a bottom
+-- element.
+class POrder a => Bottom a where bottom :: a
+
+-- | A class indicating that the type @a@ is partially ordered and has a top
+-- element.
+class POrder a => Top a where top :: a
+
+-- | The dual order
+instance POrder a => POrder (Dual a)
+
+-- | Bottom is the 'top' of @a@
+instance Top a => Bottom (Dual a) where bottom = Dual top
+
+-- Annoyingly, we have to give all instances here, to avoid orphans
+
+-- | Arbitrary using the @False < True@ order
+instance POrder Bool
+
+-- | Bottom is 'False'
+instance Bottom Bool where bottom = False
+
+-- | Top is 'True'
+instance Top Bool where top = True
+
+-- | Ordered by 'S.subsetOf'
+instance Eq a => POrder (S.Set a)
+
+-- | Bottom is 'S.empty'
+instance Eq a => Bottom (S.Set a) where bottom = S.empty
+
+-- | Ordered by '(<=)f'
+instance POrder Natural
+
+-- | 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)
+
+-- | Bottom is 'Nothing'
+instance POrder a => Bottom (Maybe a) where bottom = Nothing
diff --git a/Data/Recursive/Bool.hs b/Data/Recursive/Bool.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Bool.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE TypeApplications #-}
+
+{- | The type @R Bool@ is ike 'Bool', but allows recursive definitions:
+
+>>> :{
+  let x = rTrue
+      y = x &&& z
+      z = y ||| rFalse
+  in getR x
+:}
+True
+
+
+This finds the least solution, i.e. prefers 'False' over 'True':
+
+>>> :{
+  let x = x &&& y
+      y = y &&& x
+  in (getR x, getR y)
+:}
+(False,False)
+
+Use @R (Dual Bool)@ from "Data.Recursive.DualBool" if you want the greatest solution.
+
+-}
+module Data.Recursive.Bool
+  ( R
+  , getR
+  , 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
+
+-- $setup
+-- >>> :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 (||)
+
+rand :: [R Bool] -> R Bool
+rand = defRList $ liftList and
+
+ror :: [R Bool] -> R Bool
+ror = defRList $ liftList or
+
+rnot :: R (Dual Bool) -> R Bool
+rnot = defR1 $ lift1 $ coerce not
+
+-}
+
+-- | prop> getR (r1 &&& r2) === (getR r1 && getR r2)
+(&&&) :: R Bool -> R Bool -> R Bool
+(&&&) = defR2 $ coerce $ \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
+    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
+  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 ->
+    mapM_ @[] (`implies` p) ps
+
+-- | prop> getR (rnot r1) === not (getRDual r1)
+rnot :: R (Dual Bool) -> R Bool
+rnot = defR1 $ coerce $ \p1 p -> do
+    implies p1 p
diff --git a/Data/Recursive/DualBool.hs b/Data/Recursive/DualBool.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/DualBool.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeApplications #-}
+
+{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:
+
+>>> :{
+  let x = rTrue
+      y = x &&& z
+      z = y ||| rFalse
+  in getRDual x
+:}
+True
+
+
+This finds the greatest solution, i.e. prefers 'True' over 'False':
+
+>>> :{
+  let x = x &&& y
+      y = y &&& x
+  in (getRDual x, getRDual y)
+:}
+(True,True)
+
+Use @R Bool@ from "Data.Recursive.Bool" if you want the least solution.
+
+-}
+module Data.Recursive.DualBool
+  ( R
+  , getRDual
+  , 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
+
+-- $setup
+-- >>> :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> getRDual rTrue == True
+rTrue :: R (Dual Bool)
+rTrue = mkR (Dual True)
+
+-- | prop> getRDual rFalse == False
+rFalse :: R (Dual Bool)
+rFalse = mkR (Dual False)
+
+-- | 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> getRDual (r1 &&& r2) === (getRDual r1 && getRDual r2)
+(&&&) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)
+(&&&) = defR2 $ coerce $ \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
+  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> getRDual (rnot r1) === not (getR r1)
+rnot :: R Bool -> R (Dual Bool)
+rnot = defR1 $ coerce $ \p1 p -> do
+    implies p1 p
diff --git a/Data/Recursive/Examples.hs b/Data/Recursive/Examples.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Examples.hs
@@ -0,0 +1,199 @@
+{-|
+
+This file contains a few examples of using the @rec-def@ library. There is no
+need to actually use this module.
+
+= A @rec-def@ tutorial
+
+Imagine you are trying to calculate a boolean value, but your calculation is
+happens to be recursive. Just writing down the equations does not work:
+
+>>> withTimeout $ let x = y || False; y = x && False in x
+*** Exception: timed out
+
+This is unfortunate, isn’t it?
+
+== A @Bool@ with recursive equations
+
+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
+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
+True
+>>> getR rFalse
+False
+>>> getR (rFalse &&& rTrue)
+False
+>>> getR (rTrue &&& rTrue)
+True
+>>> getR (ror [rTrue,  rFalse, rTrue])
+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
+False
+>>> let x = ror [y]; y = ror [x, rFalse] in getR x
+False
+>>> let x = ror [y]; y = ror [x, rTrue] in getR x
+True
+>>> let x = ror [y]; y = ror [x] in getR x
+False
+
+== Least or greatest solution
+
+The last equation is interesting: We essentially say that @x@ is @True@ if @y@ is
+@True@, and @y@ is @True@ if @x@ is @True@. This has two solutions, we can either set
+both to @True@ and both to @False@.
+
+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:
+
+>>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x
+False
+>>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x
+True
+>>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x
+True
+>>> let x = DB.ror [y]; y = DB.ror [x] in getRDual 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)
+
+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)
+ :}
+(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)
+ :}
+(True,False,False)
+
+== Sets
+
+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'
+
+>>> :{
+  let s1 = rInsert 23 s2
+      s2 = rInsert 42 s1
+  in getR s1
+ :}
+fromList [23,42]
+
+Here is a slightly larger example, where we can 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
+     where
+       sets :: M.Map Int (R (S.Set Int))
+       sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g
+ :}
+
+>>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]
+>>> reachable graph M.! 1
+fromList [1,2,3]
+>>> reachable graph M.! 3
+fromList [3]
+
+== Caveats
+
+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:
+
+>>> :{
+    withTimeout $
+      let x = rand [x, if getR y then z else rTrue]
+          y = rand [x, rTrue]
+          z = rFalse
+      in getR 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
+*** Exception: timed out
+>>> withTimeout $ let x = x &&& x in getR 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
+
+is the same as
+
+> let s = rInsert 42 s in rInsert 42 s
+
+However, the the following two expressions are not equivalent:
+
+>>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s
+[42]
+>>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())
+*** Exception: timed out
+
+It is debatable if that is a problem.
+
+-}
+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
+
+-- $setup
+--
+-- >>> import System.Timeout
+-- >>> import Control.Exception
+-- >>> import Data.Maybe
+-- >>> import Data.Map as M
+-- >>> import qualified Data.Set as S
+-- >>>
+-- >>> :{
+-- let withTimeout :: Show a => a -> IO a
+--     withTimeout a =
+--       fromMaybe (errorWithoutStackTrace "timed out") <$>
+--          timeout 100000 (length (show a) `seq` evaluate a)
+-- :}
+
+
diff --git a/Data/Recursive/Propagator/Class.hs b/Data/Recursive/Propagator/Class.hs
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Propagator/Class.hs
@@ -0,0 +1,55 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Propagator/Naive.hs
@@ -0,0 +1,110 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Propagator/P2.hs
@@ -0,0 +1,101 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/R.hs
@@ -0,0 +1,8 @@
+-- |
+-- 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
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/R/Internal.hs
@@ -0,0 +1,113 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Data/Recursive/Set.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE TypeFamilies #-}
+{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:
+
+>>> :{
+  let s1 = rInsert 23 s2
+      s2 = rInsert 42 s1
+  in getR s1
+ :}
+fromList [23,42]
+
+-}
+module Data.Recursive.Set
+  ( R
+  , mkR
+  , getR
+  , 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
+
+-- $setup
+-- >>> :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
+
+-- | prop> getR rEmpty === S.empty
+rEmpty :: Eq a => R (S.Set a)
+rEmpty = mkR S.empty
+
+-- | 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> 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> \(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> 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> 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> 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> 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
+    let update = do
+            s <- readProp ps
+            when (S.member x s) $ coerce 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
+    let update = do
+            s <- readProp ps
+            when (S.member x s) $ coerce 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
+    let update = do
+            s1 <- readProp ps1
+            s2 <- readProp ps2
+            unless (S.disjoint s1 s2) $ coerce setTop pb
+    watchProp ps1 update
+    watchProp ps2 update
+    update
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2022, Joachim Breitner
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,28 @@
+rec-def - Pure recursive definition
+===================================
+
+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
+     :}
+    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`.
+
+Related work
+------------
+
+* Edward Kmett's [`Data.Propagator.Prop` module](https://github.com/ekmett/propagators/blob/master/src/Data/Propagator/Prop.hs) achieves something similar, and allows to construct more the graphs more flexibly, but requires a stricter phase control akin to `runST`.
+
+* Jeannin, Kozen and Silva’s work on [“CoCaml: Functional Programming with
+Regular Coinductive
+Types”](https://www.cs.cornell.edu/~kozen/Papers/CoCaml.pdf) in Ocaml even goes
+a step further and not only allow the recursive definitions to be written down
+as here, but even allows functions _consume_ regular recursive values, and
+still produces something that can be solved.
diff --git a/System/IO/RecThunk.hs b/System/IO/RecThunk.hs
new file mode 100644
--- /dev/null
+++ b/System/IO/RecThunk.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE CPP #-}
+
+{-|
+
+The 'Thunk' API provides a way to defer potentially recursive computations:
+
+* '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
+* '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.
+
+The implementation is hopefully thread safe: Even if multiple threads force or
+kick related thunks, all actions are still run at most once, and all calls to
+force terminate (no deadlock).
+
+>>> :set -XRecursiveDo
+>>> :{
+  mdo t1 <- thunk $ putStrLn "Hello" >> pure [t1, t2]
+      t2 <- thunk $ putStrLn "World" >> pure [t1, t2]
+      putStrLn "Nothing happened so far, but now:"
+      force t1
+      putStrLn "No more will happen now:"
+      force t1
+      putStrLn "That's it"
+:}
+Nothing happened so far, but now:
+Hello
+World
+No more will happen now:
+That's it
+
+-}
+module System.IO.RecThunk
+    ( Thunk
+    , thunk
+    , doneThunk
+    , force
+    )
+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 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)
+
+#else
+
+#define Ctxt
+#define Thunk_  Thunk
+#define ResolvingState_  ResolvingState
+#define KickedThunk_  KickedThunk
+#define ThreadId_  ThreadId
+#define IORef_ IORef
+#define MVar_  MVar
+#define M      IO
+
+import Control.Concurrent.MVar
+import Control.Concurrent
+import Data.IORef
+
+#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
+-- | A 'Thunk' that is being evaluated
+data KickedThunk_ = KickedThunk (MVar_ [KickedThunk_]) (MVar_ ResolvingState_)
+
+-- | Create a new 'Thunk' from an 'IO' action.
+--
+-- The 'IO' action may return other thunks that should be forced together
+-- whenver this thunk is forced (in arbitrary order)
+thunk :: Ctxt M [Thunk_] -> M Thunk_
+thunk act = Thunk <$> newMVar (Left act)
+
+-- | A Thunk that that already is done.
+--
+-- Equivalent to @do {t <- thunk (pure []); force t; pure t }@
+doneThunk :: Ctxt M Thunk_
+doneThunk = do
+    mv_ts <- newMVar []
+    mv_s <- newMVar Done
+    Thunk <$> newMVar (Right (KickedThunk mv_ts mv_s))
+
+-- Recursively explores the thunk, and kicks the execution
+-- May return before before execution is done (if started by another thread)
+kick :: Ctxt Thunk_ -> M KickedThunk_
+kick (Thunk t) = takeMVar t >>= \case
+    Left act -> do
+        mv_thunks <- newEmptyMVar
+        mv_state <- newMVar NotStarted
+        let kt = KickedThunk mv_thunks mv_state
+        putMVar t (Right kt)
+
+        ts <- act
+        kts <- mapM kick ts
+        putMVar mv_thunks kts
+        pure kt
+
+    -- Thread was already kicked, nothing to do
+    Right kt -> do
+        putMVar t (Right kt)
+        pure kt
+
+wait :: Ctxt KickedThunk_ -> M ()
+wait (KickedThunk mv_deps mv_s) = do
+    my_id <- myThreadId
+    s <- takeMVar mv_s
+    case s of
+        -- Thunk and all dependences are done
+        Done -> putMVar mv_s s
+        -- Thunk is being processed by a higher priority thread, so simply wait
+        ProcessedBy other_id done_mv | other_id < my_id -> do
+            putMVar mv_s s
+            readMVar done_mv
+        -- Thunk is already being processed by this thread, ignore
+        ProcessedBy other_id _done_mv | other_id == my_id -> do
+            putMVar mv_s s
+            pure ()
+        -- Thunk is not yet processed, or processed by a lower priority thread, so process now
+        _ -> do
+            done_mv <- newEmptyMVar
+            putMVar mv_s (ProcessedBy my_id done_mv)
+            ts <- readMVar mv_deps
+            mapM_ wait ts
+            -- Mark kicked thunk as done
+            _ <- swapMVar mv_s Done
+            -- Wake up waiting threads
+            putMVar done_mv ()
+
+-- | Force the execution of the thunk. If it has been forced already, it will
+-- do nothing. Else it will run the action passed to 'thunk', force thunks
+-- returned by that action, and not return until all of them are forced.
+force :: Ctxt Thunk_ -> M ()
+force t = do
+    rt <- kick t
+    wait rt
diff --git a/dejafu.hs b/dejafu.hs
new file mode 100644
--- /dev/null
+++ b/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.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
new file mode 100644
--- /dev/null
+++ b/doctests.hs
@@ -0,0 +1,2 @@
+import Test.DocTest
+main = doctest ["--fast", "-package=QuickCheck", "Data/"]
diff --git a/examples.hs b/examples.hs
new file mode 100644
--- /dev/null
+++ b/examples.hs
@@ -0,0 +1,199 @@
+{-|
+
+This file contains a few examples of using the @rec-def@ library. There is no
+need to actually use this module.
+
+= A @rec-def@ tutorial
+
+Imagine you are trying to calculate a boolean value, but your calculation is
+happens to be recursive. Just writing down the equations does not work:
+
+>>> withTimeout $ let x = y || False; y = x && False in x
+*** Exception: timed out
+
+This is unfortunate, isn’t it?
+
+== A @Bool@ with recursive equations
+
+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
+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
+True
+>>> getR rFalse
+False
+>>> getR (rFalse &&& rTrue)
+False
+>>> getR (rTrue &&& rTrue)
+True
+>>> getR (ror [rTrue,  rFalse, rTrue])
+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
+False
+>>> let x = ror [y]; y = ror [x, rFalse] in getR x
+False
+>>> let x = ror [y]; y = ror [x, rTrue] in getR x
+True
+>>> let x = ror [y]; y = ror [x] in getR x
+False
+
+== Least or greatest solution
+
+The last equation is interesting: We essentially say that @x@ is @True@ if @y@ is
+@True@, and @y@ is @True@ if @x@ is @True@. This has two solutions, we can either set
+both to @True@ and both to @False@.
+
+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:
+
+>>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x
+False
+>>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x
+True
+>>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x
+True
+>>> let x = DB.ror [y]; y = DB.ror [x] in getRDual 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)
+
+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)
+ :}
+(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)
+ :}
+(True,False,False)
+
+== Sets
+
+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'
+
+>>> :{
+  let s1 = rInsert 23 s2
+      s2 = rInsert 42 s1
+  in getR s1
+ :}
+fromList [23,42]
+
+Here is a slightly larger example, where we can 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
+     where
+       sets :: M.Map Int (R (S.Set Int))
+       sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g
+ :}
+
+>>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]
+>>> reachable graph M.! 1
+fromList [1,2,3]
+>>> reachable graph M.! 3
+fromList [3]
+
+== Caveats
+
+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:
+
+>>> :{
+    withTimeout $
+      let x = rand [x, if getR y then z else rTrue]
+          y = rand [x, rTrue]
+          z = rFalse
+      in getR 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
+*** Exception: timed out
+>>> withTimeout $ let x = x &&& x in getR 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
+
+is the same as
+
+> let s = rInsert 42 s in rInsert 42 s
+
+However, the the following two expressions are not equivalent:
+
+>>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s
+[42]
+>>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())
+*** Exception: timed out
+
+It is debatable if that is a problem.
+
+-}
+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
+
+-- $setup
+--
+-- >>> import System.Timeout
+-- >>> import Control.Exception
+-- >>> import Data.Maybe
+-- >>> import Data.Map as M
+-- >>> import qualified Data.Set as S
+-- >>>
+-- >>> :{
+-- let withTimeout :: Show a => a -> IO a
+--     withTimeout a =
+--       fromMaybe (errorWithoutStackTrace "timed out") <$>
+--          timeout 100000 (length (show a) `seq` evaluate a)
+-- :}
+
+
diff --git a/rec-def.cabal b/rec-def.cabal
new file mode 100644
--- /dev/null
+++ b/rec-def.cabal
@@ -0,0 +1,106 @@
+cabal-version:      2.4
+name:               rec-def
+version:            0.1
+synopsis:           Recusively 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
+   .
+   will not loop, but rather produces the set @fromList [23,42]@
+   .
+   See "Data.Recursive.Examples" for more examples, or just browse the modules
+   .
+   * "Data.Recursive.Bool"
+   * "Data.Recursive.Set"
+   * "Data.Recursive.DualBool"
+   .
+   More APIs (e.g. for '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
+     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
+     the two-point lattice, i.e. 'Bool'
+   .
+   The library is not (yet) focussed on performance, and uses a rather naive
+   propagator implementation. Expect this to be slow if you have large graphs.
+   This may be improved in the future (e.g. by propagating only deltas, and
+   accumulating deltas before applying a function), but for now the focus is on
+   foremost providing this capability in the first place and getting the
+   user-facing API right.
+
+homepage:           https://github.com/nomeata/haskell-rec-def
+bug-reports:        https://github.com/nomeata/haskell-rec-def/issues/new
+license:            BSD-2-Clause
+license-file:       LICENSE
+author:             Joachim Breitner
+maintainer:         mail@joachim-breitner.de
+copyright:          2022 Joachim Breitner
+category:           Data
+extra-source-files:
+    CHANGELOG.md
+    README.md
+    examples.hs
+tested-with: GHC==9.2.1, GHC==9.0.2, GHC==8.10.7, GHC==8.8.4, GHC==8.6.5, GHC==8.4.4
+
+library
+    exposed-modules: Data.Recursive.Examples
+    exposed-modules: Data.Recursive.Bool
+    exposed-modules: Data.Recursive.DualBool
+    exposed-modules: Data.Recursive.Set
+    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
+
+    build-depends:    base >= 4.9 && < 5
+    build-depends:    containers >= 0.5.11 && < 0.7
+
+    default-language: Haskell2010
+
+test-suite doctest
+    type:             exitcode-stdio-1.0
+    main-is:          doctests.hs
+    default-language: Haskell2010
+    ghc-options:      -threaded
+
+    build-depends:    rec-def
+    build-depends:    base >= 4.9 && < 5
+    build-depends:    doctest ^>= 0.18.2
+    build-depends:    QuickCheck
+    build-depends:    template-haskell
+
+
+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
+    main-is:          dejafu.hs
+    default-language: Haskell2010
+    ghc-options:      -threaded
+    cpp-options:      -DDEJAFU
+
+    build-depends:    base >= 4.9 && < 5
+    build-depends:    containers >= 0.5.11 && < 0.7
+    build-depends:    concurrency ^>= 1.11.0.2
+    build-depends:    dejafu ^>= 2.4.0.3
+    build-depends:    tasty
+    build-depends:    tasty-dejafu
+    build-depends:    random
+
+source-repository head
+    type:     git
+    location: git://github.com/nomeata/haskell-rec-def
+