如何在Coq中形式化Haskell的Term类型？递归方案实现问询

嘿，你遇到的这个严格正性错误是Coq归纳类型系统的典型限制，我来一步步帮你拆解问题：

一、怎么在Coq里形式化Haskell的Term f类型？ #

Coq的归纳类型要求严格正性——简单说，递归类型的出现不能在箭头的左侧（或者说函子的逆变参数位置），而Haskell的Term f = In { out :: f (Term f) }是函子的固定点，直接写会触发错误，因为Coq没法默认验证f是协变的。这里有几种可行的办法：

1. 先定义协变函子接口，再基于它定义固定点 #

先给Functor做一个类型类约束，明确f是协变的，这样Coq能放心接受递归出现：

Class Functor (F : Type -> Type) := {
  fmap : forall {A B}, (A -> B) -> F A -> F B;
  fmap_id : forall {A}, fmap (@id A) = id;
  fmap_comp : forall {A B C} (g : B -> C) (h : A -> B), fmap (g ∘ h) = fmap g ∘ fmap h
}.

Inductive Term (F : Type -> Type) `{Functor F} : Type :=
| In : F (Term F) -> Term F.

不过要注意，这个定义还是需要F的参数是正位置的——如果F是逆变函子（比如F X := X -> bool），还是会报错，所以本质上还是要保证F是严格正的函子。

2. 针对具体的正函子定义固定点 #

如果不需要泛化到所有函子，而是针对具体的归纳函子（比如列表、二叉树对应的函子），可以直接为每个函子写对应的固定点：

-- 列表函子：ListF a b 表示“还差一个b就能拼成完整列表”
Inductive ListF (a : Type) (b : Type) : Type :=
| NilF : ListF a b
| ConsF : a -> b -> ListF a b.

-- 列表就是ListF的固定点
Inductive List (a : Type) : Type :=
| InList : ListF a (List a) -> List a.

这个是完全合法的，因为ListF的第二个参数是正出现的，Coq能识别到递归的结构递减。

3. 使用Coq的递归类型扩展 #

Coq有一个RecursiveTypes库，支持直接定义最小固定点类型，完美对应Haskell的Term f：

Require Import RecursiveTypes.

-- mu X. F X 就是F的最小固定点
Definition Term (F : Type -> Type) := mu (fun X => F X).

-- 对应Haskell的In和out
Definition In {F} : F (Term F) -> Term F := roll.
Definition out {F} : Term F -> F (Term F) := unroll.

这个方式最贴近Haskell的写法，而且只要F是严格正的函子，就能正常使用。

二、限制f为归纳类型能保证递减吗？ #

其实核心不是f是不是归纳类型，而是f作为Type -> Type的函子是否是严格正的。严格正函子指的是，递归类型的出现只会在“正向”位置——比如多项式函子（由和、乘积、恒等函子组合而成的函子，比如F X := unit + nat * X）都是严格正的。

如果把f限制为严格正的归纳函子，那么f (Term f)里的Term f就是正出现的，Coq就能验证递归结构是递减的，从而接受这个归纳定义。单纯的归纳类型如果是逆变的（比如F X := X -> unit），还是会触发正性错误。

三、Coq里已经有Bananas、Lenses等递归方案的实现吗？ #

当然有！社区里早就有成熟的实现了：

• Coq Equations库：这个库是定义复杂递归的神器，支持直接定义paramorphisms、histomorphisms、catamorphisms等各种递归方案，而且能和函子固定点无缝结合。
• Mathematical Components库：里面有高度抽象的函子、固定点和递归方案定义，适合做形式化数学的场景。
• 社区自定义实现：很多GitHub项目里都有针对多项式函子的递归方案，比如catamorphism的通用定义大概是这样的：

  Definition cata {F} `{Functor F} {A} (alg : F A -> A) : Term F -> A :=
    fix go (t : Term F) := alg (fmap go (out t)).
  

  这个就是经典的香蕉组合子——用代数alg把固定点折叠成目标类型A。

另外，Coq标准库里的基础函数其实就是递归方案的实例：比如列表的fold_right就是列表函子的catamorphism，二叉树的折叠也是同理。

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