Categorical programming in OCaml

Learning
,
1

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 ?

2

What do you call a refold ?

3

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