Laws and partial values (was: [Haskell-cafe] mapM_ ->
Monoid.Monad.map)
roconnor at theorem.ca
roconnor at theorem.ca
Sat Jan 24 12:32:51 EST 2009
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.''
More information about the Haskell-Cafe
mailing list