[Haskell-cafe] Re: Laws and partial values

[Lennart Augustsson]

I can't argue with your position, because I don't understand it. :)

  -- Lennart

On Sat, Jan 24, 2009 at 10:52 PM,  <roconnor at 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.''
>