[Haskell-cafe] Re: Laws and partial values

[roconnor at theorem.ca]

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.''