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

[Luke Palmer]

On Sat, Jan 24, 2009 at 10:32 AM, <roconnor at theorem.ca> wrote:

> On Fri, 23 Jan 2009, Luke Palmer wrote:
>
>  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.
>>
>
> BTW, This last statement isn't true.  The expression (let x = 1:x in x)
> won't work in CBV, but it is a well defined value without any bottoms.
> In fact, every subexpression in that value is a well defined value wihtout
> any bottoms.


That's not what I said.  My statement was a hypothetical: *if* it works
call-by-value, then you don't have to worry about bottom.  This program does
not work in CBV, so my statement is true.

I'm just being pedantic, of course.

The deeper reason that you have to worry about bottoms in this expression is
that its denotation is a limit:  { _|_, 1:_|_, 1:1:_|_, 1:1:1:_|_, ... }.
Bottom has an essential role in describing infinity, not just programs which
don't halt.

Luke
**
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/226e28cd/attachment.htm