问题描述
在 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)
但是如果我理解正确的话,我不能有多个变体。有解决办法吗?
解决方法
明白了——我错过了定义数据类型的一般形式:
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)