Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

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:

`>>>`

*** Exception: timed out`withTimeout $ let x = y || False; y = x && False in x`

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`

`>>>`

RB.true :: RBool`:t RB.true`

`>>>`

RB.false :: RBool`:t RB.false`

`>>>`

(RB.||) :: RBool -> RBool -> RBool`:t (RB.||)`

`>>>`

(RB.&&) :: RBool -> RBool -> RBool`:t (RB.&&)`

`>>>`

True`RB.get RB.true`

`>>>`

False`RB.get RB.false`

`>>>`

False`RB.get (RB.false RB.&& RB.true)`

`>>>`

True`RB.get (RB.true RB.&& RB.true)`

`>>>`

True`RB.get (RB.or [RB.true, RB.false, RB.true])`

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

`>>>`

False`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`

`>>>`

True`let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x`

`>>>`

False`let x = RB.or [y]; y = RB.or [x] in RB.get x`

## 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`

`>>>`

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

`>>>`

True`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`

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

`>>>`

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

`>>>`

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

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,[])]`

`>>>`

fromList [1,2,3]`reachable graph M.! 1`

`>>>`

fromList [3]`reachable graph M.! 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:

`>>>`

*** Exception: timed out`withTimeout $ let x = x :: RBool in RB.get x`

`>>>`

False`withTimeout $ let x = x RB.&& x in RB.get x`

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:

`>>>`

[42]`withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s`

`>>>`

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

It is debatable if that is a problem.