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 RBool type comes with functions that look quite like their ordinary counterparts acting on Bool.

>>> import Data.Recursive.Bool (RBool)
>>> import qualified Data.Recursive.Bool as RB

>>> :t RB.true
RB.true :: RBool
>>> :t RB.false
RB.false :: RBool
>>> :t (RB.||)
(RB.||) :: RBool -> RBool -> RBool
>>> :t (RB.&&)
(RB.&&) :: RBool -> RBool -> RBool
>>> RB.get RB.true
True
>>> RB.get RB.false
False
>>> RB.get (RB.false RB.&& RB.true)
False
>>> RB.get (RB.true RB.&& RB.true)
True
>>> RB.get (RB.or [RB.true,  RB.false, RB.true])
True

So far so good, lets see what happens when we try something recursive:

>>> let x = RB.or [y]; y = RB.and [x, RB.false] in RB.get x
False
>>> let x = RB.or [y]; y = RB.or [x, RB.false] in RB.get x
False
>>> let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x
True
>>> let x = RB.or [y]; y = RB.or [x] in RB.get 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 RDualBool. The module Data.Recursive.DualBool exports all the functions for that type too. We can run the same equations, and get different answers:

>>> import Data.Recursive.DualBool (RDualBool)
>>> import qualified Data.Recursive.DualBool as RDB

>>> let x = RDB.or [y]; y = RDB.and [x, RDB.false] in RDB.get x
False
>>> let x = RDB.or [y]; y = RDB.or [x, RDB.false] in RDB.get x
True
>>> let x = RDB.or [y]; y = RDB.or [x, RDB.true] in RDB.get x
True
>>> let x = RDB.or [y]; y = RDB.or [x] in RDB.get x
True

The negation function is also available, and goes from can-be-true to must-be-true and back:

>>> :t RB.not
RB.not :: RDualBool -> RBool
>>> :t RDB.not
RDB.not :: RBool -> RDualBool

This allows us to mix the different types in the same computation:

>>> :{
  let x = RB.not y RB.|| RB.not z
      y = RDB.not x RDB.&& z
      z = RDB.true
  in (RB.get x, RDB.get y, RDB.get z)
 :}
(False,True,True)

>>> :{
  let x = RB.not y RB.|| RB.not z
      y = RDB.not x RDB.&& z
      z = RDB.false
  in (RB.get x, RDB.get y, RDB.get z)
 :}
(True,False,False)

Sets

We do not have to stop with booleans, and can define similar APIs for other data stuctures, e.g. sets:

>>> import qualified Data.Recursive.Set as RS

Again we can describe sets recursively, using the monotone functions empty, insert and union

>>> :{
  let s1 = RS.insert 23 s2
      s2 = RS.insert 42 s1
  in RS.get s1
 :}
fromList [23,42]

Here is a slightly larger example, where we can 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 Set, it now works even if the graph has cycles:

>>> :{
   reachable :: M.Map Int [Int] -> M.Map Int (S.Set Int)
   reachable g = fmap RS.get sets
     where
       sets :: M.Map Int (RS.RSet Int)
       sets = M.mapWithKey (\v vs -> RS.insert v (RS.unions [ sets ! v' | v' <- vs ])) g
 :}

>>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]
>>> 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 get) while you are building the graph:

>>> :{
    withTimeout $
      let x = RB.and [x, if RB.get y then z else RB.true]
          y = RB.and [x, RB.true]
          z = RB.false
      in RB.get y
    :}
*** Exception: timed out

Similarly, you have to make sure you recurse through one of these functions; let x = x still does not work:

>>> withTimeout $ let x = x :: RBool in RB.get x
*** Exception: timed out
>>> withTimeout $ let x = x RB.&& x in RB.get x
False

We belive that the APIs provided here are still “pure”: evaluation order does not affect the results, and you can replace equals with equals, in the sense that

let s = RS.insert 42 s in s

is the same as

let s = RS.insert 42 s in RS.insert 42 s

However, the the following two expressions are not equivalent:

>>> withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s
[42]
>>> withTimeout $ S.toList $ let s () = RS.insert 42 (s ()) in RS.get (s ())
*** Exception: timed out

It is debatable if that is a problem.