{-# OPTIONS_GHC -Wno-unused-imports #-}

{-|

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 'Data.Recursive.Bool.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 'RS.empty',
'RS.insert' and 'RS.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
'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 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 'RB.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.

-}
module Data.Recursive.Examples () where

-- Imports for haddock

import qualified Data.Recursive.Bool as RB
import qualified Data.Recursive.DualBool as RDB
import qualified Data.Recursive.Set as RS

-- $setup
--
-- >>> 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)
-- :}