roconnor at theorem.ca roconnor at theorem.ca
Fri Jan 23 22:22:38 EST 2009

```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.
>
>
>
> 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.''
```