lude

commit ee026033bc4bcc8e78989a739eeffa085c8369db
parent 83c4f6a837370e1cf1f737d3cc6d07e082401a83
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed,  9 Sep 2026 17:16:53 -0700

Algebra.Category: add Monad

Diffstat:
M
src/Lude/Algebra/Category/Bifunctor.hs
 | 
3
+++
M
src/Lude/Algebra/Category/Core.hs
 | 
13
++++++++++---
A
src/Lude/Algebra/Category/Monad.hs
 | 
50
++++++++++++++++++++++++++++++++++++++++++++++++++

3 files changed, 63 insertions(+), 3 deletions(-)
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -13,6 +13,9 @@ module Lude.Algebra.Category.Bifunctor (
 import Lude.Algebra.Category.Core
 import Lude.Haskell
 
+-- TODO: Read Conor McBride's paper on bifunctors and decide what abstractions
+-- are worth providing here.
+
 --------------------------------------------------------------------------------
 
 -- NOTE: We ought not need to assume that BidomR p and Bicod p are categorical,
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 
--- TODO: Consider what to re-export from Lude.Haskell.Category.
 module Lude.Algebra.Category.Core (
     Cat,
     DefaultCat,
@@ -16,6 +15,8 @@ module Lude.Algebra.Category.Core (
     FunctorialOn,
     Endofunctorial,
     EndofunctorialOn,
+    CatOfEndo,
+    ObjArg,
     preservesObj,
     --
     NT (..),
@@ -112,14 +113,20 @@ type FunctorialOn :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constraint
 class (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f | f -> p q
 instance (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f
 
-type Endofunctorial :: forall {i}. (i -> i) -> Constraint
+type Endofunctorial :: forall {i}. Endo i -> Constraint
 class (Functorial f, Dom f ~ Cod f) => Endofunctorial f
 instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f
 
-type EndofunctorialOn :: forall {i}. Cat i -> (i -> i) -> Constraint
+type EndofunctorialOn :: forall {i}. Cat i -> Endo i -> Constraint
 class (FunctorialOn p p f) => EndofunctorialOn p f | f -> p
 instance (FunctorialOn p p f) => EndofunctorialOn p f
 
+type CatOfEndo :: forall {i}. Endo i -> Cat i
+type CatOfEndo f = Dom f
+
+type ObjArg :: forall {i} {j}. (i -> j) -> Predicate i
+type ObjArg f = Obj (Dom f)
+
 preservesObj :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (f :: i -> j) -> (FunctorialOn p q f) => forall (a :: i) -> Obj p a :- Obj q (f a)
 preservesObj _ _ = preservesObj_
 
diff --git a/src/Lude/Algebra/Category/Monad.hs b/src/Lude/Algebra/Category/Monad.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Algebra.Category.Monad (
+    Monadic (..),
+    MonadicOn,
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Haskell
+
+-- TODO: Make applicative/monoidal functors a superclass.
+
+-- TODO: Comonads
+
+--------------------------------------------------------------------------------
+
+-- infixl 1 >>=, >>
+
+--------------------------------------------------------------------------------
+
+type Monadic :: forall {i}. Endo i -> Constraint
+class (Endofunctorial f) => Monadic (f :: Endo i) where
+    {-# MINIMAL pure, (join | bind) #-}
+
+    -- NOTE: We unwrap the natural transformations so we don't have to use
+    -- nominal Identity and Compose types.
+
+    pure :: forall (a :: i). (ObjArg f a) => CatOfEndo f a (f a)
+
+    join :: forall (a :: i). (ObjArg f a) => CatOfEndo f (f (f a)) (f a)
+    join = bind identity \\ f `preservesObj` a
+
+    bind :: forall (a :: i) (b :: i). (ObjArg f b) => CatOfEndo f a (f b) -> CatOfEndo f (f a) (f b)
+    bind f = join . map f
+
+type MonadicOn :: forall {i}. Cat i -> Endo i -> Constraint
+class (Monadic f, CatOfEndo f ~ p) => MonadicOn p f
+instance (Monadic f, CatOfEndo f ~ p) => MonadicOn p f
+
+--------------------------------------------------------------------------------
+-- Haskell
+
+-- TODO: Generalize to internal hom
+instance Monadic ((->) r) where
+    pure x = \_ -> x
+    join mm = \c -> mm c c
+    bind k m = \c -> k (m c) c
+
+-- (>>=) :: forall f a b. (MonadicOn Function f) => f a -> (a -> f b) -> f b
+-- (>>=) = ()