Data.Functor.Foldable.Instances

unfix : Fix f -> f (Fix f)

Unfix a 'Fix f'

lambek : Recursive f t => Corecursive f t => t -> f t

Lambek's lemma assures us this function always exists.

fix : f (Fix f) -> Fix f

Create a fix-point with a functor

colambek : Recursive f t => Corecursive f t => f t -> t

The dual of Lambek's lemma.

data StreamF : Type -> Type -> Type

Pipe : a -> b -> StreamF a b

data Nu : (f : Type -> Type) -> Type -> Type

Nu fix-point functor for coinduction

NuF : ((a -> f a) -> a) -> b -> Nu f b

data Mu : (Type -> Type) -> Type

Mu fix-point functor for induction

MuF : ((a -> f a) -> a) -> Mu f

data ListF : Type -> Type -> Type

NilF : ListF _ _

Cons : a -> b -> ListF a b

data Fix : (Type -> Type) -> Type

Fix-point data type for exotic recursion schemes of various kinds

Fx : f (Fix f) -> Fix f