Is there a reason why embed and project have a Base constraint?
Right now, embed and project look like this:
interface (Functor f, Base t f) => Corecursive (f : Type -> Type) (t : Type) where
embed : (Base t f) => f t -> t
interface (Functor f, Base t f) => Recursive (f : Type -> Type) (t : Type) where
project : (Base t f) => t -> f t
I was surprised they didn't look like this:
interface (Functor f, Base t f) => Corecursive (f : Type -> Type) (t : Type) where
embed : f t -> t
interface (Functor f, Base t f) => Recursive (f : Type -> Type) (t : Type) where
project : t -> f t
Is there a reason for the extra constraint on embed and project?
Also, something else I just noticed: the Base constraint can be removed in some of the functions in Data.Functor.Foldable because Base is implied by Recursive and Corecursive.
One last thing:
Currently the definition of Base looks like this:
interface Base t (f : Type -> Type) where
type : Type
functor : Type -> Type
However, it seems like it could be simplified to just this:
interface Base t (f : Type -> Type) where
Since Base is just used to tie together t and f, I don't think the type and functor methods are needed.
Is there a reason why
embedandprojecthave aBaseconstraint?Right now,
embedandprojectlook like this:I was surprised they didn't look like this:
Is there a reason for the extra constraint on
embedandproject?Also, something else I just noticed: the
Baseconstraint can be removed in some of the functions inData.Functor.FoldablebecauseBaseis implied byRecursiveandCorecursive.One last thing:
Currently the definition of
Baselooks like this:However, it seems like it could be simplified to just this:
Since
Baseis just used to tie togethertandf, I don't think thetypeandfunctormethods are needed.