20 Feb
2007
20 Feb
'07
10:55 a.m.
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