CODEWITHSUNDEEP
idrisrecursion-schemes
nnnmmm
nnnmmm

Reputation: 8754

How do I write a CV-Coalgebra in Idris2?

In Haskell, I can write

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

but Idris doesn't seem to allow such fix-point types with data. They do work with record, i.e. I can write

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

but there I can't have more than one variant if I understand right. Is there a solution?

Upvotes: 1

Views: 58

Answers (1)

nnnmmm
nnnmmm

Reputation: 8754

Got it – I missed the general form of defining data types:

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)

Upvotes: 2

Related Questions