idris - 如何在 Idris2 中编​​写 CV-Coalgebra？

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)