[volta83]

> 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]

I 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]

I 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]

> 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.