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]

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

[jamesmckinna]

hmmm... circular dependencies? Does splitting the Spec module into two help at all?

[silas-hw]

I think it would rather be splitting Instances. I.e. have TwoList-RawQueue defined as an instance somewhere, have that imported into Properties, which can then be imported into some module that defines TwoList-IsQueue - but this does go against the current style.

Or maybe moving the definitions used in the instance of IsQueue to the Instances file itself, but this would result in a Instances file containing mostly properties.

[jamesmckinna]

Can these be refactored to make use of the lemmas added in #3091

[jamesmckinna]

The operative word here is 'bundle'.

I think that IsQueue, even if only for consistency with existing distinctions between 'structure' and 'bundle' (eg. see #3052), should be considered as a structure, and thus parametrised on Q and the rawQ : RawQueue Q .

A bundled Queue would then be a record with three fields:

• the type constructor Q
• its associated rawQ
• the proof that it, indeed, satisfies IsQueue

Cf. #2252

[jamesmckinna]

Oh, and a propos @JacquesCarette 's jeremiad in #3052 we should perhaps consider instead write QueueSig rather than RawQueue...?

[silas-hw]

I see! And from the perspective of a relatively new developer, XSig is more immediately obvious than RawQueue, so I'm in favor of that

[silas-hw]

And for the bundle, how about 'lifting' the Sig functions to be on the bundle itself?, e.g.

record Queue (A : Set a) : Set (suc a) where
  field
    Q : Set a → Set a
    q : Q A
    rawQueue : RawQueue A Q
    isQueue : IsQueue A rawQueue

open Queue

-- 'lifted' functions
enqueue  : {a : Level} → {A : Set a} → A → Queue A → Queue A
enqueue x q' = record { Q = q' .Q ; q = RawQueue.enqueue (q' .rawQueue) x (q' .q) ; rawQueue = q' .rawQueue ; isQueue = q' .isQueue }

Is there some nice automatic way of doing this?

[jamesmckinna]

Ooh. Maybe I was too hasty/casual in my suggestion above regarding the bundle (I think the structure story makes sense)...

Is it obviously a good idea to allow the basic operations potentially to change the underlying type constructor Q upon each invocation? (your suggested lifted versions obviously do not, but it isn't ruled out for the implied API defined by the bundled version?)

Perhaps some more thought required?