Bug fix: handle graphs with cycles #3

igormoreno · 2021-05-26T06:43:39Z

The function to turn diagrams into ASTs is incorrect! It is not handling cycles appropriately so if the graph has cycles the function does not terminate. The issue wasn't detected because only diagrams constructed from ASTs were being tested.

igormoreno · 2021-05-26T06:57:51Z

Done in:
58036cf (I left the intermediate steps as comments in this commit for documentation for us (erased in the next))
78a168d

The fix consists of traversing the diagram keeping track of the nodes already visited. This means we need state so I introduced a State monad. I had never used this monad before so I had to learn that. Moreover, everything has to happen within (or in conjunction with a monad that represents the failure of the conversion from diagram to AST (which has been represented by a Maybe). This means that we need a monad transformer to deal with the combination of these monads. I had never actually had to use a monad transformer before so I had to learn that. The final solution is very elegant. It is crucial that the implementation is correct and elegant because we will present the code in the paper and they will definitely care.

The first attempt uses manual manipulation of state:

ExpTreeDiagram -> Set Int -> (Maybe Program, Set Int)

Then I introduce the State monad containing a Maybe:

ExpTreeDiagram -> State (Set Int) (Maybe Program)

After I go through a series of refactorings gradually introducing the appropriate State manipulation functions (get, put, modify, withState). Finally, I merged State and Maybe using StateT:

ExpTreeDiagram -> StateT (Set Int) Maybe Program

That allowed for the removal of a layer of monad manipulation and, after a couple of rewrites, the structure became more clear... it is essentially the same code as before! That is a pattern matching on the structure of the diagram, followed by the construction of the corresponding AST nodes through a monad (before Maybe and now StateT) except that now the construction of nodes is guarded by a factored out ifNotVisited check which reads the state, checks if the node was visited, and adds it to the state if necessary.

Other variations of the implementation were considered:

Use the monad transformers MaybeT instead of StateT: not good because we need State information to determine Maybe (if visited return Nothing). Interestingly, the other Nothing depends only on the structure of the Diagram (not State).
Flip the arguments from the first version: not good because we get State -> Diagram -> Maybe and we can't combine State and Maybe with a transformer leading to extra monad manipulation code. But! Diagram -> Maybe is a Reader so that could actually work with 2 monads stacked: State, Reader, Maybe. Maybe there's a way to use a transformer to combine these 3, but I'm not sure.

An important point is that the commutation proof of the bisimulation relays on the argument that:

diagram2ast . ast2diagrm == return

But I'm not sure how to prove that with the StateT in the middle. Maybe I can just do it with successive simplifications... I haven't tried actually.

Issue: Tests graphs that are not only generated from ASTs (#4)