I can't argue with your position, because I don't understand it. :) -- Lennart
On Sat, Jan 24, 2009 at 10:52 PM, <rocon...@theorem.ca> wrote: > 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