I wonder what is the state of “categorical programming” in the OCamlverse.
Vague question probably, but that’s why I ask it here.
Let me precise what I mean by that :

Functors : is there any standardish 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 standardish 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