On Fri, May 1, 2015 at 11:34 PM, Keean Schupke <[email protected]> wrote: > On 2 May 2015 03:44, "Matt Oliveri" <[email protected]> wrote: >> > You can have a global coherence check. >> >> Sure, but that's a crutch in this case. Depend on the order rather >> than a phantom type, and you don't need typeclasses or coherence at >> all for this. > > Well I want to make sure it's a compile time property, hence a type.
It's frustrating that you're still confused about this, despite our long discussion about it off-list. Anyway, in my solution, the order a Set is stored in is tracked at compile time. >> Here is the signature for union in my solution: >> union : forall (E:Type) (o:Order E),Set E o->Set E o->Set E o >> >> Arguments E and o are implicit. In fact E can be implicit for Set too: >> union : forall (E:Type) (o:Order E),Set o->Set o->Set o > > What is o? Is it an implicit value? Yes. > Do I really want orders being passed around at runtime? I suppose not. But I figure you could implement passing the order in the same way as how an Ord instance would be passed with typeclasses. It shouldn't matter that the way the compiler picks the argument is different. If passing an ordering at runtime is unacceptable, then so are typeclasses. > Doesn't Set need a type parameter for the type of the > object n the set? That's what E is. The type of Set is: Set : forall E:Type,Order E->Type The E argument can be implicit because it can be recovered from the type of the Order argument. This is the same non-instance-resolution implicit argument support as with union. You don't have to make it implicit if it seems weird to you. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
