PriorityQueue based on Okasaki's "Purely Functional Data Structures"

[dvberkel]

I have created a pull-request that adds a PriorityQueue to base.

A priority queue is a

an abstract data type similar to a regular queue or stack data structure in which each element additionally has a "priority" associated with it. In a priority queue, an element with high priority is served before an element with low priority.

In the implementation a priority is function A -> Nat. A smaller natural number corresponds with a higher priority.

I would love to receive feedback. Specifically on style, implementation and improvements.

[dvberkel]

I am looking for some theorems to proof so I can cement my knowledge of Kind's theorem proving

[rigille]

Also be careful with this current limitation of the smart motive: #278. I hope to fix it soon ^^

[dvberkel]

The following is my attempt to work towards the In type for queues. It delegates to an In type for trees. But the following seems to trip up the Kind type checker:

PriorityQueue.Tree.In<A: Type>(tree: PriorityQueue.Tree<A>, a: A): Type
case tree {
    empty: Empty
    node:
      ?a
    //   PriorityQueue.Tree.Location!(tree, a)<hypothesis>
}

PriorityQueue.Tree.left_of<A: Type>(tree: PriorityQueue.Tree<A>)<Hyp: PriorityQueue.Tree.is_empty!(tree) == false>: PriorityQueue.Tree<A>
  case tree with Hyp {
      empty:
        let hypothesis = Hyp :: rewrite x in (x == false) with PriorityQueue.Tree.empty_tree_is_empty<A>
        let impossible = Bool.true_neq_false(hypothesis)
        Empty.absurd!(impossible)
      node:
        tree.left
  }!

PriorityQueue.Tree.right_of<A: Type>(tree: PriorityQueue.Tree<A>)<Hyp: PriorityQueue.Tree.is_empty!(tree) == false>: PriorityQueue.Tree<A>
  case tree with Hyp {
      empty:
        let hypothesis = Hyp :: rewrite x in (x == false) with PriorityQueue.Tree.empty_tree_is_empty<A>
        let impossible = Bool.true_neq_false(hypothesis)
        Empty.absurd!(impossible)
      node:
        tree.right
  }!

type PriorityQueue.Tree.Location<A: Type>(tree: PriorityQueue.Tree<A>, a: A)<Hyp: PriorityQueue.Tree.is_empty!(tree) == false> {
  here(prf: PriorityQueue.Tree.peek!(tree)<Hyp> == a)
  left(prf: PriorityQueue.Tree.Location!(PriorityQueue.Tree.left_of!(tree)<Hyp>, a))
  right(prf: PriorityQueue.Tree.Location!(PriorityQueue.Tree.right_of!(tree)<Hyp>, a))
}

And I am not sure why. The code can be found in situ in the branch for the pull-request

When I run kind-scm PriorityQueue.Tree.In it does not seem to halt. I was expecting to say something clever to make me slap my forehead

[rigille]

Congratulations you found a bug in the desugaring process of datatype definitions! It's described in #281.

That's not what's causing the loop however. There's a missing parameter at the end of, for example, PriorityQueue.Tree.Location!(PriorityQueue.Tree.left_of!(tree)<Hyp>, a). It cannot be filled because left_of tree could be empty.

How about this?

type PriorityQueue.Either <A; Type, B: Type, C: Type> {
  left(val: A)
  here(val: B)
  right(val: C)
}
PriorityQueue.Tree.In<A: Type>(tree: PriorityQueue.Tree<A>, a: A): Type
  case tree {
    empty:
      Empty
    node: 
      PriorityQueue.Either<
        PriorityQueue.Tree.In(tree.left),
        a == tree.here,
        PriorityQueue.Tree.In(tree.right)
      >
  }

[dvberkel]

Where PriorityQueue.Either and PriorityQueue.Tree.In.aux should be the same 🤔

[rigille]

oops let me fix this

[dvberkel]

Progress on the @rigille suggestions

• PriorityQueue.In
• PriorityQueue.priority
• PriorityQueue.safe_head
• PriorityQueue.In.not_empty
• PriorityQueue.head_ok