如何在Idris2中编写CV-余代数？

Question

在Haskell中，我可以写

data CoAttr f a
  = Automatic a
  | Manual (f (CoAttr f a))

但是Idris似乎不允许在data中使用这种定点类型。它们可以使用record，也就是说，我可以写

record CoAttrWithoutAutomatic (f : Type -> Type) where
    constructor Manual
    out : f (CoAttrWithoutAutomatic f)

但是如果我理解正确的话，我不能有超过一个的变种。有解决方案吗？

Answer 1

明白了--我错过了定义数据类型的一般形式：

data CoAttr : (f : Type -> Type) -> (a : Type) -> Type where
  Automatic : a -> CoAttr f a
  Manual : (f (CoAttr f a)) -> CoAttr f a

CVCoalgebra : (f: Type -> Type) -> (a: Type) -> Type
CVCoalgebra f a = a -> f (CoAttr f a)