4 ms·
> If you didn't have canonical implementations, you would have to give up being able to write safe & efficient data-structures like this. No? Just make the typ
by volta83 5y ago
> If you didn't have canonical implementations, you would have to give up being able to write safe & efficient data-structures like this.
No? Just make the type generic on the ordering.
Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) or something like that.
- curtisf 5y agoI explained why this doesn't work -- what do you do when you combine two heaps with different internal orderings? You need some way to enforce that the orderings are the _same_. A canonical ordering per type is how Haskell does it; dependent types are a more complicated alternative method.
- remexre 5y agoI think GP is suggesting... well, dependent types, but in a restricted enough way that I don't believe it adds additional complexity over DataKinds. At least, I read > Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) as saying the kind of MaxHeap should be, in Coq syntax, (forall (T : Set), (T -> T -> Bool)). I think this doesn't add any additional complexity vs DataKinds since the function doesn't need to be evaluable at typechecking time, just unified against at construction-time.
- volta83 5y ago> You need some way to enforce that the orderings are the _same_ Just require that the Ord type is the same for all heaps ? MaxHeap(MaxHeap(T, MyOrd), MyOrd) uses the same ordering, but MaxHeap(MaxHeap(T, Ord0), Ord1) does not.
- volta83 5y agoA simple way to do this is to: MyNestedMaxHeap(T, Ord) = MaxHeap(MaxHeap(T, Ord), Ord) such that when using MyNestedMaxHeap only one Ord type can be passed.