
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?
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. Isn't there room for hope? All the best Conor