# Categorical programming in OCaml

I wonder what is the state of “categorical programming” in the OCaml-verse.

Vague question probably, but that’s why I ask it here.
Let me precise what I mean by that :

• Functors : is there any standard-ish libraries expressing functors in the categorical sense. be it restricted from OCam to OCaml, “the category of ocaml types and functions” (as in the haskell typeclass Functor the functors from Hask to Hask), or, better, between categories in general

• Fold technology : is there any standard-ish libraries dealing with different kinds of fixed points encoded as syntax (a la `newtype Fix f = Fix (f (Fix f))` in haskell), as an explicit church / least fixed point, greatest fixed points and accompanying fold/unfold/refold

• Higher order fold technologies à la Sheard. (and of course one could add adjunctions, lan, ran, profunctors etc…)

What’s the state of this line of expression, and what would be missing to push it ?

What do you call a refold ?

`refold` is defined in Haskell as

``````refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b
refold f g = go where go a = f (fmap go (g a))
``````

If you introduce the initial algebra with the iso `f (Fix f) -> Fix f`, the least and the greatest fixed points (whose universal properties are categorically described as being a "limit " of the forgetful functor from algebras to their codomains + the dual )

``````newtype Fix f = Fix {unFix :: f (Fix f)} deriving (Generic)
newtype Mu f = Mu {unMu :: forall b. (f b -> b) -> b} -- least
data Nu f = forall a. Nu (a -> f a) a -- greatest
``````

This is akin to a function

``````nuToMu :: Functor f => Nu f -> Mu f
``````

and it allows to translate between the various representations like

``````foldFix :: Functor s => Fix s -> Mu s
foldFix x f = Mu (refold f unFix x)
``````
``````decodeNu :: Functor f => Nu f -> Fix f
decodeNu (Nu next seed) = refold Fix next seed
``````

and of course there are many variants, where `f` is not just a `Functor` in haskell terminology, that is, categorically, an endofunctor from `Hask` to `Hask`. (But Haskell does not allow to express those kinds of construct in their full generality. It can’t encode as a type, say, the category of categories, as far as I know)

Notably, this can happen with second order functors where the fix operator has kind ( (* → * ) → (* → *) ) → * → * and Tim Sheard’s paper already mentioned make great use of it

1 Like