Termination-checking of function over a trie

Question

I'm having difficulty convincing Agda to termination-check the function fmap below and similar functions defined recursively over the structure of a Trie. A Trie is a trie whose domain is a Type, an object-level type formed from unit, products and fixed points (I've omitted coproducts to keep the code minimal). The problem seems to relate to a type-level substitution I use in the definition of Trie. (The expression const (μₜ τ) * τ means apply the substitution const (μₜ τ) to the type τ.)

module Temp where

   open import Data.Unit
   open import Category.Functor
   open import Function
   open import Level
   open import Relation.Binary

   -- A context is just a snoc-list.
   data Cxt {} (A : Set ) : Set  where
      ε : Cxt A
      _∷ᵣ_ : Cxt A → A → Cxt A

   -- Context membership.
   data _∈_ {} {A : Set } (a : A) : Cxt A → Set  where
      here : ∀ {Δ} → a ∈ Δ ∷ᵣ a
      there : ∀ {Δ a′} → a ∈ Δ → a ∈ Δ ∷ᵣ a′
   infix 3 _∈_

   -- Well-formed types, using de Bruijn indices.
   data _⊦ (Δ : Cxt ⊤) : Set where
      nat : Δ ⊦
       : Δ ⊦
      var : _ ∈ Δ → Δ ⊦
      _+_ _⨰_ : Δ ⊦ → Δ ⊦ → Δ ⊦
      μ : Δ ∷ᵣ _ ⊦ → Δ ⊦
   infix 3 _⊦

   -- A closed type.
   Type : Set
   Type = ε ⊦

   -- Type-level substitutions and renamings.
   Sub Ren : Rel (Cxt ⊤) zero
   Sub Δ Δ′ = _ ∈ Δ → Δ′ ⊦
   Ren Δ Δ′ = ∀ {x} → x ∈ Δ → x ∈ Δ′

   -- Renaming extension.
   extendᵣ : ∀ {Δ Δ′} → Ren Δ Δ′ → Ren (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
   extendᵣ ρ here = here
   extendᵣ ρ (there x) = there (ρ x)

   -- Lift a type renaming to a type.
   _*ᵣ_ : ∀ {Δ Δ′} → Ren Δ Δ′ → Δ ⊦ → Δ′ ⊦
   _ *ᵣ nat = nat
   _ *ᵣ  = 
   ρ *ᵣ (var x) = var (ρ x)
   ρ *ᵣ (τ₁ + τ₂) = (ρ *ᵣ τ₁) + (ρ *ᵣ τ₂)
   ρ *ᵣ (τ₁ ⨰ τ₂) = (ρ *ᵣ τ₁) ⨰ (ρ *ᵣ τ₂)
   ρ *ᵣ (μ τ) = μ (extendᵣ ρ *ᵣ τ)

   -- Substitution extension.
   extend : ∀ {Δ Δ′} → Sub Δ Δ′ → Sub (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
   extend θ here = var here
   extend θ (there x) = there *ᵣ (θ x)

   -- Lift a type substitution to a type.
   _*_ : ∀ {Δ Δ′} → Sub Δ Δ′ → Δ ⊦ → Δ′ ⊦
   θ * nat = nat
   θ *  = 
   θ * var x = θ x
   θ * (τ₁ + τ₂) = (θ * τ₁) + (θ * τ₂)
   θ * (τ₁ ⨰ τ₂) = (θ * τ₁) ⨰ (θ * τ₂)
   θ * μ τ = μ (extend θ * τ)

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

   infixr 5 Trie
   syntax Trie A τ = τ ▷ A

   {-# NO_TERMINATION_CHECK #-}
   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 σ)

It would seem that fmap recurses into a strictly smaller argument in each case; certainly the product case is fine if I remove recursive types. On the other hand, the definition handles recursive types fine if I remove products.

What's the simplest way to proceed here? The inline/fuse trick does not look particularly applicable, but maybe it is. Or should I be looking for another way to deal with the substitution in the definition of Trie?

Answer 1

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 σ)