Termination-checking of function over a trie

agda, recursion, termination, trie

Solution

The inline/fuse trick can be applied in (perhaps) surprising way. This trick is suited for problems of this sort:

data Trie (A : Set) : Set where
  nil  :                     Trie A
  node : A → List (Trie A) → Trie A

map-trie : {A B : Set} → (A → B) → Trie A → Trie B
map-trie f nil = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

This function is structurally recursive, but in a hidden way. `map` just applies `map-trie f` to the elements of `xs`, so `map-trie` gets applied to smaller (sub-)tries. But Agda doesn't look through the definition of `map` to see that it doesn't do anything funky. So we must apply the inline/fuse trick to get it past termination checker:

map-trie : {A B : Set} → (A → B) → Trie A → Trie B
map-trie         f nil = nil
map-trie {A} {B} f (node x xs) = node (f x) (map′ xs)
  where
  map′ : List (Trie A) → List (Trie B)
  map′ [] = []
  map′ (x ∷ xs) = map-trie f x ∷ map′ xs

Your `fmap` function shares the same structure, you map a lifted function of some sort. But what to inline? If we follow the example above, we should inline `fmap` itself. This looks and feels a bit strange, but indeed, it works:

fmap fmap′ : ∀ {a} {A B : Set a} {τ} → (A → B) → τ ▷ A → τ ▷ B

fmap  f (〈〉 x) = 〈〉 (f x)
fmap  f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕
fmap  f (↑ σ) = ↑ (fmap (fmap′ f) σ)
fmap  f (roll σ) = roll (fmap f σ)

fmap′ f (〈〉 x) = 〈〉 (f x)
fmap′ f 〔 σ₁ , σ₂ 〕 = 〔 fmap′ f σ₁ , fmap′ f σ₂ 〕
fmap′ f (↑ σ) = ↑ (fmap′ (fmap f) σ)
fmap′ f (roll σ) = roll (fmap′ f σ)

There's another technique you can apply: it's called sized types. Instead of relying on the compiler to figure out when somethig is or is not structurally recursive, you instead specify it directly. However, you have to index your data types by a `Size` type, so this approach is fairly intrusive and cannot be applied to already existing types, but I think it is worth mentioning.

In its simplest form, sized type behaves as a type indexed by a natural number. This index specifies the upper bound of structural size. You can think of this as an upper bound for the height of a tree (given that the data type is an F-branching tree for some functor F). Sized version of `List` looks almost like a `Vec`, for example:

data SizedList (A : Set) : ℕ → Set where
  []  : ∀ {n} → SizedList A n
  _∷_ : ∀ {n} → A → SizedList A n → SizedList A (suc n)

But sized types add few features that make them easier to use. You have a constant `∞` for the case when you don't care about the size. `suc` is called `↑` and Agda implements few rules, such as `↑ ∞ = ∞`.

Let's rewrite the `Trie` example to use sized types. We need a pragma at the top of the file and one import:

{-# OPTIONS --sized-types #-}
open import Size

And here's the modified data type:

data Trie (A : Set) : {i : Size} → Set where
  nil  : ∀ {i}                         → Trie A {↑ i}
  node : ∀ {i} → A → List (Trie A {i}) → Trie A {↑ i}

If you leave the `map-trie` function as is, the termination checker is still going to complain. That's because when you don't specify any size, Agda will fill in infinity (i.e. don't-care value) and we are back at the beginning.

However, we can mark `map-trie` as size-preserving:

map-trie : ∀ {i A B} → (A → B) → Trie A {i} → Trie B {i}
map-trie f nil         = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

So, if you give it a `Trie` bounded by `i`, it will give you another `Trie` bounded by `i` as well. So `map-trie` can never make the `Trie` larger, only equally large or smaller. This is enough for the termination checker to figure out that `map (map-trie f) xs` is okay.

This technique can also be applied to your `Trie`:

open import Size
  renaming (↑_ to ^_)

data Trie {} (A : Set ) : {i : Size} → Type → Set  where
  〈〉    : ∀ {i} → A →
    Trie A {^ i} 
  〔_,_〕 : ∀ {i τ₁ τ₂} → Trie A {i} τ₁ → Trie A {i} τ₂ →
    Trie A {^ i} (τ₁ + τ₂)
  ↑_    : ∀ {i τ₁ τ₂} → Trie (Trie A {i} τ₂) {i} τ₁ →
    Trie A {^ i} (τ₁ ⨰ τ₂)
  roll  : ∀ {i τ} → Trie A {i} (const (μ τ) * τ) →
    Trie A {^ i} (μ τ)

infixr 5 Trie
syntax Trie A τ = τ ▷ A

fmap : ∀ {i } {A B : Set } {τ} → (A → B) → Trie A {i} τ → Trie B {i} τ
fmap f (〈〉 x) = 〈〉 (f x)
fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕
fmap f (↑ σ) = ↑ fmap (fmap f) σ
fmap f (roll σ) = roll (fmap f σ)

Problem

Original source

Related problems

• Termination of structural induction