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

[roconnor at theorem.ca]

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, <roconnor at theorem.ca> 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.''