On Fri, May 1, 2015 at 2:28 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
That doesn't seem like the way to go to me. We should be able to determine statically that two sets use the same order, so that we can just call fast union. This doesn't work if each set hides its order in an existential package. > 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. But how do you actually do that test? If you arrange a way to do that test, then yes, you could do general union that way. But it seems like a good idea to expose fast union too. > If Ord has multiple instances, we can still imagine lifting this check to > the type level, but the check can't be evaded. Yeah, that's what my solution essentially does. Just that it isn't an instance anymore. > What the discussion is telling us is that Set isn't a datatype. It's an > abstract interface. Yeah. I decided not to give Keean a hard time about that, since it'd just make the code longer, fast union is just an example, and Keean and I get into arguments about everything. > 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. Wait you're saying the element type doesn't need Eq, or Set doesn't? It kinda seems like the element type needs Eq to me. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
