lude

commit ded67be251b3a619bf3ceddb15251389842b24c2
parent 0571baab02bb4549c48e76409850ec6cd6ec0bcc
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri,  4 Sep 2026 12:19:58 -0700

Add (co)algebras for endofunctors

Diffstat:
A
src/Lude/Algebra/Algebra.hs
 | 
79
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1 file changed, 79 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra/Algebra.hs b/src/Lude/Algebra/Algebra.hs
@@ -0,0 +1,79 @@
+module Algebra.Algebra (
+    Algebra,
+    Algebraic,
+    --
+    DefaultRecursive (..),
+    Recursive (..),
+    --
+    Coalgebra,
+    Coalgebraic,
+    --
+    DefaultCorecursive (..),
+    Corecursive (..),
+) where
+
+import Lude.Algebra.Category
+import Lude.Constraint
+import Lude.Kind
+
+-- TODO: Check whether we really need a separate default instance for Nt.
+-- I think it's necessary, because composition with `map h` forces eager
+-- evaluation of h.
+
+--------------------------------------------------------------------------------
+
+-- | An algebra for an endofunctor.
+type Algebra :: forall {k}. Cat k -> Endo k -> k -> Type
+type Algebra p f a = f a `p` a
+
+-- | A type equipped with an algebra for an endofunctor.
+type Algebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (EndofunctorialOn p f) => Algebraic p f a | a -> f where
+    wrap :: Algebra p f a
+
+--------------------------------------------------------------------------------
+
+type DefaultRecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class DefaultRecursive p f r where
+    defaultCata :: (Algebraic p f r) => forall a. Algebra p f a -> r `p` a
+
+instance (Coalgebraic Hask f r) => DefaultRecursive Hask f r where
+    defaultCata f = h where h = f . map h . peel
+instance (Categorical p, Categorical q, Coalgebraic (Nt p q) f r) => DefaultRecursive (Nt p q) f r where
+    defaultCata f@(Nt _) = h where h = Nt (comp f . comp (map h) . comp peel) \\ witnessObj (wrap @(Nt p q) @f @r)
+
+-- | A type equipped with an initial algebra for an endofunctor.
+type Recursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (Algebraic p f r) => Recursive p f r where
+    cata :: forall a. Algebra p f a -> r `p` a
+    default cata :: (DefaultRecursive p f r) => forall a. Algebra p f a -> r `p` a
+    cata = defaultCata
+
+--------------------------------------------------------------------------------
+
+-- | A coalgebra for an endofunctor.
+type Coalgebra :: forall {k}. Cat k -> Endo k -> k -> Type
+type Coalgebra p g b = b `p` g b
+
+-- | A type equipped with a coalgebra for an endofunctor.
+type Coalgebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (EndofunctorialOn p g) => Coalgebraic p g b | b -> g where
+    peel :: Coalgebra p g b
+
+--------------------------------------------------------------------------------
+
+type DefaultCorecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class DefaultCorecursive p g s where
+    defaultAna :: (Coalgebraic p g s) => forall b. Coalgebra p g b -> b `p` s
+
+instance (Algebraic Hask g s) => DefaultCorecursive Hask g s where
+    defaultAna g = h where h = wrap . map h . g
+instance (Categorical p, Categorical q, Algebraic (Nt p q) g s) => DefaultCorecursive (Nt p q) g s where
+    defaultAna g@(Nt _) = h where h = Nt (comp wrap . comp (map h) . comp g) \\ witnessObj (peel @(Nt p q) @g @s)
+
+-- | A type equipped with a final coalgebra for an endofunctor.
+type Corecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (Coalgebraic p g s) => Corecursive p g s where
+    ana :: forall b. Coalgebra p g b -> b `p` s
+    default ana :: (DefaultCorecursive p g s) => forall b. Coalgebra p g b -> b `p` s
+    ana = defaultAna