[Haskell-cafe] Re: Laws and partial values

[Jake McArthur]

What you said makes little sense to me either. ;) But I will try to fit 
the pieces together as best I can.

It appears to me that you may be talking about isomorphisms between the 
concepts we try to map to data types and the data representations 
themselves, and that you are postulating that these concepts are 
necessarily total, therefore the representations should be as well, or 
something like that.

If my understanding of your point is correct, then I disagree with it. 
What you describe sounds like abstraction, and what you describe as a 
partial function sounds like a *leaky* abstraction. If we truly want to 
restrict the domain of a function to nonzero real numbers, then the 
"total" way to go about it would be to create a new type that represents 
this domain, say by wrapping your real number type with a newtype and 
only exporting smart constructors to build values of that type. Deep 
inside, the function will definitely require a partial expression, but 
this is abstracted away. Then you can define a Monoid instance for this 
domain without fear.

But you *still* have to account for nontermination. You can still arrive 
at a situation where you have

     _|_ `mappend` nonzeroRealNum

, even though you can't end up with

     0 `mappend` nonzeroRealNum

. I hope I have understood correctly. I feel that I have not and that 
this email will just contribute to the confusion of other readers. :\

- Jake

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. :)
>