Re: Laws and partial values (was: [Haskell-cafe] mapM_ -> Monoid.Monad.map)

Thanks for letting me reflect on this. I assume that my final program (my final value) is always a total value. Anything else is an error. Therefore, if we required relaxed monoid laws of the form x `mappend` mzero <= x then we could safely substitute (x `mappend` mzero) by x without changing the final value (I think this true). But the reverse substituion ,replacing x with (x `mappend` mzero), might not be sound. Now, I can see why you would prefer that the laws hold for partial values. On Fri, 23 Jan 2009, Luke Palmer wrote:

On Fri, Jan 23, 2009 at 6:10 PM, wrote: On Fri, 23 Jan 2009, Derek Elkins wrote:

mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law.  That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws.

So the answer to the question is "Yes."  Another example of making things as lazy as possible going astray.

I'd like to argue that laws, such as monoid laws, do not apply to partial values.  But I haven't thought my position through yet.

Please try to change your mind.  

You know how annoying it is when you are doing math, and you want to divide, but first you have to add the provision that the denominator isn't zero.  Saying that monoid laws do not apply to partial values, while easing the implementation a bit, add similar provisions to reasoning. 

For example, it is possible to prove that foldr mappend mempty (x:xs) = foldr1 mappend (x:xs).  Which means that anywhere in the source where we see the former, we can "clean it up" to the latter.  However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_.  This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct.

Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to.  You can pretend they don't exist, but then you have to be okay with never using an infinite data structure.  I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms.

Luke

-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''