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

[roconnor at theorem.ca]

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.

Now I'm wondering how many bottoms I use in my actual code, because it 
seems like, even though I make use of lazy evaluation, I still don't have 
sub-expressions with bottoms.  If it is the case that I never make use of 
bottoms, then having laws only apply to total values is fine.

Obviously I use bottoms via the error function etc, but I don't count 
these.  These can only be accessed by calling functions with paramters 
violating their preconditions.  If I had dependent types, I'd place the 
preconditions formally into the definition of the function.  I'm looking 
for a place where I have a partial value as a sub-expression of my program 
in some essential way.  I find it plausible that this never happens.

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