On Wed, Apr 29, 2015 at 2:12 PM, Matt Oliveri <[email protected]> wrote:
> > The definition of union should be (using braces for the implicit
> parameter):
> >
> > union :: {Ord a} -> Set a -> Set a -> Set a
>
> The meaning of that type is ambiguous, depending on whether you expect
> instances to be coherent or not. Will all three sets be ordered
> according to the implicit argument, or just the result? Fast union
> depends on all three using the same order.
While I agree with the pragmatic implementation point that you are making
here, you're overlooking the obvious: the consequence of this statement is
that fast union isn't actually operating on sets at all. It's operating on
some existentially encapsulated data type that specifies an ordering, such
that an interface providing definitions for set operations over the
encapsulated data type exists.
A *general* implementation of union needs to do a trial "open" on the
existential type, test the underlying Ord implementations for suitable
compatibility, and either run the fast union algorithm or fall back to the
slow one.
If Ord has multiple instances, we can still imagine lifting this check to
the type level, but the check can't be evaded.
What the discussion is telling us is that Set isn't a datatype. It's an
abstract interface.
Oh. And no, they don't have to have Eq either. They have to have an
equivalence-rejecting operator. That could be EQ, EQL, EQUAL, EGAL, or
several others. The question of how equivalence is defined is orthogonal to
how containment is defined.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
