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.''
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
