Merge sort in agda

Question

There are at least three ways in which you can write merge sort so that it passes the termination checker.

First of all, here's what we need to make our merge sort generic:

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module MergeSort
  {ℓ a} {A : Set a}
  {_<_ : Rel A ℓ}
  (strictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open IsStrictTotalOrder strictTotalOrder

Once we prove that some relation is a strict total order, we can use that proof as a parameter to this module and get corresponding merge sort.

The first way is to use well-founded recursion, which is more or less what the linked code in your question uses. However, we do not need to prove that merge sort returns a sorted permutation of its input list in a bounded number of comparisions, so we can cut most of the code.

I wrote something about well-founded recursion in this answer, you might want to check it out.

Other imports first:

open import Data.List
open import Data.Nat
  hiding (compare)
open import Data.Product
open import Function
open import Induction.Nat
open import Induction.WellFounded

Here's the implementation of merge:

merge : (xs ys : List A) → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with compare x y
... | tri< _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri≈ _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri> _ _ _ = y ∷ merge (x ∷ xs) ys

If you are having problems getting this past termination checker, check out my answer on this. It should work as is with the development version of Agda.

split is easy as well:

split : List A → List A × List A
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l

But now we get to the complicated part. We need to show that split returns two lists that are both smaller than the original (which of course holds only if the original list had at least two elements). For this purpose, we define a new relation on lists: xs <ₗ ys holds iff length x < length y:

_<ₗ_ : Rel (List A) _
_<ₗ_ = _<′_ on length

The proof is then fairly straightforward, it's just an induction on the list:

-- Lemma.
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl     = ≤′-refl
s≤′s (≤′-step p) = ≤′-step (s≤′s p)

split-less : ∀ (x : A) y ys →
  let xs    = x ∷ y ∷ ys
      l , r = split (x ∷ y ∷ ys)
  in l <ₗ xs × r <ₗ xs
split-less _ _ [] = ≤′-refl , ≤′-refl
split-less _ _ (_ ∷ []) = ≤′-refl , ≤′-step ≤′-refl
split-less _ _ (x ∷ y ∷ ys) with split-less x y ys
... | p₁ , p₂ = ≤′-step (s≤′s p₁) , ≤′-step (s≤′s p₂)

Now we have everything we need in order to bring the well-founded recursion machinery. Standard library gives us proof that _<′_ is well-founded relation, we can use this to construct a proof that our freshly defined _<ₗ_ is also well-founded:

open Inverse-image {A = List A} {_<_ = _<′_} length
  renaming (well-founded to <ₗ-well-founded)

open All (<ₗ-well-founded <-well-founded)
  renaming (wfRec to <ₗ-rec)

And finally, we use <ₗ-rec to write merge-sort.

merge-sort : List A → List A
merge-sort = <ₗ-rec _ _ go
  where
  go : (xs : List A) → (∀ ys → ys <ₗ xs → List A) → List A
  go [] rec = []
  go (x ∷ []) rec = x ∷ []
  go (x ∷ y ∷ ys) rec =
    let (l , r)   = split (x ∷ y ∷ ys)
        (p₁ , p₂) = split-less x y ys
    in merge (rec l p₁) (rec r p₂)

Notice that in the recursive call (rec), we not only specify what to recurse on, but also a proof that the argument is smaller than the original one.

The second way is to use sized types. I also wrote an overview in this answer, so you might want to check it out.

We need this pragma at the top of the file:

{-# OPTIONS --sized-types #-}

And a different set of imports:

open import Data.Product
open import Function
open import Size

However, we cannot reuse lists from standard library since they do not use sized types. Let's define our own version:

infixr 5 _∷_

data List {a} (A : Set a) : {ι : Size} → Set a where
  []  : ∀ {ι} →                  List A {↑ ι}
  _∷_ : ∀ {ι} → A → List A {ι} → List A {↑ ι}

merge stay more or less the same, we only need to change the type a bit to convince the termination checker:

merge : ∀ {ι} → List A {ι} → List A → List A

However, split has a slight but very important change:

split : ∀ {ι} → List A {ι} → List A {ι} × List A {ι}
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l

The implementation stays the same, but the type changed. What this change does is that it tells Agda that split is size-preserving. This means that the two resulting lists cannot be larger than the input one. merge-sort then looks very natural:

merge-sort : ∀ {ι} → List A {ι} → List A
merge-sort [] = []
merge-sort (x ∷ []) = x ∷ []
merge-sort (x ∷ y ∷ ys) =
  let l , r = split ys
  in  merge (merge-sort (x ∷ l)) (merge-sort (y ∷ r))

And indeed, this gets past the termination checker. The trick is the above mentioned size-preserving property: Agda can see that split ys does not produce lists larger than ys and thus x ∷ l and y ∷ r are both smaller than x ∷ y ∷ ys. This is enough to convince the termination checker.

The last one is not really a merge sort in the usual sense. It uses the same idea but instead of repeatedly splitting the lists, recursively sorting them and then merging them together, it does all the splitting upfront, stores the results in a tree and then folds the tree using merge.

However, since this answer is already fairly long, I'll just give you a link.