Add Queue datatype

[silas-hw]

Will eventually resolve #3083. Uses the two-list method mentioned in #3072 (but in a PR not generated by an LLM this time).

There may be some poor stylistic choices due to my unfamiliarity with the standard library, for which I am sorry! There are some 'low hanging' basic operations that could still be added, but I think those would be good for separate PRs.

[JacquesCarette]

When adding new functionality, we tend to make somewhat larger PRs than when fixing things. In particular, a bunch of properties should be proved too. The main reason is that quite often the proofs reveal when some of functionality was written in a correct-but-hard-to-use (or reason about) manner. So basically all of #3083 will need to be done in this PR.

On the other hand, asking for reviews of the intermediate steps is a good idea.

[JacquesCarette]

As was mentioned on the (closed) PR, one of these should be a SnocList.

[JacquesCarette]

Probably consider fromSnocList too.

[jamesmckinna]

Some alternative suggestions as to implementation.

Against @JacquesCarette , and because I'm a bit more 'OO-minded', I tend to put things like Empty/isEmpty as manifest fields of the record, because then I don't have to think about the scope management. Similarly toList, because all the pieces are at-hand without further ado... but YMMV.

As for references for this kind of implementation, probably Okasaki's "Purely functional data structures" would be the go-to citation?

Oh, and: fix-whitespace!

[gallais]

As for references for this kind of implementation, probably Okasaki's "Purely functional data structures" would be the go-to citation?

There is also https://doi.org/10.1017/S0956796800001489

[jamesmckinna]

When adding new functionality, we tend to make somewhat larger PRs than when fixing things. In particular, a bunch of properties should be proved too. The main reason is that quite often the proofs reveal when some of functionality was written in a correct-but-hard-to-use (or reason about) manner. So basically all of #3083 will need to be done in this PR.

On the other hand, asking for reviews of the intermediate steps is a good idea.

So, eg.:

toList-fromList : toList (fromList xs) ≡ xs

The converse direction requires some simulation relation on Queues... but that's (probably) worth discussing/thinking about a bit more... although the toList observer of 'internal state' is already one kind of characteristic...

[silas-hw]

I think that's a generally good direction to go in, even if just to be consistent with Algebra.* . I remember briefly talking about Raw* interfaces with @TOTBWF, but can't exactly remember what was brought up.

[silas-hw]

* ... permitting the following [ DRY ] simplifications
  ```agda
  queue : List A → List A → Queue A
  queue []         ys = fromList (reverse ys)
  queue xs@(_ ∷ _) ys = mkQ xs ys null-∷
  ```

fromList uses the queue smart constructor! In a way which fails the termination checker as well (at least currently)...

[silas-hw]

I think _≈_ can be defined regardless of implementation in terms of enqueue:

data _≈_ {A : Set a} : Queue A → Queue A → Set a where
  refl : ∀ {q : Queue A} → q ≈ q
  enq  : ∀ {q q' : Queue A} {x : A} → q ≈ q' → (enqueue x q) ≈ (enqueue x q')

See below

[gallais]

Isn't _≈_ defined inductively equivalent to _≡_?

[silas-hw]

Isn't _≈_ defined inductively equivalent to _≡_?

Yeah, it is...

How else would you go about defining it? Or is it good to keep this alongside a proof of logical equivalence?

Edit: I see where I'm going wrong! It's not observational at all...

[jamesmckinna]

* ... permitting the following [ DRY ] simplifications
  ```agda
  queue : List A → List A → Queue A
  queue []         ys = fromList (reverse ys)
  queue xs@(_ ∷ _) ys = mkQ xs ys null-∷

fromList uses the queue smart constructor! In a way which fails the termination checker as well (at least currently)...

Sorry! I'd in the meantime refactored my own experiment to have

fromList : List A → Queue A
fromList xs = mkQ xs [] (const [])

which is obviously uncoupled from queue (and indeed, that is the point!).

[jamesmckinna]

Thanks for this... I'd needed some specimen fields, but it occurs to me that we should only add IsQueue once we actually agree what properties we want!

[jamesmckinna]

Eg the above two properties, I think, follow from:

record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where

  open RawQueue rawQ

  field
    isEquivalence   : IsEquivalence (_≈_ {A = A})
    ≈-resp-Empty    : Empty Respects (_≈_ {A = A})
    ≈-=[toList]⇒-≡  : _≈_ {A = A} =[ toList ]⇒ _≡_
    empty-toList    : ∀ {q : Q A} → Empty q → Null (toList q)
    empty-fromList  : Null {A = A} xs → Empty (fromList xs)
    toList-fromList : ∀ {q : Q A} → q ≈ fromList xs → toList q ≡ xs
    fromList-toList : ∀ {q : Q A} → xs ≡ toList q → fromList xs ≈ q
    toList-enqueue  : ∀ {q : Q A} → toList (enqueue x q) ≡ toList q List.∷ʳ x
    toList-dequeue  : ∀ {q : Q A} → .{{i : False (empty? q)}} →
                      let x , r = dequeue q {{i}} in toList q ≡ x ∷ toList r

[silas-hw]

I think enqueue-suc is good to add as well. And maybe something like

empty-enqueue-dequeue : ∀ {q : Q A} {x : A} → Empty q → proj₁ (dequeue (enqueue x q)) ≡ x

And just generally some more properties on the behaviour of enqueue and dequeue

[silas-hw]

Given toList-enqueue and toList-dequeue, I think _≈_ can be defined generically as

_≈_ : ∀ {A : Set a} → Rel (Q A) a
q ≈ q' = (toList q) ≡ (toList q')

Which is how it is currently defined in TwoList.Base!

But would this mean moving _≈_ to IsQueue? which feels like it somewhat betrays the distinction between RawQueue and IsQueue...

[jamesmckinna]

To maintain 'abstraction', it seemed that simply requiring an implication in the spec was preferably to insisting this be definitional... the fact that the proof of that property is then trivial for TwoList.Base is a bonus...?

Ah.. you think it's definable as _≈_ = _≡_ on toList (see Function.Base._on_) given the toList characterisations? Could be!?

[jamesmckinna]

I think enqueue-suc is good to add as well. And maybe something like

empty-enqueue-dequeue : ∀ {q : Q A} {x : A} → Empty q → proj₁ (dequeue (enqueue x q)) ≡ x

And just generally some more properties on the behaviour of enqueue and dequeue

Hmmm... there is a whole thing here, and I'd like @JacquesCarette and @MatthewDaggitt to weigh in on this, as it's yet another twist on the 'narrow' vs. 'wide' signature for a given 'algebraic specification'. The enqueue-suc property might seems good to have, but it is in any case derivable once you have toList-enqueue, isn't it?

[gallais]

I don't think this will be ergonomic to use as opposed to the
Maybe-returning one.

Note that the List equivalents are all Maybe-based:
https://agda.github.io/agda-stdlib/master/Data.List.Base.html#8038

I'm not against having a dequeue-style variant that always succeeds
by constraining its input but in that case it should be suffixed IMO. We
may also want to go for full-blown size-indexed queues in that case.

[silas-hw]

I'm torn between the two directions myself; I don't have enough 'proof intuition' to know which is best! It's an easy change between the two for the most part, so I'll let other maintainers discuss :-)

[jamesmckinna]

Well, in a way, the definition of dequeue′ as a derived form shows the clunkiness, so in that sense I agree.

I'd understood from @Taneb 's comments above that this was an opportunity for something other than the pure-haskell-ish style, and of course that style is a major influence on the 'core' of stdlib. And yes: on whatever types things should have, in the spec or in any candidate implementation, we should reach a reasonable consensus! But nothing stops us from having the Maybe style...

What name do you think the 'guarded' version should have?

[jamesmckinna]

Oh, and regarding the ergonomics (I've always been a bit shaky on True/False... ;-)), we can simplify this a bit to

dequeue : Q A → Maybe (A × Q A)
dequeue q with isEmpty q in eq
... | true  = nothing
... | false = just (dequeue-guarded q)
  where instance
  _ : T (not (isEmpty q))
  _ rewrite eq = _

for the 'obvious' renamings of everything that has gone before, and unfolding False...

[jamesmckinna]

Maybe this should itself be Data.Queue.TwoList as the top-level (sic) module for this implementation?
Again, up for discussion!

[jamesmckinna]

See below. stdlib style would favour delegating to _≡_ on toList (and then the parentheses would go away... which as already noted, is a global comment on this PR... ;-))

[gallais]

Have we given up on the snoclist?

[jamesmckinna]

Not as such, but there's a hint above that the trade-offs associated with that choice seem to complicate matters?

From the point of view of the API, obviously the choice shouldn't matter, so the question is whether the ergonomics of one choice over the other does matter...?

In each case, it seems as though there will always be some O(n) behaviour associated with the queue smart constructor/fromList, so what would the trade-offs be?

For implementing double-ended queues, there perhaps are clear(er) advantages to a snoclist implementation? And we should surely have such queues as well... esp. given your Okasaki citation for improving the amortized complexity?

[jamesmckinna]

Related (or not?): @gallais your mention of FIFO queues in #480 ... is there more to say about this here?

[silas-hw]

I will try again with SnocList now, but my previous attempts seemed to complicate managing the invariant a lot (namely in that Null doesn't have an equivalent definition for SnocList, so you end up with something along the lines of Null (toList> front) in the invariant).

With the smart constructor, this shouldn't be as much of an issue at all.

May also be a hint that there should SnocList.Properties? But the fact most of that would be a repetition of List.Properties but with SnocList instead smells off to me; is there a better way of handling it than manually re-defining list properties on SnocList?

[silas-hw]

Indeed, I have had difficulty again, all in the lack of a Null< and the messiness of using Null (toList> front). I think it would be an easy change once more is there for SnocList? Due to the scope, I think it's a separate PR deal (which I can help start!)

For now, having List for both seems semi-reasonable, in that at least most users won't ever look at the specific implementation anyway and use the API instead, and that the change will (eventually) be easy to implement.

EDIT: Actually, I think it wouldn't be too much to add just the basic definitions of All< and Null< within this PR?

[gallais]

Null for snoclist should definitely not go via toList>

[jamesmckinna]

Similarly, should this be called null? or isEmpty? or what, in general...

[jamesmckinna]

Don't quite know what happened here; the irrefutable let-binding for the pair worked for me!?

And... for what will probably not be the last time: please please please remove parentheses where you can. (and you can, a lot...)

[silas-hw]

I'll do a big sweep through for parens now! Sorry not catching it.

When trying type check the let binding it gives me Not in scope: r for whatever reason.