I'm still getting my head around this myself, but I know a few references that might help (maybe not directly, but they're in the ballpark).
1 I believe the phrase "natural lifting" or "naturality of liftings" is what you're after when you attempt to compare a monad and a "bigger monad" that includes the affects of the first. I recall this concept from Liang and Hudak's modular monadic semantics work, but I'm having a heck of a time quickly finding it in their papers. Try at least section 8.1 in Monad Transformers and Modular Interpreters. 2 Another example that helped me when getting a feel for reasoning about monadic code (which is the basis of what we're doing here) was William Harrison's "Proof Abstraction for Imperative Languages _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
