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