-- An non-recursive isomorphism between `[[[x]]] + [[[x]]]` and `x + [[[x]]]`.
-- Reminiscent of "Seven Trees in One".
-- Based on the discussion at https://golem.ph.utexas.edu/category/2013/04/iterating_the_free_monoid_cons.html.

iso :: Either [[[x]]] [[[x]]] -> Either x [[[x]]]
iso (Left x) = Right ([[]] : x)
iso (Right []) = Right []
iso (Right ([] : xs)) = Right ([] : xs)
iso (Right (([] : ys) : xs)) = Right (([] : [] : ys) : xs)
iso (Right [[[z]]]) = Left z
iso (Right ([[z]] : [] : xs)) = Right ([[z]] : xs)
iso (Right ([[z]] : (w : ws) : xs)) = Right (([] : (z : w) : ws) : xs)
iso (Right (([z] : y2 : ys) : xs)) = Right (([z] : y2 : ys) : xs)
iso (Right (((z : z2 : zs) : ys) : xs)) = Right (((z : z2 : zs) : ys) : xs)

iso' :: Either x [[[x]]] -> Either [[[x]]] [[[x]]]
iso' (Right ([[]] : x)) = Left x
iso' (Right []) = Right []
iso' (Right ([] : xs)) = Right ([] : xs)
iso' (Right (([] : [] : ys) : xs)) = Right (([] : ys) : xs)
iso' (Left z) = Right [[[z]]]
iso' (Right ([[z]] : xs)) = Right ([[z]] : [] : xs)
iso' (Right (([] : (z : w) : ws) : xs)) = Right ([[z]] : (w : ws) : xs)
iso' (Right (([z] : y2 : ys) : xs)) = Right (([z] : y2 : ys) : xs)
iso' (Right (((z : z2 : zs) : ys) : xs)) = Right (((z : z2 : zs) : ys) : xs)