Laws and partial values (was: [Haskell-cafe] mapM_ ->
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
> 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.
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.''
More information about the Haskell-Cafe