Check strictness details for Data.Tree instances

[treeowl]

I recently fixed a strictness problem affecting an identity law for the Monad Tree instance. We should verify that strictness is okay for the associativity law, and similarly check strictness for the MonadFix laws. One question is whether list conses should contain thunks that evaluate to trees or the trees themselves.

[treeowl]

I think the Monad instance is okay now. Here's a sketch of a proof of the associative law. Does that look okay?

(Node x ts >>= f) >>= g
= (case f x of
     Node x' ts' -> Node x' (ts' ++ map (>>= f) ts)) >>= g
= case (case f x of
    Node x' ts' -> Node x' (ts' ++ map (>>= f) ts)) of
    Node x'' ts'' -> case g x'' of
                       Node x''' ts''' -> Node x''' ts''' ++ map (>>= g) ts''
= -- case of case
  case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' (ts'' ++ map (>>= g) (ts' ++ map (>>= f) ts))
= case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' (ts'' ++ (map (>>= g) ts' ++ map (>>= g) (map (>>= f) ts)))
= case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' (ts'' ++ (map (>>= g) ts' ++ map (\z -> (z >>= f) >>= g) ts)) -- induction
= case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' (ts'' ++ (map (>>= g) ts' ++ map (\z -> z >>= (\y -> f y >>= g)) ts))
= case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' (ts'' ++ (map (>>= g) ts' ++ map (>>= (\y -> f y >>= g)) ts)
= case f x of
    Node x' ts' -> case g x' of
                     Node x'' ts'' -> Node x'' ((ts'' ++ map (>>= g) ts') ++ map (>>= (\y -> f y >>= g)) ts)
= case (case f x of
          Node x' ts' -> case g x' of
                           Node x'' ts'' -> Node x'' (ts'' ++ map (>>= g) ts')) of
    Node x''' ts''' -> Node x''' (ts''' ++ map (>>= (\y -> f y >>= g)) ts)

= case f x >>= g of
    Node x' ts' -> Node x' (ts' ++ map (>>= (\y -> f y >>= g)) ts)
= case (\y -> f y >>= g) x of
    Node x' ts' -> Node x' (ts' ++ map (>>= (\y -> f y >>= g)) ts)
= Node x ts >>= (\y -> f y >>= g)

It might also be worth checking if the Applicative instance matches up right. The MonadFix instance is likely to be tricky to check in such detail; if someone has an idea, let me know. We should probably collect whatever proofs we produce somewhere in the repo.

[treeowl]

Another question about the MonadFix instance relates to how to handle levels within the tree. At present, we effectively get the full spine (that is, list structure) of each level by applying the given function to the root. That's not the only option. We could also use the root of the head of the list to learn about what comes next, in much the same way that the MonadFix [] instance does. However, I think we probably shouldn't do that; Tree is supposed to represent a multi-way tree; it seems much more natural for the information to flow down and right, rather than up and right. I suspect this is compatible with the MonadFix laws, but again, a detailed check would be wise.

[treeowl]

@m-renaud was right; whatever we do, we need to document the MonadFix instance.