
On 2008-03-13, Conor McBride
Hi
On 13 Mar 2008, at 22:28, ajb@spamcop.net wrote:
G'day all.
Quoting Adrian Hey
: What's disputed is whether or not this law should hold: (a == b) = True implies a = b
Apart from possibly your good self, I don't think this is disputed. Quotient types, as noted elsewhere in this thread, are very useful.
For a suitable notion of = on quotients, and with a suitable abstraction barrier at least morally in place, is that really too much to ask?
I really think it is. I don't think the case of "equivalent for this purpose, but not that purpose" can be ignored. Now, it may be the case that fooBy functions are then the right thing, but it's not clear to me at all that this is true. And if the fooBy option works, then why would the foo option fail for equivalence classes? I've seen mention of difficulties with Data.Map, and edison, but not in enough detail to really grasp what the problems are. Until I do, my natural bias (which I'm trying to resist, really) is that it's a matter of lazy coding, not any inherent difficulty.
Their common use predates Miranda, so it's way too late to unbless them now.
How depressing! Untyped programming also predates Miranda. We can always aspire for better. It's not that we need to get rid of Quotients: it's just that we need to manage information hiding properly, which is perhaps not such a tall order.
Meanwhile, the sort/Ord/OrdWrap issue may be a storm in a different teacup: the type of sort is too tight. Ord (total ordering) is way too strong a requirement for sorting. Antisymmetry isn't needed for sorting and isn't possessed by OrdWrap. A bit more structure for order-related classes would surely help here.
Say what? If I don't have a total ordering, then it's possible two elements are incomparable -- what should a sort algorithm do in such a situation? -- Aaron Denney -><-