On Thu, Apr 30, 2015 at 2:58 PM, Matt Oliveri <atma...@gmail.com> wrote: > On Thu, Apr 30, 2015 at 5:10 PM, Matt Rice <ratm...@gmail.com> wrote: >> On Thu, Apr 30, 2015 at 12:53 PM, Matt Oliveri <atma...@gmail.com> wrote: >>> On Thu, Apr 30, 2015 at 6:31 AM, Matt Rice <ratm...@gmail.com> wrote:
>>>> and you define eq as a comparison between 2 sets, and not 2 sets and a >>>> peacekeeping force, you arrive at a couple of different possible >>>> answers... >>>> >>>> yes (same elements by my eq), no (different elements by my eq), no >>>> (x.eq != y.eq), or nonsense the eq's aren't the same this is not a >>>> valid question, >>> >>> I'd prefer the last one, if it's possible for the sets to have >>> different element equality tests. >> >> That's the answer that typeclasses give, that the types aren't the same >> and so the answer is a type error. > > Umm, well I thought with typeclasses with instance coherence, you > can't have sets of the same type whose elements are "unique" according > to different equality tests. > > (Assuming you are using the Eq instance > for the equality test.) So I wouldn't call that a type error when the > tests are different, but that you can't arrange for the tests to be > different. > > Back in the fast union example, the whole problem with not having > instance coherence is that the type system actually does _not_ have a > way to check that the arguments to union use the same ordering. It was > relying on the (anti-modular) global property that all sets with the > same element type use the same ordering. Right, I was just trying to get to the idea that typeclasses always give the 'correct' answer, and thus any solution which defines equality as a single order with a relation between 2 types must exhibit the same behavior as type classes for those cases where typeclasses *will* give you an answer... >>> With dependent >>> types, sets could be tagged, at the type level, with which element >>> equality test they use. Neither the elements nor the element type have >>> an associated equality. With implicit instance arguments, it seems >>> ambiguous how set equality is supposed to work. >> >> most things can take an explicit ordering if you must, >> equality is really where this breaks down because the definition of >> equality as a comparison between 2 distinct things, > > Huh? That doesn't sound right. If we could only test for equality > between distinct things, why are we doing the test? We'll definitely > get false. Sorry, s/2 distinct things/2 operands/ you can't add a 3rd argument to Eq, or Ord to add explicitness, assuming you get rid of 'use', so that types are passed in from the top to the calling function you can have some function union(Ord 'a) -> Set 'a * Set 'a -> Set 'a or some other ordering unionSlow(Ord 'a) -> Set 'a * Set 'a -> Ord 'a -> Set 'a to get a different ordering from the input sets than the output sets. equality operators are inherently troublesome due to the parameter set so you can't just pass them explicitly, you seem stuck with anti-modular global or smashing a specific operator in place for the operands to use so that the operator *is* the 3rd parameter to Eq, I can't think of any other solutions than the dependent type one you described > I can see that it's probably a lot less useful to have multiple > notions of equality in the same type than multiple notions of order. > But that's nothing technical, it's just a convention that a type > usually comes with the right notion of equality for elements (even if > you can't test it). Eq may be less useful but it's not less troublesome, since Ord entails Eq. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
