The trek goes on

0049

Specifying stack order using parametric types

Posted at 16:29 on 29 January 2026

Continuing 0048, soon I’ve successfully adapted the proof for stacks over the last weekend. Happily, my intuition proves correct: the key step is switching to a more complex concrete model for the indices.

The main difference between the queue and stack interfaces is in the type of push. Recall that the State type family has two indices, which intuitively are the endpoints of a range. If we pop from the left —so a successful pop changes the left index in the state type— then we push into a queue from the right, changing the right index,

Queue.push : ∀ {i j k} → R j k → State i j → State i k

whereas we push into a stack from the left and change the left index:

Stack.push : ∀ {i j k} → R i j → State j k → State i k

It follows that the stack interface never changes the right index, so actually we can switch to a single-index state type family, keeping only the left index:

module _ (I : Set) (i₀ : I) (R : I → I → Set) where

  data ListF (X : I → Set) : I → Set where
    nil  :                         ListF X i₀
    cons : ∀ {i j} → R i j → X j → ListF X i

  record Stack : Set₁ where
    field
      State : I → Set
      empty : State i₀
      push  : ∀ {i j} → R i j → State j → State i
      pop   : ∀ {i} → State i → ListF State i

In the two-index setting, the nil constructor of ListF has type ∀ {i} → ListF X i i, but for stacks the right index is fixed at i₀, so in the single-index setting we should require the (originally left) index to be i₀. As before, we define

PStack : Set₁
PStack = ∀ I i₀ R → Stack I i₀ R

SStack : Set → Set₁
SStack A = Stack ⊤ tt (λ _ _ → A)

inst : PStack → (A : Set) → SStack A
inst St A = St ⊤ tt (λ _ _ → A)

and formulate the bisimilarity theorem only for SStacks instantiated from PStack:

data ListFᴿ {A : Set} {X X' : Set} (Xᴿ : X → X' → Set)
        : ListF ⊤ tt (λ _ _ → A) (λ _ → X ) tt
        → ListF ⊤ tt (λ _ _ → A) (λ _ → X') tt → Set where
  nilᴿ  :                    ListFᴿ Xᴿ  nil        nil
  consᴿ : a ≡ a' → Xᴿ x x' → ListFᴿ Xᴿ (cons a x) (cons a' x')

record Bisim {A : Set} (st st' : SStack A) : Set₁ where
  field
    Stateᴿ : st .State tt → st' .State tt → Set
    emptyᴿ : Stateᴿ (st .empty) (st' .empty)
    pushᴿ  : (a : A) → Stateᴿ s s'
           → Ford² Stateᴿ (st .push a s) (st' .push a s')
    popᴿ   : Stateᴿ s s'
           → Ford² (ListFᴿ Stateᴿ) (st .pop s) (st' .pop s')

bisim : (St St' : PStack) → Param St → Param St'
      → (A : Set) → Bisim (inst St A) (inst St' A)

One minor difference from the queue version is that I decide to employ the principle that ‘Fording’ should be applied and only applied at places where the ‘unifiable-index’ rule is violated. The unifiable-index rule says that we should use only variables and constructors in indices to allow unification to succeed when performing pattern matching. If we need more complex indices, the usual solution is to apply Fording, internalising the index equality and delaying unification when performing pattern matching:

Ford : {I : Set} → (I → Set) → I → Set
Ford P i₀ = ∀ {i} → i ≡ i₀ → P i

In the code above we use the two-index version (definable from the single-index version):

Ford² : {I J : Set} → (I → J → Set) → I → J → Set
Ford² R i₀ j₀ = Ford (λ i → Ford (R i) j₀) i₀

In 0048 Fording was applied in ListFᴿ, whereas here it’s applied in Bisim, where complex indices (the push and pop expressions) actually appear and Fording can be seen to be necessary. The principle is also applied in the definition of unary parametricity:

module _ {I  : Set}         (Iᴾ  : I → Set)
         {i₀ : I}           (i₀ᴾ : Iᴾ i₀)
         {R  : I → I → Set} (Rᴾ  : ∀ {i j} → Iᴾ i → Iᴾ j → R i j → Set)
  where

  data ListFᴾ {X : I → Set} (Xᴾ : ∀ {i} → Iᴾ i → X i → Set)
          : ∀ {i} (iᴾ : Iᴾ i) → ListF I i₀ R X i → Set where
    nilᴾ  : ListFᴾ Xᴾ i₀ᴾ nil
    consᴾ : ∀ {i j} {r : R i j} {x : X j}
          → {iᴾ : Iᴾ i} {jᴾ : Iᴾ j} → Rᴾ iᴾ jᴾ r → Xᴾ jᴾ x
          → ListFᴾ Xᴾ iᴾ (cons r x)

  record Stackᴾ (st : Stack I i₀ R) : Set₁ where
    field
      Stateᴾ : ∀ {i} → Iᴾ i → st .State i → Set
      emptyᴾ : Stateᴾ i₀ᴾ (st .empty)
      pushᴾ  : ∀ {i j} {r : R i j} {s : st .State j}
             → {iᴾ : Iᴾ i} {jᴾ : Iᴾ j} → Rᴾ iᴾ jᴾ r → Stateᴾ jᴾ s
             → Ford (Stateᴾ iᴾ) (st .push r s)
      popᴾ   : ∀ {i} {s : st .State i}
             → {iᴾ : Iᴾ i} → Stateᴾ iᴾ s
             → Ford (ListFᴾ Stateᴾ iᴾ) (st .pop s)

Param : PStack → Set₁
Param St =
  {I  : Set}         (Iᴾ  : I → Set)
  {i₀ : I}           (i₀ᴾ : Iᴾ i₀)
  {R  : I → I → Set} (Rᴾ  : ∀ {i j} → Iᴾ i → Iᴾ j → R i j → Set)
                    → Stackᴾ Iᴾ i₀ᴾ Rᴾ (St I i₀ R)

Applying the principle does help to simplify a bit of code later.

Remark. In general, I’m hoping that someday we can formalise the principle as a theorem explaining the benefit of applying Fording systematically, a subject which 0045 vaguely talked about. And incidentally, I don’t really like naming the programming pattern after Ford because it doesn’t follow the usual scientific naming convention with which we remember the right people to remember, namely the inventors. On the other hand, the name has become fairly standard, and you can’t possibly find a more convenient term than a single-syllable one… (End of remark.)

The index in the state types looks like the height of a stack, and, following the reasoning about CQueue in 0048, one may think that substituting the natural numbers for the parameter I would lead to a more concrete interface that still completely specifies the extensional behaviour, for example

CStack : (ℕ → Set) → Set₁
CStack P = Stack ℕ 0 (λ i j → i ≡ suc j × P i)

But this doesn’t work for stacks because the serial numbers may get reused. For example, let st : CStack P and consider the operation sequence

         s₀ = st .empty
         s₁ = st .push x₁  s₀
cons y₁  s₂ = st .pop      s₁
         s₃ = st .push x₁' s₂
cons y₁' s₄ = st .pop      s₃

where all of x₁, x₁', y₁, and y₁' have type P 1. It’s possible to deduce that y₁ has to be x₁, but y₁' doesn’t have to be x₁': pop is only required to emit an element with a specified serial number; after pushing x₁', the ‘stack’ has been given two elements with serial number 1, and it could choose to cache and emit x₁ for the pop from s₃ rather than emit x₁'.

So we should find a new model so that we can assign distinct serial numbers to pushed elements. One possibility I experimented with is to count the pushed elements in an operation sequence, which is still a natural number — for example in the sequence above, x₁ would be numbered 1 (because it’s the first push), and x₁' would be numbered 2 (because it’s the second push). (We don’t assign 0 to any element, so that we can deduce that it’s impossible to pop an element from a state indexed 0.) We also need to replace the predecessor relation λ i j → i ≡ suc j with a more complex one so that the new state produced by pop has the right index — in the example above we need a relation Pred such that Pred 1 0 and Pred 2 0. However, the definition of this Pred depends on the operation sequence, and this dependence proved to be problematic.

Eventually the model I use is List ℕ. There are two ways of thinking about this model. The first way is that it’s an abstraction of a stack state. Still using the example above:

the empty state is indexed by an empty abstract stack [];
when we push x₁, we push 0 into the abstract stack and assign to x₁ the ‘number’ 0 ∷ [], which I interpret as saying that the element is the 0-th element to be stored at this position of the stack;
when popping from s₁, we also pop from the abstract stack, and s₂ is again indexed by []; at the same time we also push the popped 0 into an (initially empty) residual stack, so that
when pushing x₁', we can look into the residual stack and see that there have been other elements stored at this position, so we pop 0 from the residual stack, push its successor into the abstract stack, and assign to x₁' the ‘number’ 1 ∷ [], meaning that it’s the 1-st element at this position.

We can define this ‘numbering scheme’ in the indices of the data type OpSeq of operation sequences,

data OpSeq (A : Set) : List ℕ → List ℕ → Set where

  emptyOp :     OpSeq A           []        []

  pushOp₀ : A → OpSeq A          stk        []
              → OpSeq A (zero  ∷ stk)       []

  pushOp₁ : A → OpSeq A          stk  (k ∷ res)
              → OpSeq A (suc k ∷ stk)      res

  popOp   :     OpSeq A (    k ∷ stk)      res
              → OpSeq A          stk  (k ∷ res)

so that if pushOpᵢ a ops : OpSeq A stk res then stk is the ‘number’ we assign to a. Formally, the assignments are defined as a PushMap relation (similarly for queues),

data PushMap : OpSeq A stk res → List ℕ → A → Set where
  pushOp₀-here  : {ops : OpSeq A stk []}
                → PushMap (pushOp₀ a ops) (zero  ∷ stk) a
  pushOp₁-here  : {ops : OpSeq A stk (k ∷ res)}
                → PushMap (pushOp₁ a ops) (suc k ∷ stk) a
  pushOp₀-there : PushMap ops ks a' → PushMap (pushOp₀ a ops) ks a'
  pushOp₁-there : PushMap ops ks a' → PushMap (pushOp₁ a ops) ks a'
  popOp         : PushMap ops ks a' → PushMap (popOp     ops) ks a'

and we can prove that the assignments are indeed distinct as a lemma saying that PushMap is a functional relation:

PushMap-functional : PushMap ops ks a → PushMap ops ks a' → a ≡ a'

Assigning abstract stacks is actually a refinement of our initial numbering scheme assigning heights since the length of the abstract stack is the stack height — so the second way of thinking about the refined numbering scheme is that we’re still numbering the elements with stack heights, but the suc constructors are suitably decorated (and become _∷_ constructors) so that we never assign the same number twice. And note that the predecessor relation for these numbers is just tail, whose definition doesn’t depend on an operation sequence.

The rest is largely the same as the queue proof. First define

record BisimState {A : Set} (st st' : SStack A)
                  (s : st .State tt) (s' : st' .State tt) : Set where
  constructor bisimState
  field
    {stk res} : List ℕ
    ops  : OpSeq A stk res
    run  : RunOpSeq ops st  s
    run' : RunOpSeq ops st' s'

where

data RunOpSeq : OpSeq A stk res → (st : SStack A)
              → st .State tt → Set where
  emptyOp : st .empty ≡ s
          → RunOpSeq emptyOp st s
  pushOp₀ : RunOpSeq ops st s → st .push a s ≡ t
          → RunOpSeq (pushOp₀ a ops) st t
  pushOp₁ : RunOpSeq ops st s → st .push a s ≡ t
          → RunOpSeq (pushOp₁ a ops) st t
  popOp   : RunOpSeq ops st s → st .pop s ≡ cons a t
          → RunOpSeq (popOp ops) st t

so that we can start filling in bisim, where again the emptyᴿ/pushᴿ case starts/extends the operation sequence in BisimState:

bisim : (St St' : PStack) → Param St → Param St'
      → (A : Set) → Bisim (inst St A) (inst St' A)
bisim St St' param param' A = record
  { Stateᴿ = BisimState st st'
  ; emptyᴿ = bisimState emptyOp
                       (emptyOp refl)
                       (emptyOp refl)
  ; pushᴿ  = λ { a (bisimState {_} {[]} ops run run') refl refl →
                    bisimState (pushOp₀ a ops)
                               (pushOp₀ run  refl)
                               (pushOp₀ run' refl)
               ; a (bisimState {_} {k ∷ res} ops run run') refl refl →
                    bisimState (pushOp₁ a ops)
                               (pushOp₁ run  refl)
                               (pushOp₁ run' refl)
               }
  ; popᴿ   = popᴿ-proof
  }
  where

  st st' : SStack A
  st  = inst St  A
  st' = inst St' A

  popᴿ-proof :
      BisimState st st' s s'
    → Ford² (ListFᴿ (BisimState st st')) (st .pop s) (st' .pop s')
  popᴿ-proof (bisimState ops run run') eq eq' = ?

In popᴿ-proof we invoke unary parametricity proofs param and param' to create CCStacks defined by

CCStack : SStack A → OpSeq A stk res → Set₁
CCStack st ops = Stackᴾ (λ _ → List ℕ)
                        []
                        (λ ks ks' a → (∃ λ k → ks ≡ k ∷ ks')
                                    × PushMap ops ks a)
                        st

fast-forward their states using

simulate : {ops : OpSeq A stk res} → RunOpSeq ops st s
         → (stᴾ : CCStack st ops) → stᴾ .Stateᴾ stk s

and then pop from the resulting states, on which we perform a case analysis:

popᴿ-proof :
    BisimState st st' s s'
  → Ford² (ListFᴿ (BisimState st st')) (st .pop s) (st' .pop s')
popᴿ-proof (bisimState ops run run') eq eq'
  with stᴾ  ← CCStack st  ops ∋ param  _ _ _
     | st'ᴾ ← CCStack st' ops ∋ param' _ _ _
     | stᴾ  .popᴾ (simulate run  stᴾ ) eq
     | st'ᴾ .popᴾ (simulate run' st'ᴾ) eq'
...  | nilᴾ                     | nilᴾ                      = ?
...  | nilᴾ                     | consᴾ ((_ , kseq) , m') _ = ?
...  | consᴾ ((_ , kseq) , m) _ | nilᴾ                      = ?
...  | consᴾ ((_ , refl) , m) _ | consᴾ ((_ , refl) , m') _ = ?

When invoking popᴾ, since we Forded the type of popᴾ instead of nilᴾ and consᴾ, a single equality constraint eq is prepared outside and passed in as an argument as opposed to letting the nilᴾ and consᴾ patterns below carry their own equality proofs (as in the queue proof), which looks messier. Moreover, eq : i ≡ st .pop s arises from the type of popᴿ, where the complex index st .pop s first appears and is Forded; as the constraint gets passed into popᴾ and unified, it’s the variable i introduced by Fording the type of popᴿ that’s unified, so, for example, in the nilᴾ-nilᴾ case the type of eq specialises to nil ≡ st .pop s —and similarly for eq'— and the goal type becomes ListFᴿ (BisimState st st') nil nil, which we can directly discharge with nilᴿ. That is, we Ford the goal type, obtaining some equality constraints about the indices, which then get sufficiently specialised by unification so that the goal type becomes dischargeable.

In the cases where one state matches nilᴾ and the other matches consᴾ, since the indices (that is, the decorated heights) of the two states are the same (as guaranteed by simulate), matching one state with nilᴾ means that the shared index is [], so from the other state we somehow successfully pops an element numbered [], but this is impossible because we don’t assign [] to any element —that is, the type of m/m' has form PushMap ops [] a, which can be proved to be uninhabited— or more simply, any number we assign should have a predecessor but [] has no predecessor — that is, the type of kseq has form [] ≡ k ∷ ks, which is obviously uninhabited.

The consᴾ-consᴾ case is the same as the queue proof: both sides pop elements with the same number, and then PushMap-functional m m' proves that the two elements are equal; finally we extend the operation sequence in BisimState to relate the two new states.

popᴿ-proof :
    BisimState st st' s s'
  → Ford² (ListFᴿ (BisimState st st')) (st .pop s) (st' .pop s')
popᴿ-proof (bisimState ops run run') eq eq'
  with stᴾ  ← CCStack st  ops ∋ param  _ _ _
     | st'ᴾ ← CCStack st' ops ∋ param' _ _ _
     | stᴾ  .popᴾ (simulate run  stᴾ ) eq
     | st'ᴾ .popᴾ (simulate run' st'ᴾ) eq'
...  | nilᴾ                     | nilᴾ                      = nilᴿ
...  | nilᴾ                     | consᴾ ((_ , ()  ) , _ ) _
...  | consᴾ ((_ , ()  ) , _) _ | nilᴾ
...  | consᴾ ((_ , refl) , m) _ | consᴾ ((_ , refl) , m') _ =
  consᴿ (PushMap-functional m m')
        (bisimState (popOp ops)
                    (popOp run  (sym eq ))
                    (popOp run' (sym eq')))

Even though the stack proof is more complex (some of the complexity is not shown in this post — for example, PushMap-functional is more difficult to prove than for queues), it’s actually less useful than the queue proof because the stack interface is easily and optimally implementable using lists in a functional setting, and we don’t seem to need to consider other implementations. I think the role of this proof is to pave the way for a deque proof, which will probably be significantly harder but also more useful, covering more implementations. But I really have to get back to revising my unloved paper with Shin for (the soon-to-be-reborn) JFP.

Acknowledgements. I’ve been writing Agda in VS Code for several years, but in recent months the Agda input method has become so broken (with the cursor drifting uncontrollably) that I started to consider switching back to emacs. Just when I had that thought, my former assistant Zong-You Shih ported the Agda input method to macOS as a native input method called Unicorn, with which the Agda programs behind this post are happily written (and the cursor feels stable again). A big thanks to Zong-You as well as all the Agda developers, who have made and kept programming in Agda a joy. (End of acknowledgements.)

Agda file: Stack.agda