Завершение проверки функции по дереву

Уловку inline / fuse можно применить (возможно) неожиданным образом. Этот трюк подходит для задач такого рода:

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)

Эта функция является структурно рекурсивной, но скрытым образом. map просто применяет map-trie f к элементам xs, поэтому map-trie применяется к меньшим (под-) попыткам. Но Agda не просматривает определение map, чтобы убедиться, что он не делает ничего необычного. Поэтому мы должны применить трюк с встроенным / предохранителем, чтобы пройти проверку завершения:

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

Ваша fmap функция имеет ту же структуру, вы сопоставляете какую-то приподнятую функцию. Но что встроить? Если мы последуем примеру выше, мы должны встроить сам fmap. Это выглядит и кажется немного странным, но действительно работает:

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

Вы можете применить еще один прием: он называется типами размера. Вместо того, чтобы полагаться на компилятор, чтобы выяснить, когда что-то является или не является структурно рекурсивным, вы вместо этого указываете это напрямую. Однако вы должны индексировать свои типы данных по типу Size, поэтому этот подход довольно навязчив и не может быть применен к уже существующим типам, но я думаю, что о нем стоит упомянуть.

В простейшей форме размерный тип ведет себя как тип, индексированный натуральным числом. Этот индекс определяет верхнюю границу структурных размеров. Вы можете думать об этом как о верхней границе высоты дерева (учитывая, что тип данных является F-ветвлением для некоторого функтора F). Увеличенная версия List выглядит почти как Vec, например:

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

Но типоразмеры добавляют несколько функций, которые упрощают их использование. У вас есть константа ∞ на тот случай, если вам не важен размер. suc называется ↑, и Agda реализует несколько правил, например ↑ ∞ = ∞.

Давайте перепишем пример Trie, чтобы использовать размерные типы. Нам понадобится прагма вверху файла и один импорт:

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

А вот и измененный тип данных:

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

Если вы оставите функцию map-trie как есть, средство проверки завершения все равно будет жаловаться. Это потому, что, когда вы не укажете какой-либо размер, Agda заполнит бесконечность (то есть значение безразличия), и мы вернемся к началу.

Однако мы можем отметить map-trie как сохраняющий размер:

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)

Итак, если вы дадите ему Trie, ограниченный i, он также даст вам другой Trie, ограниченный i. Таким образом, map-trie никогда не сможет сделать Trie больше, только одинаково большим или меньшим. Этого достаточно для проверки завершения, чтобы выяснить, что map (map-trie f) xs в порядке.

Этот метод также можно применить к вашему 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 σ)