Hi
On 13 Mar 2008, at 23:33, Aaron Denney wrote:
On 2008-03-13, Conor McBride <[EMAIL PROTECTED]> wrote:
Hi
On 13 Mar 2008, at 22:28, [EMAIL PROTECTED] wrote:
G'day all.
Quoting Adrian Hey <[EMAIL PROTECTED]>:
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.
Sure. But use the right tools for the job.
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?
It seems reasonable to construct quotients from
arbitrary equivalences: if fooBy works for the
carrier, foo should work for the quotient. Of
course, if you want to expose the representation
for some other legitimate purpose, then it wasn't
equality you were interested in, so you should
call it something else.
A bit more structure
for order-related classes would surely help here.
Say what?
Don't panic!
If I don't have a total ordering, then it's possible two
elements are incomparable
Quite so.
-- what should a sort algorithm do in such a
situation?
Not care. Produce a resulting list where for any
[..., x, ..., y, ...]
in the result, y <= x implies x <= y. Vacuously
satisfied in the case of incomparable elements.
In the case of a total order, that gives you
y <= x implies x = y (and everything in between),
but for a preorder, you put less in, you get less
out.
Will that do?
Conor
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
