PriorityQueue interface

[damhiya]

Hi I wrote an interface of priority queue as discussed in #1542.

What I focused was describing soundness of priority queue with small number of fields as possible,
so that not to blowing up record size with declarations of consistency between fields.
For example, I defined toList using popMin, and used permutation relation over result of toList to
guarantee correctness of queue implementation.

If someone has better design idea, please notice me.
I'll also implement instance for PriorityQueue soon, in order to convince interface definition.

[damhiya]

Since I used permutation relation of lists defined over propositional equality, one should think equivalence between Queue as a relation defined over _≡_, not underlying equivalence relation of totalOrder (_≈_). _≈_ should be considered as equivalence of 'priority'

[MatthewDaggitt]

Thanks for putting together a draft @damhiya! It's a fascinating design problem.

From an implementor's perspective, I can definitely see the attraction of having a thin interface with the other operations derivable. However, from a user's perspective I think a fat interface might be more desirable.

For example with your definitions, any notion of equality (i.e permutations of toList applied to each queue) is going to unfold to a huge jumble of stuff when normalised, which is going to be very difficult to parse to say the least. Equally from a performance perspective, converting to a list by repeatedly removing the minimum is going to go to at least O(nlogn) right? I think it would probably be better to expose a toList method that can be implemented efficiently underneath the hood?

With a fat interface, yes you're going to get some blowup in the number of proofs required for the implementation but at least that burden is during the implementation (which only happens once) rather than on the user (of which there will be many).

If we do go for a fat interface then I'd probably have at least the following additional fields:

• Equality type + proof of decidability
• Membership type + proof of decidability
• toList

What are your thoughts?

[MatthewDaggitt]

Hmm from a performance perspective, maybe we should have a separate findMin as well which can be O(1) instead of the O(log n) of popMin?

[damhiya]

In my opinion, ideal solution is providing minimal, but enough operations so that one can derive all general properties of priority queue without having specific instance of priority queue implementation. What I mean by general properties are properties which should be true for any implementation of priority queue. Then, we should prove such properties parametrically, not to prove such things for multiple times.

So I'm looking forward that users may use such proofs constructed on top of minimal interface. However, as you said, it might not very convenient due to complex permutation related things. I think this decision should be made after examining some application of priority queues.

Current implementation of toList is pretty important, not only because it's a heap sort, but it is a connection between whole element of priority queue and result of popMin. If we provide another function elems that return all the elements of the queue without sorting it, then we need toList anyway to convince repeated use of popMin will give the same result. I agree that it would be useful to have elems when we need efficiency, rather than sortedness. However, on proving aspects, I don't see much reason to have elems. If we're working on specific implementation, we can just use elems defined for that implementation. When we're working parametrically, since we don't have the definition of elems, there is no reason to prefer elems over toList.

[damhiya]

Hmm from a performance perspective, maybe we should have a separate findMin as well which can be O(1) instead of the O(log n) of popMin?

I thought one may implement popMin lazily, so make it works O(1) if we demand only for first item. But I'm not sure about evaluation strategy of agda.

[MatthewDaggitt]

Apologies for taking so long to reply, I've been mulling this over in my head.

In my opinion, ideal solution is providing minimal, but enough operations so that one can derive all general properties of priority queue without having specific instance of priority queue implementation. What I mean by general properties are properties which should be true for any implementation of priority queue. Then, we should prove such properties parametrically, not to prove such things for multiple times.

So what are the advantages of this solution for the users of the standard library? I understand that from the implementor's perspective it's desirable to have a minimal interface so as to only have to prove the properties once. I ask, because the point of the standard library is to make the life of the users as easy possible, not the life of the implementors.

So I'm looking forward that users may use such proofs constructed on top of minimal interface. However, as you said, it might not very convenient due to complex permutation related things. I think this decision should be made after examining some application of priority queues.

Hmm having tried it out, the type messages are still pretty bad even when we're considering an abstract definition. I'm getting things like:

x ∷
      SizeLaws.toListAux sizeLaws (meld p q)
      (Data.PriorityQueue.Base.SizeLaws.Size⇒Acc sizeLaws
       (size (meld p q)) (meld p q) refl)
      ≡
      SizeLaws.toListAux sizeLaws (insert x p)
      (Data.PriorityQueue.Base.SizeLaws.Size⇒Acc sizeLaws
       (size (insert x p)) (insert x p) refl)
      ++
      SizeLaws.toListAux sizeLaws q
      (Data.PriorityQueue.Base.SizeLaws.Size⇒Acc sizeLaws (size q) q
       refl)

Having toList as a primitive would make this into:

x ∷ toList (meld p q) ≡ toList (insert x p) ++ toList q

The situation is going to get much worse once you're using a concrete backing implementation.

Current implementation of toList is pretty important, not only because it's a heap sort, but it is a connection between whole element of priority queue and result of popMin. If we provide another function elems that return all the elements of the queue without sorting it, then we need toList anyway to convince repeated use of popMin will give the same result.

I'm not suggesting removing the current definition of toList merely renaming it something like popAll and making it part of the derived definitions, rather than using it as part of the laws.

[MatthewDaggitt]

Closing this as I don't think we're going to make progress on it.