As far as I understand, recursive data types from Haskell correspond to initial algebras of endofunctors from the Hask
category [1, 2]. For example:
- Natural numbers,
data Nat = Zero | Succ Nat
, correspond to the initial algebra of the endofunctorF(-) = 1 + (-)
. - Lists,
data List a = Nil | Cons a (List a)
, correspond to the initial algebra of the endofunctorF(A, -) = 1 + A × (-)
.
However, it's not clear to me what the endofunctor corresponding to the rose trees should be:
data Rose a = Node a (List (Rose a))
What confuses me is that there are two recursions: one for the rose tree and the other for the list. According to my calculations, I would get the following functor, but it doesn't seem right:
F(A, •, -) = A × (1 + (-) × (•))
Alternatively, rose trees can be defined as mutually recursive data types:
data Rose a = Node a (Forest a)
type Forest a = List (Rose a)
Do mutually recursive data types have an interpretation in category theory?
I would discourage talk of "the Hask Category" because it subconsciously conditions you against looking for other categorical structure in Haskell programming.
Indeed, rose trees can be seen as the fixpoint of an endofunctor on types-and-functions, a category which we might be better to call
Type
, now thatType
is the type of types. If we give ourselves some of the usual functor kit......and fixpoints...
...then we may take
The fact that
[]
is itself recursive does not prevent its use in the formation of recursive datatypes viaFix
. To spell out the recursion explicitly, we have nested fixpoints, here with bound variable names chosen suggestively:Now, by the time we've arrived in the second fixpoint, we have a type formula
which is functorial (indeed, strictly positive) in both
rose
andlist
. One might say it is aBifunctor
, but that's unnecessary terminology: it's a functor from(Type, Type)
toType
. You can make aType -> Type
functor by taking a fixpoint in the second component of the pair, and that's just what happened above.The above definition of
Rose
loses an important property. It is not true thatmerely that
Rose x :: Type
ifx :: Type
. In particular,is not a well typed constraint, which is a pity, as intuitively, rose trees ought to be functorial in the elements they store.
You can fix this by building
Rose
as itself being the fixpoint of aBifunctor
. So, in effect, by the time we get to lists, we have three type variables in scope,a
,rose
andlist
, and we have functoriality in all of them. You need a different fixpoint type constructor, and a different kit for buildingBifunctor
instances: forRose
, life gets easier because thea
parameter is not used in the inner fixpoint, but in general, to define bifunctors as fixpoints requires trifunctors, and off we go!This answer of mine shows how to fight the proliferation by showing how indexed types are closed under a fixpoint-of-functor construction. That's to say, work not in
Type
but ini -> Type
(for the full variety of index typesi
) and you're ready for mutual recursion, GADTs, and so on.So, zooming out, rose trees are given by mutual fixpoints, which have a perfectly sensible categorical account, provided you see which categories are actually at work.