Agda中使用map递归时如何通过终止检查？

你定义的Foo是嵌套递归类型，构造器Bar接收的是List Foo而非直接的Foo类型值。Agda默认终止检查器不会穿透map这类高阶函数跟踪参数的结构递减关系，无法判定map process x中传入process的参数是外层Bar x的严格子结构，因此抛出终止检查失败错误。

方案1：终止注解（改动最小） #

如果你确认函数逻辑确实是按结构递减递归，直接在process前加{-# TERMINATING #-}注解，告知Agda跳过该函数的终止检查即可，代码改动只有一行：

open import Data.List using (List; map)

data Foo : Set where
  Bar : List Foo → Foo

data Foo2 : Set where
  Bar2 : List Foo2 → Foo2

{-# TERMINATING #-}
process : Foo → Foo2
process (Bar x) = Bar2 (map process x)

这个方案代码改动最少，适合快速验证、个人项目场景。

方案2：大小类型（不跳过检查，更严谨） #

如果需要保留Agda的终止校验、避免标注TERMINATING带来的潜在风险，可以启用大小类型扩展，让Agda自动识别嵌套结构的递减性，仅需少量修改：

-- 顶部启用大小类型扩展
{-# OPTIONS --sized-types #-}
open import Data.List using (List; map)
open import Size using (Size; ↑_)

-- 给Foo加大小索引
data Foo : Size → Set where
  Bar : {i : Size} → List (Foo i) → Foo (↑ i)

data Foo2 : Set where
  Bar2 : List Foo2 → Foo2

-- 给process加大小参数，核心逻辑完全不需要改
process : {i : Size} → Foo i → Foo2
process (Bar x) = Bar2 (map process x)

这种写法下Agda可以通过大小索引自动证明递归参数严格递减，完全合规通过终止检查，适合需要高可靠性的正式代码场景。

内容的提问来源于stack exchange，提问作者Camelid