如何在Lean4中定义Free Monad与Cofree Comonad？

问题背景 #

在Haskell中，我们可以轻松定义Free Monad和Cofree Comonad：

data Free (f :: Type -> Type) (a :: Type) = Pure a | Free (f (Free f a))
data Cofree (f :: Type -> Type) (a :: Type) = Cofree a (f (Cofree f a))

但在Lean4中尝试相同定义时，会触发内核错误：

-- error: (kernel) arg #3 of 'Free.free' contains a non valid occurrence of the datatypes being declared
inductive Free (f : Type → Type) (α : Type) where
  | pure : α → Free f α
  | free : f (Free f α) → Free f α

-- (kernel) arg #4 of 'Cofree.cofree' contains a non valid occurrence of the datatypes being declared
inductive Cofree (f : Type → Type) (α : Type) where
  | cofree : α → f (Cofree f α) → Cofree f α

疑问：Lean4是否有类似Agda的TERMINATING编译指示？或者错误由其他原因导致？

错误原因 #

这个错误与终止检查无关，根源是Lean4默认的归纳类型检查规则限制：当归纳类型出现在类型构造器（如示例中的f）的参数位置时，内核需要明确的universe层级保证类型一致性，默认会拒绝这类“嵌套递归”的定义，除非显式声明调整。

解决方法 #

1. 显式指定Universe参数 #

为类型构造器f和参数α指定相同的universe层级，让内核确认类型合法性：

universe u

-- 合法的Free Monad定义
inductive Free (f : Type u → Type u) (α : Type u) where
  | pure : α → Free f α
  | free : f (Free f α) → Free f α

-- 合法的Cofree Comonad定义
inductive Cofree (f : Type u → Type u) (α : Type u) where
  | cofree : α → f (Cofree f α) → Cofree f α

2. 直接使用标准库实现 #

Lean4标准库已内置Free Monad和Cofree Comonad的官方实现，可直接导入使用：

import Control.Monad.Free
import Control.Comonad.Cofree

-- 示例：使用标准库定义
def demoFree : Free Option Nat := Free.free (some (Free.pure 42))
def demoCofree : Cofree Option Nat := Cofree.cofree 42 (some (Cofree.cofree 24 none))

关于类似Agda的TERMINATING指示 #

Lean4中没有直接对应Agda的TERMINATING编译指示，但针对递归函数的终止性问题：

• 可使用partial关键字标记函数为部分函数，跳过终止检查（不推荐用于正式代码，会牺牲类型安全性）；
• 对于合法递归函数，可通过termination_by指定终止度量，或decreasing_by提供自定义终止性证明，帮助内核通过检查。

内容的提问来源于stack exchange，提问作者André Muricy