Solving cyclic boolean implications with pure code and laziness

Show and Tell
#21

I’ve just noticed that you can do many of the things you advertise also with the lattices package, e.g.:

import Algebra.Lattice
import qualified Data.Set as S
import qualified Data.Map as M

transitive g = 
  lfpFrom g $ \sets -> 
    M.mapWithKey 
      (\v vs -> S.insert v (S.unions [ sets M.! v' | v' <- S.toList vs ]))
      sets

main = print $ transitive 
  $ M.map S.fromList $ M.fromList [(1,[2,3]),(2,[1,3]),(3,[])]

I guess your package has the advantage of allowing more natural code. But it requires using custom functions like rInsert and the R type wrapper, so I’m not sure which is easier to use.

I guess performance is another advantage of your approach.

3 Likes
#22

Thanks for the pointer, I was not aware of that package!

Would it be fair to say that rec-def is to lattice’s lfpFrom as expressing recursion with let is to using fix?

But it requires using custom functions like rInsert

True! That is so because I want Data.Recursive.Set to provide a safe interface, and only expose monotonic functions. An alternative interface allowing (lifting of) arbitrary functions is possible as well, but would be a bit less safe.

2 Likes
#23

More on the implementation of the part that turns an imperative propagator network API into a pure API published:

https://www.joachim-breitner.de/blog/793-rec-def__Behind_the_scenes

5 Likes
#24

It seems rec-def is able to observe compiler optimizations. Take for example:

import qualified Data.Recursive.Set as RS

x =
  let s1 () = RS.insert 23 (s2 ())
      s2 () = RS.insert 42 (s1 ())
  in RS.get (s1 ())

With optimizations x is fromList [23,42] but without optimizations x is bottom.

Does that mean purity is violated? Is this a problem at all?

Personally, I think this makes rec-def definitions too brittle. I expect it will be hard to predict termination when you use this in larger programs.

1 Like
#25

Well spotted! Does it happen with -fpedantic-bottoms as well? By default GHC thinks its fine to optimize non-terminating into terminating ones here, which would explain this.

I expect it will be hard to predict termination when you use this in larger programs.

Fair criticism! But is it harder than applying other knot-tying tricks, where you need to ensure sharing actually happens? (I’m definitely not claiming that it’s easier than that…)

2 Likes
#26

Yes, -fpedantic-bottoms doesn’t change anything.

2 Likes
#27

Here is the “same“ effect with pure code:

fibs :: () -> [Int]
fibs () = 0 : 1 : zipWith (+) (fibs ()) (tail (fibs ()))

main = print (fibs () !! 1000)

Without optimization, this program takes very long (not quite bottom, but effectively bottom); with optimizations it is almost instant:

$ ghc --make Test ; timeout -v 10s ./Test
timeout: sending signal TERM to command ‘./Test’
$ ghc -O --make Test ; timeout -v 10s ./Test
817770325994397771

Of course, the unoptimized is not really bottom in the formal sense – with enough time and memory, it will finish. But in a more pragmatic sense it “doesn’t work”, and GHC’s optimization makes it work.

(I’m sure you know that; this is more for the record.)

2 Likes