On Fri, May 1, 2015 at 10:34 AM, Keean Schupke <[email protected]> wrote: > On 1 May 2015 at 15:07, Matt Oliveri <[email protected]> wrote: >> >> Now here's the nitpicky problem: If you don't have coherent instances, >> this _still_ might not work. Some idiot could make another "instance >> Ord AN int", and union could receive sets ordered differently after >> all. This is much less likely, since people who understand the setup >> would know to define a new order label to make a new Ord instance, but >> you still have no guarantee. > > 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. >> It seems better to me to skip right to dependent types, so the Set >> types can depend directly on the order the set uses. No need for >> typeclasses or phantom types here. To really get a guarantee, each Set >> should come with a (erased) proof that the elements are stored in the >> appropriate order. This actually enforces the invariant. > > This is where I agree with the video, I don't necessarily want to always > pass around the order explicitly. Its not too bad with just ordering, but it > can get pretty bad. Consider where you have a few different container types, > say two arrays and a map between them, you start having to pass around stuff > like: > > op :: ArrayDict a -> ArrayDict b -> MapDict a b -> Array a -> Array b -> > Bool > > whereas with type-classes 'op' could be an infix binary operator. You have made an assumption. In the solution I am proposing, the order _would_ be an implicit argument. Just not an _instance_ argument. In other words, the argument that implicitly gets passed is determined by unification, not typeclass instance resolution. This works because the types of the Set arguments depend on the order, so from those types, we know what order to pass. This is very standard in dependently typed languages. 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 > Interestingly type-classes are related to Prolog clauses, where clause heads > are like instance definitions and are globally unique. This is where you go > if you follow the argument to it conclusion and get rid of first class > functions. I don't think anyone has made an argument that would get rid of first class functions if followed to its conclusion. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
