Agda Patience Sort

Having recently decided to learn myself an Agda, I thought that implementing a Patience sort would be a neat example to try and program. Having already implemented a Scala Patience sort, I was interested to see how I could tighten up the implementation by using a dependently-typed language such as Agda.

I'm going to go reasonably fast when describing my implementation, feel free to take a look at the same file on Github if you'd like to explore it using the excellent Emacs agda-mode.

First, let's define the module, and import a bunch of stuff from the standard library.

module Patience where
  open import Relation.Binary using (DecTotalOrder; module DecTotalOrder;
    IsDecTotalOrder; module IsDecTotalOrder; Rel; module IsTotalOrder;
    module IsPartialOrder; module IsPreorder)
  open import Relation.Binary.Core hiding (refl)
  open import Level hiding (_⊔_ ; suc) renaming (zero to lzero)
  open import Data.Nat using (ℕ; z≤n; s≤s; suc; _+_)
    renaming (decTotalOrder to decTotalOrderℕ; _≤_ to _≤ℕ_)
  open import Data.List using (List; []; _∷_)
  open import Data.Product using (Σ; _,_; _×_)
  open import Function using (_∘_)
  open import Data.Sum using (inj₁; inj₂)
  open import Data.Nat.Properties.Simple using (+-suc; +-assoc; +-comm)
  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; subst; cong; sym)
  open PropEq.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)

Now, using a total-ordered set, X, I create a "lifted" data-type that adds a maximum element to X. I create an ordering on the lifted type (i.e. that compares all elements as less than the maximum, and otherwise defers to the underlying ordering), and prove that it is transitive. I could prove other properties, but do not require them, so save space by not doing so.

  -- A module that will contain a type of ordered "piles", analogous
  -- to piles of cards in Patience (though with the stronger
  -- restriction that piles are ordered by the top element).
  module Piles (dto : DecTotalOrder lzero lzero lzero) where
    open DecTotalOrder dto public renaming (Carrier to X)

    -- Append maximum element to X
    data X⊤ : Set where
      ⊤ : X⊤
      ⟦_⟧ : (x : X) → X⊤ -- lift an element of X

    -- Define an ordering relation on the resulting type
    data _⟦≤⟧_ : Rel X⊤ Level.zero where
      x≤⊤ : ∀ {x} → x ⟦≤⟧ ⊤
      ⟦_⟧ : ∀ {x y} → (x ≤ y) → ⟦ x ⟧ ⟦≤⟧ ⟦ y ⟧ -- lift an ordering on X

    -- Ensure the order is transitive
    ⟦≤⟧-trans : Transitive _⟦≤⟧_
    ⟦≤⟧-trans _ x≤⊤ = x≤⊤
    ⟦≤⟧-trans ⟦ p ⟧ ⟦ q ⟧ =  ⟦ trans p q ⟧

We will want to use this lifted type to track the minimum element in a set of Piles, and we will therefore need to find the minimum of two elements of this type.

    -- Minimum w.r.t. X⊤
    min : X⊤ → X⊤ → X⊤
    min ⊤ x = x
    min x ⊤ = x
    min ⟦ x ⟧ ⟦ y ⟧ with total x y
    ... | inj₁ x≤y = ⟦ x ⟧
    ... | inj₂ y≤x = ⟦ y ⟧

We can now define a type of ordered vectors, which records the number of elements it contains. Notice how we leverage dependent types, taking a proof object argument that ensures that elements that are consd onto the vector are indeed smaller than the existing head of the vector.

    -- Define a type of bounded, ordered vectors
    data OVec : X⊤ → ℕ → Set where
      ε : OVec ⊤ 0
      cons : ∀ {t n} → (x : X) → (⟦ x ⟧ ⟦≤⟧ t) → OVec t n → OVec ⟦ x ⟧ (suc n)

Now, using ordered vectors (individual piles), we can define a type representing a (ordered by top element) set of piles, again tracking the minimum element and the number of elements in the Piles.

    -- Define a type of bounded, ordered (by head elem) vectors of
    -- (non-empty) OVecs.
    data Piles : X⊤ → ℕ → Set where
      ε : Piles ⊤ 0
      consP : ∀{x t n m} → OVec ⟦ x ⟧ (suc n) → (⟦ x ⟧ ⟦≤⟧ t) → Piles t m
        → Piles ⟦ x ⟧ (suc n + m)

Later, we will require a couple of lemmas:

    -- Given a proof of equivalence between two elements of ℕ, we can transform
    -- Piles with one size to the other.
    cong-Piles : ∀ {l} {n m : ℕ} → (n ≡ m) → Piles l n  → Piles l m
    cong-Piles {l} p fn = subst (Piles l) p fn

    ⟦≤⟧-resp-min : ∀ {x y z} → x ⟦≤⟧ y → x ⟦≤⟧ z → x ⟦≤⟧ (min y z)
    ⟦≤⟧-resp-min x≤⊤ q = q
    ⟦≤⟧-resp-min ⟦ p ⟧ x≤⊤ = ⟦ p ⟧
    ⟦≤⟧-resp-min {_} {⟦ y ⟧} {⟦ z ⟧} p q with total y z
    ... | inj₁ y≤z = p
    ... | inj₂ z≤y = q

And now, we can move onto the meat of the implementation, inserting single elements, and complete piles into existing (possibly empty) Piles:

    -- We can insert a single element into existing Piles...
    insertElemPiles : ∀ {l n} → (x : X) → Piles l n
      → Piles (min ⟦ x ⟧ l) (suc n)
    insertElemPiles x ε = consP (cons x x≤⊤ ε) x≤⊤ ε
    insertElemPiles x (consP {x′} {t} {n} {m} p x′≤t ps) with total x x′
    ... | inj₁ x≤x′ = consP (cons x ⟦x≤x′⟧ p) (⟦≤⟧-trans ⟦x≤x′⟧ x′≤t) ps
      where
        ⟦x≤x′⟧ = ⟦ x≤x′ ⟧
    ... | inj₂ x′≤x = cong-Piles ≡ℕ (consP p (⟦≤⟧-resp-min ⟦ x′≤x ⟧ x′≤t) rec)
      where
        rec = insertElemPiles x ps

        ≡ℕ : suc (n + suc m) ≡ suc (suc (n + m))
        ≡ℕ = cong suc (+-suc n m)

    -- ...and insert a Pile into Piles.
    insertPilePiles : ∀ {x t n m} → OVec ⟦ x ⟧ (suc n)
      → Piles t m → Piles (min ⟦ x ⟧ t) (suc n + m)
    insertPilePiles {t = ⊤} p ε = consP p x≤⊤ ε
    insertPilePiles {x} {⟦ t ⟧} {n₁} p (consP {n = n₂} {m = m₁} q x≤t′ qs)
      with total x t
    ... | inj₁ x≤t = consP p ⟦ x≤t ⟧ (consP q x≤t′ qs)
    ... | inj₂ t≤x = cong-Piles ≡ℕ (consP q (⟦≤⟧-resp-min ⟦ t≤x ⟧ x≤t′) rec)
      where
       rec = insertPilePiles p qs

       -- Since we build the piles in two different ways, we need to
       -- prove that the sizes are equivalent, using this lemma about ℕ.
       permute-suc-xyz : {x y z : ℕ} → x + suc (y + z) ≡ y + suc (x + z)
       permute-suc-xyz {x} {y} {z} =
         begin
          x + suc (y + z)
         ≡⟨ +-suc x (y + z) ⟩
          suc (x + (y + z))
         ≡⟨ cong suc (sym (+-assoc x y z)) ⟩
         suc ((x + y) + z)
         ≡⟨ cong suc (cong (λ x → x + z) (+-comm x y)) ⟩
         suc ((y + x) + z)
         ≡⟨ cong suc (+-assoc y x z) ⟩
         suc (y + (x + z))
         ≡⟨ sym (+-suc y (x + z)) ⟩
         y + suc (x + z)
         ∎

       ≡ℕ = cong suc (permute-suc-xyz {n₂} {n₁} {m₁})

It'd be nice to use some of Connor McBride's ideas to avoid the Green Slime1 (i.e. the use of min in the return types). However, I seem to require the tight bounds, and didn't manage to effectively get rid of the calls to min. If you have any ideas or suggestions on this, please get in contact!

Once we have inserted elements into Piles, we can remove elements one-by-one, to obtain an ordered List of elements. When removing a single element (to obtain the minimum element and a new Piles), we have to use a dependent-sum type to encode the fact that the lower bound of the resulting Piles is the removed element. We maintain the ordering by pushing any non-empty vectors back into the Piles to be consumed in-order.

    -- From any non-empty Piles, we can remove the smallest element, to obtain
    -- a pair of that element, and a one-smaller Piles.
    removeOne : ∀ {l n} → Piles l (suc n) → X × (Σ X⊤ (λ l' → Piles l' n))
    removeOne (consP (cons x _ xs) _ ps) with xs
    ... | ε = x , _ , ps
    ... | cons y q ys = x , _ , insertPilePiles (cons y q ys) ps

    -- By repeatedly removing a single element, we can convert Piles in a List.
    pilesToList : ∀ {l n} → Piles l n → List X
    pilesToList ε = []
    pilesToList {n = suc m} p with removeOne p
    ... | x , _ , ps = x ∷ pilesToList ps

When converting an arbitrary list of elements into Piles, we cannot up-front know the lower bound or size of the Piles, thus we can use an existential type to "hide" these values. To create a existential Piles, we repeatedly insert the elements of the list, one-by-one:

    -- We can existentially hide the bound and size of Piles...
    data ∃Piles : Set where
      ∃<_> : ∀ {l n} → Piles l n → ∃Piles

    -- ...and can convert an arbitrary List into a Piles with unknown bound and
    -- size, by repeatedly inserting one element at a time.
    listToPiles : List X → ∃Piles
    listToPiles [] = ∃< ε >
    listToPiles (x ∷ xs) with listToPiles xs
    ... | ∃< ps > = ∃< insertElemPiles x ps >

Now, Patience sorting is simply defined:

    -- Finally, patience sort is simply creating Piles from an arbitrary List,
    -- before converting back to an (ordered) List.
    patienceSort : List X → List X
    patienceSort ls with listToPiles ls
    ... | ∃< ps > = pilesToList ps

And all that remains is to demonstrate some example sortings of natural numbers. Recall that Piles are parameterised by the (totally-ordered) elements they contain.

  -- Let's create Piles of ℕ
  module Pilesℕ = Piles decTotalOrderℕ

  -- and some test lists.
  xs = Pilesℕ.patienceSort (5 ∷ 4 ∷ 3 ∷ 2 ∷ 1 ∷ [])
  ys = Pilesℕ.patienceSort []
  zs = Pilesℕ.patienceSort (4 ∷ 4 ∷ 1 ∷ 5 ∷ 3 ∷ [])

  sortedXs sortedYs sortedZs : List ℕ
  sortedXs = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []
  sortedYs = []
  sortedZs = 1 ∷ 3 ∷ 4 ∷ 4 ∷ 5 ∷ []

  -- And check that sorting via patience does the right thing.
  xsOk : xs ≡ sortedXs
  xsOk = PropEq.refl

  ysOk : ys ≡ sortedYs
  ysOk = PropEq.refl

  zsOk : zs ≡ sortedZs
  zsOk = PropEq.refl

  1. Functions are highlighted in Green in Agda. Such functions are "opaque" to Agda when performing unification, and are discouraged from being used in data type indices such as here, hence the term "Green Slime". ↩