commit 954e96fedbba63e0f3563fe72ceb1172c465b5c1
parent 459ae6ab64ab937751af969f91b9c03b09b1d4ce
Author: Robert Russell <robert@rr3.xyz>
Date: Sat, 12 Sep 2026 10:29:10 -0700
Algebra.Category.Algebra: refactor
Diffstat:
2 files changed, 97 insertions(+), 55 deletions(-)
diff --git a/src/Lude/Algebra/Category/Algebra.hs b/src/Lude/Algebra/Category/Algebra.hs
@@ -1,82 +1,124 @@
module Lude.Algebra.Category.Algebra (
Algebra,
- Algebraic,
+ Algebraic (..),
+ AlgebraicOn,
+ wrap_default,
--
- DefaultRecursive (..),
Recursive (..),
+ cata_defaultFunction,
+ cata_defaultNT,
--
Coalgebra,
- Coalgebraic,
+ Coalgebraic (..),
+ CoalgebraicOn,
+ peel_default,
--
- DefaultCorecursive (..),
Corecursive (..),
+ ana_defaultFunction,
+ ana_defaultNT,
) where
import Lude.Algebra.Category.Core
import Lude.Haskell
--- TODO: Check whether we really need a separate default instance for Nt.
+-- 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.
--- TODO: Add Coalgebraic (Algebraic) as a super class of Recursive (Corecursive).
-
-- TODO: Eilenberg-Moore (co)algebras?
--------------------------------------------------------------------------------
--- | An algebra for an endofunctor.
-type Algebra :: forall {k}. Cat k -> Endo k -> k -> Type
-type Algebra p f a = f a `p` a
+-- | An algebra for an endofunctor
+type Algebra :: forall {i}. Endo i -> i -> Type
+type Algebra f a = Dom f (f a) 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
+-- | A type equipped with a canonical algebra for an endofunctor
+type Algebraic :: forall {i}. Endo i -> i -> Constraint
+class (Endofunctorial f) => Algebraic (f :: Endo i) (a :: i) | a -> f where
+ wrap :: Algebra f a
---------------------------------------------------------------------------------
+type AlgebraicOn :: forall {i}. Cat i -> Endo i -> i -> Constraint
+class (Algebraic f a, Dom f ~ p) => AlgebraicOn p f a
+instance (Algebraic f a, Dom f ~ p) => AlgebraicOn 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
+-- | Default: @wrap = ana (map peel)@
+wrap_default :: forall {i} (f :: Endo i) (a :: i). (Corecursive f a) => Algebra f a
+wrap_default = ana (map peel)
-instance (Coalgebraic Function f r) => DefaultRecursive Function f r where
- defaultCata f = h where h = f . map h . peel
-instance (Categorical p, Categorical q, Coalgebraic (p ==> q) f r) => DefaultRecursive (NT p q) f r where
- defaultCata f@(Naturally _) = h where h = Naturally (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(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 type @r@ equipped with an initial algebra @wrap@ for an endofunctor @f@
+--
+-- Laws:
+-- - __@r@ is an initial @f@-algebra:__ for all @f@-algebras @a@,
+-- @cata a@ is an @f@-algebra homomorphism from @r@ to @a@
+-- (i.e., @cata a . wrap = a . map (cata a)@) and unique with this property
+-- - __@peel@ is the inverse of @wrap@:__ @peel . wrap = identity@ (at @f r@)
+-- and @wrap . peel = identity@ (at @r@) (cf., Lambek's theorem)
+type Recursive :: forall {i}. Endo i -> i -> Constraint
+class (Algebraic f r, Coalgebraic f r) => Recursive (f :: Endo i) (r :: i) where
+ cata :: forall (a :: i). Algebra f a -> Dom f r a
+
+type DefaultCata :: forall {i}. Endo i -> i -> Type
+type DefaultCata f r = (Algebraic f r, Coalgebraic f r) => forall a. Algebra f a -> Dom f r a
+
+-- | Default: @cata f = f . map (cata f) . peel@
+cata_defaultFunction
+ :: forall (f :: Endo Type) r
+ . (Dom f ~ Function) => DefaultCata f r
+cata_defaultFunction a = h where h = a . map h . peel
+
+-- | Default: @cata f = f . map (cata f) . peel@ (modulo laziness)
+cata_defaultNT
+ :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: Endo (i -> j)) r
+ . (Categorical p, Categorical q, Dom f ~ NT p q) => DefaultCata f r
+cata_defaultNT a@(Naturally _) = h where h = Naturally (comp a . comp (map h) . comp peel) \\ witnessMor (wrap @f @r)
--------------------------------------------------------------------------------
--- | 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 coalgebra for an endofunctor
+type Coalgebra :: forall {i}. Endo i -> i -> Type
+type Coalgebra g b = Dom g b (g b)
+
+-- | A type equipped with a canonical coalgebra for an endofunctor
+type Coalgebraic :: forall {i}. Endo i -> i -> Constraint
+class (Endofunctorial g) => Coalgebraic (g :: Endo i) (b :: i) | b -> g where
+ peel :: Coalgebra g b
+
+type CoalgebraicOn :: forall {i}. Cat i -> Endo i -> i -> Constraint
+class (Coalgebraic g b, Dom g ~ p) => CoalgebraicOn p g b
+instance (Coalgebraic g b, Dom g ~ p) => CoalgebraicOn 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
+-- | Default: @peel = cata (map wrap)@
+peel_default :: forall {i} (g :: Endo i) (b :: i). (Recursive g b) => Coalgebra g b
+peel_default = cata (map wrap)
--------------------------------------------------------------------------------
-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 Function g s) => DefaultCorecursive Function g s where
- defaultAna g = h where h = wrap . map h . g
-instance (Categorical p, Categorical q, Algebraic (p ==> q) g s) => DefaultCorecursive (p ==> q) g s where
- defaultAna g@(Naturally _) = h where h = Naturally (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(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
+-- | A type @s@ equipped with a terminal coalgebra @peel@ for an endofunctor @g@
+--
+-- Laws:
+-- - __@s@ is a terminal @g@-coalgebra:__ for all @g@-coalgebras @b@,
+-- @ana b@ is a @g@-coalgebra homomorphism from @b@ to @s@
+-- (i.e., @map (ana b) . b = peel . ana b@) and unique with this property
+-- - __@wrap@ is the inverse of @peel@:__ @peel . wrap = identity@ (at @g s@)
+-- and @wrap . peel = identity@ (at @s@) (cf., Lambek's theorem)
+type Corecursive :: forall {i}. Endo i -> i -> Constraint
+class (Algebraic g s, Coalgebraic g s) => Corecursive (g :: Endo i) (s :: i) where
+ ana :: forall (b :: i). Coalgebra g b -> Dom g b s
+
+type DefaultAna :: forall {i}. Endo i -> i -> Type
+type DefaultAna g s = (Coalgebraic g s, Algebraic g s) => forall b. Coalgebra g b -> Dom g b s
+
+-- | Default: @ana g = wrap . map (ana g) . g@
+ana_defaultFunction
+ :: forall (g :: Endo Type) s
+ . (Dom g ~ Function) => DefaultAna g s
+ana_defaultFunction b = h where h = wrap . map h . b
+
+-- | Default: @ana g = wrap . map (ana g) . g@ (modulo laziness)
+ana_defaultNT
+ :: forall {i} {j} (p :: Cat i) (q :: Cat j) (g :: Endo (i -> j)) s
+ . (Categorical p, Categorical q, Dom g ~ NT p q) => DefaultAna g s
+ana_defaultNT b@(Naturally _) = h where h = Naturally (comp wrap . comp (map h) . comp b) \\ witnessMor (peel @g @s)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -49,11 +49,11 @@ class Categorical (p :: Cat i) where
type Obj p :: Predicate i
type Obj p = Always
- identity :: forall a. (Obj p a) => a `p` a
- compose :: forall a b c. b `p` c -> a `p` b -> a `p` c
+ identity :: forall (a :: i). (Obj p a) => a `p` a
+ compose :: forall (a :: i) (b :: i) (c :: i). b `p` c -> a `p` b -> a `p` c
- witnessMor :: forall a b. Witness (a `p` b) (Mor p a b)
- default witnessMor :: forall a b. (Mor p a b) => Witness (a `p` b) (Mor p a b)
+ witnessMor :: forall (a :: i) (b :: i). Witness (a `p` b) (Mor p a b)
+ default witnessMor :: forall (a :: i) (b :: i). (Mor p a b) => Witness (a `p` b) (Mor p a b)
witnessMor = witnessOf tautology
type Mor = Obj2
@@ -65,7 +65,7 @@ type Obj3 :: forall {i}. Cat i -> i -> i -> i -> Constraint
class (Obj p a, Obj p b, Obj p c) => Obj3 p a b c
instance (Obj p a, Obj p b, Obj p c) => Obj3 p a b c
-(.) :: forall {i} (p :: Cat i) a b c. (Categorical p) => b `p` c -> a `p` b -> a `p` c
+(.) :: forall {i} (p :: Cat i) (a :: i) (b :: i) (c :: i). (Categorical p) => b `p` c -> a `p` b -> a `p` c
(.) = compose
-- TODO: Flipped composition operator? More composition operators for CCCs?
