commit 02d083d8977a8522a1d5909dcacefd027f831af5
parent 1e3c6d28859992b3781cd8f69c261269871a00b6
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 15 Mar 2026 14:46:06 -0700
Complete categorical products and sums
Diffstat:
1 file changed, 36 insertions(+), 57 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -1,6 +1,5 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Algebra.Category (
Cat,
@@ -17,24 +16,6 @@ import Lude.Pair
-- TODO: Allow non-BoxL morphism Repr?
-- TODO: Filterable is functor from Kleisli Option to Hask
--- type Type2 i = i -> i -> Type
--- type Constraint2 i = i -> i -> Constraint
-
--- 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 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
@@ -57,53 +38,51 @@ instance Category Hask where
--------------------------------------------------------------------------------
--- 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
+type Prod :: forall i j. Cat i -> Cat j -> Cat (i × j)
+data Prod p q a b where
+ Prod :: p a0 b0 -> q a1 b1 -> Prod p q '(a0, a1) '(b0, b1)
--- instance (Category p, Category q) => Category (p ×^^ q) where
--- -- type Ob (p ×^^ q) = ProdOb p q
--- type Ob (p ×^^ q) = HasPairEvidence1 (Ob p) (Ob q)
--- identity @a = case pairEvidence @_ @_ @(Ob p) @(Ob q) @a of
--- Pair1 Evidence1 Evidence1 -> Pair2 identity identity
--- compose (Pair2 f0 f1) (Pair2 g0 g1) = Pair2 (compose f0 g0) (compose f1 g1)
+-- We could simplify this, but this way it's consistent with SumOb.
+type ProdOb :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
+class ProdOb p q a where
+ prodOb :: Pair1 (Evidence1 (Ob p)) (Evidence1 (Ob q)) a
+instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
+ prodOb = Pair1 Evidence1 Evidence1
---------------------------------------------------------------------------------
-
--- 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)
+instance (Category p, Category q) => Category (Prod p q) where
+ type Ob (Prod p q) = ProdOb p q
+ identity @a = case prodOb @_ @_ @p @q @a of
+ Pair1 Evidence1 Evidence1 -> Prod identity identity
+ compose (Prod f0 f1) (Prod g0 g1) = Prod (compose f0 g0) (compose f1 g1)
--------------------------------------------------------------------------------
--- type PairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i × j)
--- type PairEvidence1 p q = Pair1 (Evidence1 p) (Evidence1 q)
-
--- type HasPairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Constraint1 (i × j)
--- class HasPairEvidence1 p q a where
--- pairEvidence :: PairEvidence1 p q a
-
--- type EitherEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i + j)
--- type EitherEvidence1 p q = Either1 (Evidence1 p) (Evidence1 q)
+type Sum :: forall i j. Cat i -> Cat j -> Cat (i + j)
+data Sum p q a b where
+ SumL :: p a b -> Sum p q (L a) (L b)
+ SumR :: q a b -> Sum p q (R a) (R b)
+
+type SumOb :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
+class SumOb p q a where
+ sumOb :: Either1 (Evidence1 (Ob p)) (Evidence1 (Ob q)) a
+instance (Ob p a) => SumOb p q (L a) where
+ sumOb = L1 Evidence1
+instance (Ob q a) => SumOb p q (R a) where
+ sumOb = R1 Evidence1
+
+instance (Category p, Category q) => Category (Sum p q) where
+ type Ob (Sum p q) = SumOb p q
+ identity @a = case sumOb @_ @_ @p @q @a of
+ L1 Evidence1 -> SumL identity
+ R1 Evidence1 -> SumR identity
+ compose (SumL f) (SumL g) = SumL (compose f g)
+ compose (SumR f) (SumR g) = SumR (compose f g)
--------------------------------------------------------------------------------
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))
+newtype Nt p q f g where
+ Nt :: (forall a. (Ob p a) => q (f a) (g a)) -> Nt p q f g
type NtOb :: Cat i -> Cat j -> (i -> j) -> Constraint
class (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
