rec-def (empty) → 0.1
raw patch · 18 files changed
+1641/−0 lines, 18 filesdep +QuickCheckdep +basedep +concurrency
Dependencies added: QuickCheck, base, concurrency, containers, dejafu, doctest, random, rec-def, tasty, tasty-dejafu, template-haskell
Files
- CHANGELOG.md +5/−0
- Data/POrder.hs +59/−0
- Data/Recursive/Bool.hs +101/−0
- Data/Recursive/DualBool.hs +83/−0
- Data/Recursive/Examples.hs +199/−0
- Data/Recursive/Propagator/Class.hs +55/−0
- Data/Recursive/Propagator/Naive.hs +110/−0
- Data/Recursive/Propagator/P2.hs +101/−0
- Data/Recursive/R.hs +8/−0
- Data/Recursive/R/Internal.hs +113/−0
- Data/Recursive/Set.hs +90/−0
- LICENSE +26/−0
- README.md +28/−0
- System/IO/RecThunk.hs +153/−0
- dejafu.hs +203/−0
- doctests.hs +2/−0
- examples.hs +199/−0
- rec-def.cabal +106/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for rec-def++## 0.1 -- 2022-09-03++* First version. Released on an unsuspecting world.
+ Data/POrder.hs view
@@ -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
+ Data/Recursive/Bool.hs view
@@ -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
+ Data/Recursive/DualBool.hs view
@@ -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
+ Data/Recursive/Examples.hs view
@@ -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)+-- :}++
+ Data/Recursive/Propagator/Class.hs view
@@ -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)
+ Data/Recursive/Propagator/Naive.hs view
@@ -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
+ Data/Recursive/Propagator/P2.hs view
@@ -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_
+ Data/Recursive/R.hs view
@@ -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
+ Data/Recursive/R/Internal.hs view
@@ -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
+ Data/Recursive/Set.hs view
@@ -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
+ LICENSE view
@@ -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.
+ README.md view
@@ -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.
+ System/IO/RecThunk.hs view
@@ -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
+ dejafu.hs view
@@ -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 ()+ ]
+ doctests.hs view
@@ -0,0 +1,2 @@+import Test.DocTest+main = doctest ["--fast", "-package=QuickCheck", "Data/"]
+ examples.hs view
@@ -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)+-- :}++
+ rec-def.cabal view
@@ -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+