On 1 May 2015 at 15:07, Matt Oliveri <atma...@gmail.com> 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. 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. We can provide the guarantee of order too, but it gets quite complex. 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. Keean.
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
