On Sat, 24 Jan 2009, Lennart Augustsson wrote:
You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory. Ordinary programming languages include non-termination, so that has to be captured somehow in the semantics. And that's what bottom does.
I'd like to argue (but am not certain) that all the sub-expressions of all *correct* programs are total, or rather that the values that the sub-expressions represent are total.
One needs to distinguish between the value of the representatives of data, and the data being represented. For example (constructive) real numbers are represented by Cauchy sequences, but real numbers are themselves a quotient of this type. We cannot create a data type that directly represents a real numbers and are forced to use representatives to compute with them. Similarly we want the reciprocal function only to be defined on real numbers that are apart from zero (the reciprocal total on this domain), but there is no such function type available in Haskell to do this. Therefore we represent it by a partial function.
Therefore we can safely reason about such programs by substitutions using laws (such as monoid laws) that are correct with respect to the *what the values are representing*. For example, real numbers form a monoid under addition only when the equivalence relation for the data that the values represent is used. Would anyone here argue that (Sum CReal) should *not* be a Monoid instance?
Sorry if this sounds a bit muddled. I need to find a clear way of conveying what I'm thinking. In short, my position is that partial values are only used to define the values of fixpoints and are sometimes used in the represenatives of data, but the data being represented is always total. Monoid laws etc. only apply to the data being represented, not to the underlying represenations.
If my position is untenable, please explain. :) -- 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
