roconnor@theorem.ca wrote:
Anyhow, the big point is that monoid laws apply to the concepts, not to the representatives.
I agree with this.
Ah, but it is impossible to create such smart constructors because it is undecidable if a particular CReal represents 0 or not.
Either way, we still have undecidability, and I don't think changing the representation can solve it in all cases. Of course, this leads us right back to how to treat _|_ in the context of the monoid laws:
_|_ `mappend` nonzeroRealNum
Since _|_ is a represenative that has no corresponding concept, the above program is simply an error.
I won't argue with the conclusion, but rather with the assumption that led you there. _|_ does have a corresponding concept. _|_ corresponds to the concept that the computation does not terminate. That is, _|_ is not a part of the concept itself, but is another concept altogether. In one sense, I think you are right. _|_ is not a valid representation of the abstract concept. I don't think it is entirely out of place though. In the presence of nontermination, you still have to have an abstraction of nontermination. Haskell's "flaw" is that _|_ can have the same type as the representation of a nonzero real number, even though _|_ itself is not a representation of a nonzero real number. - Jake