[Haskell-cafe] Re: Laws and partial values
roconnor at theorem.ca
roconnor at theorem.ca
Sat Jan 24 17:52:15 EST 2009
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.''
More information about the Haskell-Cafe