Adding priority queue implementation

[damhiya]

Hi. I implemented leftist heap based priority queue in agda. So I'm going to contribute this code to agda-stdlib if such thing was desired.

However, this code is a bit messy and I didn't care so much about library design while writing it. I would appreciate if someone give a comment about the code.

[MatthewDaggitt]

Hi @damhiya, thanks for opening the issue, yes we'd definitely be interested in a priority queue implementation!

However, the first thing we'd want to do I think is to define an interface (operations + laws) for priority queues. We'd then show that your implementation satisfied that interface. Would you be interested/willing to put together such an interface?

[damhiya]

Hi @damhiya, thanks for opening the issue, yes we'd definitely be interested in a priority queue implementation!

However, the first thing we'd want to do I think is to define an interface (operations + laws) for priority queues. We'd then show that your implementation satisfied that interface. Would you be interested/willing to put together such an interface?

Of course!

[MatthewDaggitt]

Great! If you'd like to open a PR with your proposed interface (probably in Data.PriorityQueue.Interface?) that'd be the best course. Once we've got the interface nailed down and merged in, we can then open a second PR with your implementation :+1:

[MatthewDaggitt]

See feedback in #1552 for a design discussion.

[damhiya]

I'm really sorry for inactivity. I was doing other works. I'll work on this in the future unless someone do it.

[MatthewDaggitt]

Absolutely no worries, not everything has to be added. Our discussion alone has really helped clarify my thoughts on this, so thanks!

[andreasabel]

Btw, I played around with a leftist heap implementation in Agda and ended up with this: https://gist.github.com/andreasabel/352fee52a39c0bebbd5059bff86d9b6e This is 170 loc including comments, imports, and some auxiliary functions about adding a top element to a decidable total order. The actual implementation of heaps and merging is the last third of this gist (rather tiny, I'd say).

[gallais]

We do have a generic min construction: http://agda.github.io/agda-stdlib/Algebra.Construct.NaturalChoice.Min.html And also the extension of an existing total order with a supremum: http://agda.github.io/agda-stdlib/Relation.Binary.Construct.Add.Supremum.NonStrict.html

[Taneb]

Here's a different implementation I made a while back, using pairing heaps: https://gist.github.com/Taneb/7e502c708e2e6eabcea5e7638f42b593