Agda中实现Tree结构map函数的终止检查问题如何解决？

解决方案 #

这类嵌套归纳类型的终止检查问题是Agda开发中的常见场景，以下是两种不破坏抽象封装的通用解决思路：

方案1：使用大小类型（推荐）

开启Agda的大小类型扩展后，你可以为递归类型添加大小标注，让终止检查器自动识别递归调用的结构合法性，不需要修改业务逻辑，也不需要依赖容器的内部实现：

1. 首先开启扩展并定义带大小参数的Tree类型：

{-# OPTIONS --sized-types #-}
module Tree where

open import Data.List
open import Size

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

2. 你最初写的直观版本mapTree可以直接通过终止检查：

mapTree : ∀ {A B i} → (A → B) → Tree A {i} → Tree B {i}
mapTree f (node ts) = node (map (mapTree f) ts)
mapTree f (leaf x) = leaf (f x)

这种方案适配性极强，后续如果你要把node的容器从List换成Vector、ℕ → A等其他实现，只要调整Tree定义的大小标注即可，上层的mapTree等操作代码不需要做任何修改。

方案2：封装通用折叠器

如果你不想开启实验性扩展，可以将Tree的递归逻辑一次性封装到通用折叠器中，仅需写一次互递归，后续所有操作都基于折叠器实现：

1. 首先定义通用折叠器，封装递归逻辑：

foldTree : ∀ {A B} → (A → B) → (List B → B) → Tree A → B
foldTree' : ∀ {A B} → (A → B) → (List B → B) → List (Tree A) → List B

foldTree leafF nodeF (leaf x) = leafF x
foldTree leafF nodeF (node ts) = nodeF (foldTree' leafF nodeF ts)

foldTree' leafF nodeF [] = []
foldTree' leafF nodeF (t ∷ ts) = foldTree leafF nodeF t ∷ foldTree' leafF nodeF ts

2. 后续实现mapTree等操作时完全不需要触碰递归结构：

mapTree : ∀ {A B} → (A → B) → Tree A → Tree B
mapTree f = foldTree (λ x → leaf (f x)) node

这种方案的优势是完全兼容稳定版Agda，且抽象程度高：如果后续要替换node的容器实现，仅需要修改foldTree和对应的辅助函数，所有上层基于折叠器实现的业务代码不需要做任何调整。

注意：不推荐使用{-# TERMINATING #-}标注绕过终止检查，该方式会跳过终止性校验，可能破坏类型系统的一致性。

内容的提问来源于stack exchange，提问作者Tony Beta Lambda