commit 80510bab67d9a8e0a48ecd03c88bf1917c58ad7a
parent ce628048588dd86f51337dd39b73ec99f5b9e2fe
Author: Robert Russell <robert@rr3.xyz>
Date: Tue, 10 Mar 2026 23:41:12 -0700
Ngl I'm kinda cooking
Diffstat:
1 file changed, 186 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -0,0 +1,186 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Lude.Algebra.Category (
+ Cat,
+ Category (..),
+ Functor (..),
+) where
+
+import Lude.Either
+import Lude.Kind
+import Lude.Pair
+
+-- TODO: Semicategory
+-- TODO: Allow non-BoxL morphism Repr?
+
+type Type1 i = i -> Type
+type Type2 i = i -> i -> Type
+
+type Constraint1 i = i -> Constraint
+type Constraint2 i = i -> i -> Constraint
+
+type Pair1 :: forall i j. Type1 i -> Type1 j -> Type1 (i × j)
+data Pair1 p q a where
+ Pair1 :: p a0 -> q a1 -> Pair1 p q '(a0, a1)
+
+type (×^) = Pair1
+infixl 7 ×^
+
+type Pair2 :: forall i j. Type2 i -> Type2 j -> Type2 (i × j)
+data Pair2 p q a b where
+ Pair2 :: p a0 b0 -> q a1 b1 -> Pair2 p q '(a0, a1) '(b0, b1)
+
+type (×^^) = Pair2
+infixl 7 ×^^
+
+type Either1 :: forall i j. Type1 i -> Type1 j -> Type1 (i + j)
+data Either1 p q a where
+ L1 :: p a -> Either1 p q (L a)
+ R1 :: q a -> Either1 p q (R a)
+
+type (+^) = Either1
+infixl 6 +^
+
+type Either2 :: forall i j. Type2 i -> Type2 j -> Type2 (i + j)
+data Either2 p q a b where
+ L2 :: p a b -> Either2 p q (L a) (L b)
+ R2 :: q a b -> Either2 p q (R a) (R b)
+
+type (+^^) = Either2
+infixl 6 +^^
+
+--------------------------------------------------------------------------------
+
+type Cat i = i -> i -> Type
+
+type Category :: forall i. Cat i -> Constraint
+class Category (p :: Cat i) where
+ type Ob p :: i -> Constraint
+ type Ob p = Always
+ identity :: (Ob p a) => p a a
+ compose :: p b c -> p a b -> p a c
+
+--------------------------------------------------------------------------------
+
+type Hask :: forall r. Cat (Type @r)
+type Hask @r = (->)
+
+instance Category Hask where
+ identity x = x
+ compose f g x = f (g x)
+
+--------------------------------------------------------------------------------
+
+type ProdOb :: Cat i -> Cat j -> i × j -> Constraint
+class ProdOb p q a where
+ prodOb :: PairEvidence1 (Ob p) (Ob q) a
+instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
+ prodOb = Pair1 Evidence1 Evidence1
+
+instance (Category p, Category q) => Category (p ×^^ q) where
+ type Ob (p ×^^ q) = ProdOb p q
+ identity @a = case prodOb @_ @_ @p @q @a of
+ Pair1 Evidence1 Evidence1 -> Pair2 identity identity
+ compose (Pair2 f0 f1) (Pair2 g0 g1) = Pair2 (compose f0 g0) (compose f1 g1)
+
+--------------------------------------------------------------------------------
+
+type SumOb :: Cat i -> Cat j -> i + j -> Constraint
+class SumOb p q a where
+ sumOb :: EitherEvidence1 (Ob p) (Ob q) a
+instance (Category p, Ob p a) => SumOb p q (L a) where
+ sumOb = L1 Evidence1
+instance (Category q, Ob q a) => SumOb p q (R a) where
+ sumOb = R1 Evidence1
+
+instance (Category p, Category q) => Category (p +^^ q) where
+ type Ob (p +^^ q) = SumOb p q
+ identity @a = case sumOb @_ @_ @p @q @a of
+ L1 Evidence1 -> L2 identity
+ R1 Evidence1 -> R2 identity
+ compose (L2 f) (L2 g) = L2 (compose f g)
+ compose (R2 f) (R2 g) = R2 (compose f g)
+
+--------------------------------------------------------------------------------
+
+type Always :: forall i. i -> Constraint
+class Always i
+instance Always i
+
+type Evidence :: Constraint -> Type
+data Evidence a = (a) => Evidence
+
+type Evidence1 :: forall i. Constraint1 i -> Type1 i
+data Evidence1 p a = (p a) => Evidence1
+
+type PairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i × j)
+type PairEvidence1 p q = Pair1 (Evidence1 p) (Evidence1 q)
+
+-- TODO: pattern
+
+type EitherEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i + j)
+type EitherEvidence1 p q = Either1 (Evidence1 p) (Evidence1 q)
+
+type Entailment :: Constraint -> Constraint -> Type
+newtype Entailment a b = Entailment ((a) => Evidence b)
+
+type (:-) = Entailment
+infixr 9 :-
+
+always :: a :- Always b
+always = Entailment Evidence
+
+(\\) :: (a) => ((b) => c) -> (a :- b) -> c
+c \\ Entailment Evidence = c
+
+--------------------------------------------------------------------------------
+
+type Nt :: forall i j. Cat i -> Cat j -> Cat (i -> j)
+newtype Nt p q f g = Nt (forall a. (Ob p a) => q (f a) (g a))
+
+type NtOb :: Cat i -> Cat j -> (i -> j) -> Constraint
+class (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
+instance (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
+
+instance (Category p, Category q) => Category (Nt p q) where
+ type Ob (Nt p q) = NtOb p q
+ identity @f = Nt \ @a -> identity \\ (preserveOb :: Ob p a :- Ob q (f a))
+ compose (Nt a) (Nt b) = Nt (compose a b)
+
+--------------------------------------------------------------------------------
+
+type family DefaultCat :: Cat i
+type instance DefaultCat @(Type @r) = Hask @r
+
+type Functor :: forall i j. (i -> j) -> Constraint
+class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
+ type Dom f :: Cat i
+ type Dom f = DefaultCat
+
+ type Cod f :: Cat j
+ type Cod f = DefaultCat
+
+ preserveOb :: Ob (Dom f) a :- Ob (Cod f) (f a)
+ default preserveOb :: (Ob (Cod f) ~ Always) => Ob (Dom f) a :- Ob (Cod f) (f a)
+ preserveOb = always
+
+ map :: Dom f a b -> Cod f (f a) (f b)
+
+instance Functor (Either b) where
+ map _ (L b) = L b
+ map f (R a) = R (f a)
+
+-- type Endofunctor :: forall k. (k -> k) -> Constraint
+-- type Endofunctor f = (Functor f, Dom f ~ Cod f)
+
+--------------------------------------------------------------------------------
+
+type Bifunctor :: forall i j k. (i -> j -> k) -> Constraint
+class (Category (Bildom f), Category (Birdom f), Category (Bicod f)) => Bifunctor (f :: i -> j -> k) where
+ type Bildom f :: Cat i
+ type Birdom f :: Cat j
+ type Bicod f :: Cat k
+
+-- lmap :: Bildom f a b ->
