如何在Lean4中定义free monads和cofree comonads？

Question

在 Haskell 中，我们可以这样定义这两个：

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 declaredLean 4
inductive Cofree (f : Type → Type) (α : Type) where
  | cofree : α → f (Cofree f α) → Cofree f α

是否有类似于 Agda 的 TERMINATING pragma 的东西？或者这个错误与其他问题有关？

Answer 1

可在终止语言中表达的自由单子的一个变体如下。 操作单子或自由单子：

inductive Free (f : Type → Type) (α : Type) where
  | pure : α → Free f α
  | free : ∀ x, f x -> (x -> Free f α) → Free f α

使用相同技巧的免费 comonad 变体：

inductive Cofree (f : Type → Type) (α : Type) where
  | cofree : ∀ x, α → f x -> (x -> Cofree f α) → Cofree f α

---

原始定义的问题在于，其格式良好要求

f

是满足“严格正性”条件（甚至无法在类型系统中表达）的函子（比任何

Type -> Type

更具限制性） .

如果允许，您可以使用类型函数

Free

实例化

f a = a -> a

，以便

Free f empty

与以下非法类型同构（在Haskell中）：

data Bad where
  Bad :: (Bad -> Bad) -> Bad

这很糟糕，因为它包含无类型的 lambda 演算。它可以对非终止术语进行编码，例如

(\x. x x) (\x. x x)

:

selfapply :: Bad -> Bad
selfapply (Bad x) = x (Bad x)

omega :: Bad
omega = selfapply (Bad selfapply)

上面的合法变体不要求

f

是函子。它用自由函子（在 Haskell 中也称为

Coyoneda

）组成自由单子构造，满足归纳类型所需的严格正性条件。

data FreeFunctor (f :: Type -> Type) (a :: Type) where
  Free :: f x -> (x -> a) -> FreeFunctor f a