Add Queue datatype by silas-hw · Pull Request #3084 · agda/agda-stdlib

silas-hw · 2026-07-20T21:29:45Z

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 · 2026-07-21T01:36:26Z

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 · 2026-07-21T01:48:34Z

+toList empty = []
+toList (queue dq-hd dq-tail eq) = dq-hd ∷ (dq-tail ++ (reverse eq))
+
+-- Create a Queue from a List, such that the elements


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 · 2026-07-21T12:30:09Z

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 · 2026-07-21T12:54:02Z

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

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

…queue

gallais · 2026-07-27T22:19:23Z

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

silas-hw · 2026-07-27T22:37:38Z

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 · 2026-07-28T03:19:16Z

* ... 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 · 2026-07-28T03:22:14Z

+    empty-toList   : toList (empty {A = A}) ≡ []
+    fromList-empty : empty {A = A} ≈ fromList []


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!

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

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

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

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!?

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?

See also @MatthewDaggitt 's comment on #1552 ... it seems my instinct towards minimality/definitional extension may be at odds with usability. So a design more akin to that introduced as Effect.Foldable.RawFoldable{WithDefaults} might be more suitable?

I like the general idea of Effect.Foldable.RawFoldable{WithDefaults} a lot, but wonder if there's an approach that doesn't require two records?

Obviously, native 'defaults' would be nice, but in is place, maybe a function/constructor that could take an implementation of the minimal interface and fill in the 'defaults'?

For lemmas/proofs, maybe there's also room to consider what should just be generic properties of Queues and not part of the interface, such that they would be placed in say Queue.Properties.

All open to discussion!

gallais · 2026-07-28T12:55:11Z

+... | []            = queue (x ∷ []) []
+... | front@(_ ∷ _) = queue front (x ∷ bs)
+
+dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A


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.

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 :-)

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?

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

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

jamesmckinna · 2026-07-28T13:57:35Z

+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue where


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

As in have a file Data/Queue/TwoList.agda with this content?

Indeed, this file itself will be changed to not just have TwoList.Base imported, and will then likely import Data,Queue.TwoList instead?

jamesmckinna · 2026-07-28T14:46:37Z

+  to𝔹 : Q A → Bool
+  to𝔹 = isYes ∘ empty?


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

silas-hw · 2026-07-29T22:31:02Z

Note: sorry for pushing a file with holes in!

gallais · 2026-07-30T14:35:12Z

-  {!!} ≡⟨⟩
-  {!!}
+  ++-[] : ∀ {xs ys : List A} → (xs ++ ys) ≡ [] → ys ≡ []
+  ++-[] {xs = []} {ys = []} xs++ys≡[] = xs++ys≡[]


Note that the equivalent properties in Data.Nat.Properties have more complex names:

m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0 m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0

I personally would expect ++-[] to be a proof that xs ++ [] ≡ xs

There are two hard things in computer science...

Descriptive names is definitely something I need to get a hold of!

silas-hw added 4 commits July 20, 2026 17:01

Add definition of Queue and basic operations

4905cc6

Add top-level Queue module

4125b12

Add some basic functions

bf7790b

Add singleton function

d26d47c

silas-hw marked this pull request as draft July 20, 2026 21:29

silas-hw marked this pull request as ready for review July 20, 2026 21:32

JacquesCarette requested changes Jul 21, 2026

View reviewed changes

jamesmckinna reviewed Jul 21, 2026

View reviewed changes

Comment thread src/Data/Queue/Base.agda Outdated

Comment thread src/Data/Queue/Base.agda Outdated

Comment thread src/Data/Queue/Base.agda Outdated

silas-hw marked this pull request as draft July 21, 2026 14:03

silas-hw added 9 commits July 21, 2026 10:09

Fix imports

6a8bf86

Rename l : Level -> a : Level

9056b95

Use two levels instead of one

85e54c5

Refactor Queue to use record definition

95be562

Refactor Queue to use record definition

bebe5a2

Cleanup

9ef66fb

Add properties file

a0b0353

Use record syntax in dequeue and enqueue

253edac

Fix comment

100d5db

jamesmckinna reviewed Jul 22, 2026

View reviewed changes

Comment thread src/Data/Queue/Base.agda Outdated

jamesmckinna reviewed Jul 22, 2026

View reviewed changes

Comment thread src/Data/Queue/Base.agda Outdated

jamesmckinna reviewed Jul 22, 2026

View reviewed changes

Comment thread src/Data/Queue/Base.agda Outdated

jamesmckinna reviewed Jul 22, 2026

View reviewed changes

Comment thread src/Data/Queue/Base.agda Outdated

silas-hw and others added 5 commits July 22, 2026 11:18

Fix typo in 'amortized'

e3f8872

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Use as-pattern in enqueue

48b6afd

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Merge branch 'queue' of https://github.com/silas-hw/agda-stdlib into …

86bed0a

…queue

Use ⊥-elim on impossible dequeue case

0bf49e7

Update argument order for enqueue

0561f10

silas-hw added 3 commits July 27, 2026 19:01

Add approx relation

41e76dd

Remove stale file

c2246b4

Fix whitespace

e8ff3b8

jamesmckinna reviewed Jul 28, 2026

View reviewed changes

Comment thread src/Data/Queue/TwoList/Base.agda Outdated

gallais reviewed Jul 28, 2026

View reviewed changes

Cleanup dequeue on TwoList

e2cc2c8

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

jamesmckinna reviewed Jul 28, 2026

View reviewed changes

Comment thread src/Data/Queue/TwoList/Base.agda

Add properties to IsQueue

e790193

gallais reviewed Jul 28, 2026

View reviewed changes

Comment thread src/Data/Queue/TwoList/Base.agda

jamesmckinna reviewed Jul 28, 2026

View reviewed changes

Comment thread src/Data/Queue/QueueSpec.agda Outdated

jamesmckinna reviewed Jul 28, 2026

View reviewed changes

silas-hw added 2 commits July 28, 2026 13:05

Fix Properties to use new definitions in QueueSpec

6a717da

Prove IsEquivalence of ≈

d1a9ea9

jamesmckinna reviewed Jul 29, 2026

View reviewed changes

Comment thread src/Data/Queue/QueueSpec.agda Outdated

jamesmckinna and others added 6 commits July 29, 2026 10:19

fix: whitespace

2ec3eaa

Cleanup code

99fc8f1

Add All< and Null<

6fe776f

Update TwoList Queue to use SnocList

0512a11

Fix whitespace

009697c

Cleanup code

b4e1ec7

jamesmckinna mentioned this pull request Jul 29, 2026

Adding priority queue implementation #1542

Open

Fix whitespace

07212a4

Prove ≈-resp-Empty on TwoList

84d517b

gallais reviewed Jul 30, 2026

View reviewed changes

		empty-toList : toList (empty {A = A}) ≡ []
		fromList-empty : empty {A = A} ≈ fromList []

Uh oh!

Conversation

silas-hw commented Jul 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette commented Jul 21, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

gallais commented Jul 21, 2026

Uh oh!

jamesmckinna commented Jul 21, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

gallais commented Jul 27, 2026

Uh oh!

silas-hw commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Jul 28, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

silas-hw commented Jul 20, 2026 •

edited

Loading

jamesmckinna left a comment •

edited

Loading

silas-hw commented Jul 27, 2026 •

edited

Loading

jamesmckinna Jul 28, 2026 •

edited

Loading

jamesmckinna Jul 28, 2026 •

edited

Loading

jamesmckinna Jul 28, 2026 •

edited

Loading