commit dbef37fab440d8243484712e6b4a50829383f3a9
parent d5ef98e05fee7facfc4b086cfa28af931daeb037
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 1 Mar 2026 18:21:33 -0800
Add work on generalized category type classes
I'm gonna simplify to the case where objects in categories have to be types
(of some representation). Haskell just doesn't have very good support for
dealing with non-type things (e.g., newtypes can only define types).
Diffstat:
2 files changed, 133 insertions(+), 1 deletion(-)
diff --git a/package.yaml b/package.yaml
@@ -1,5 +1,5 @@
name: lude
-version: 0.1.0.0
+version: 0.0.0
license: ISC
author: "Robert Russell"
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -0,0 +1,132 @@
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+module Lude.Algebra (
+ Category (..),
+ Functor (..),
+ Hask,
+ Op (..),
+) where
+
+import Lude.Kind
+import Lude.Repr (Repr)
+import Lude.Repr qualified as Repr
+
+-- TODO: Defaults for lmap, rmap, bimap
+
+--------------------------------------------------------------------------------
+
+type Cat k r = k -> k -> Type r
+
+type Category :: forall k (r :: Repr). Cat k r -> Constraint
+class Category cat where
+ identity :: Lev (cat a a)
+ compose :: cat b c -> cat a b -> cat a c
+
+type Functor :: forall k0 k1 (r0 :: Repr) (r1 :: Repr). Cat k0 r0 -> Cat k1 r1 -> (k0 -> k1) -> Constraint
+class (Category cat0, Category cat1) => Functor cat0 cat1 f where
+ map :: cat0 a b -> cat1 (f a) (f b)
+
+type Endofunctor :: forall k (r :: Repr). Cat k r -> (k -> k) -> Constraint
+type Endofunctor cat f = Functor cat cat f
+
+type LFunctor :: forall k0 k1 k2 (r0 :: Repr) (r2 :: Repr). Cat k0 r0 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
+class (Category cat0, Category cat2) => LFunctor cat0 cat2 f where
+ lmap :: cat0 a b -> cat2 (f a c) (f b c)
+
+type RFunctor :: forall k0 k1 k2 (r1 :: Repr) (r2 :: Repr). Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
+class (Category cat1, Category cat2) => RFunctor cat1 cat2 f where
+ rmap :: cat1 c d -> cat2 (f a c) (f a d)
+
+type Bifunctor :: forall k0 k1 k2 (r0 :: Repr) (r1 :: Repr) (r2 :: Repr). Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
+class (LFunctor cat0 cat2 f, RFunctor cat1 cat2 f) => Bifunctor cat0 cat1 cat2 f where
+ bimap :: cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
+
+type Biendofunctor :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
+type Biendofunctor cat f = Bifunctor cat cat cat f
+
+type Hypoplexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
+class (Biendofunctor cat f) => Hypoplexal cat f where
+ assoc :: Lev (cat (f (f a b) c) (f a (f b c)))
+ coassoc :: Lev (cat (f a (f b c)) (f (f a b) c))
+
+type Plexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
+class (Hypoplexal cat f) => Plexal @k cat f where
+ type IdObj cat f :: k
+ idl :: Lev (cat (f (IdObj cat f) a) a)
+ idr :: Lev (cat (f a (IdObj cat f)) a)
+ coidl :: Lev (cat a (f (IdObj cat f) a))
+ coidr :: Lev (cat a (f a (IdObj cat f)))
+
+-- type Hyperplexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
+-- class (Plexal cat f) => Hyperplexal @k cat f where
+-- type InvObj cat f :: k -> k
+-- invl :: Lev (cat (f (InvObj cat f a) a) (IdObj cat f))
+-- invr :: Lev (cat (f a (InvObj cat f a)) (IdObj cat f))
+-- coinvl :: Lev (cat (IdObj cat f) (f (InvObj cat f a) a))
+-- coinvr :: Lev (cat (IdObj cat f) (f a (InvObj cat f a)))
+
+--------------------------------------------------------------------------------
+
+type Hask :: forall (r :: Repr). Cat (Type r) Repr.BoxL
+type Hask @r = (->)
+
+instance Category Hask where
+ identity x = x
+ compose f g x = f (g x)
+
+instance LFunctor Hask Hask (,) where lmap f (a, b) = (f a, b)
+instance RFunctor Hask Hask (,) where rmap f (a, b) = (a, f b)
+instance Bifunctor Hask Hask Hask (,) where bimap f g (a, b) = (f a, g b)
+instance Hypoplexal Hask (,) where
+ assoc ((a, b), c) = (a, (b, c))
+ coassoc (a, (b, c)) = ((a, b), c)
+instance Plexal Hask (,) where
+ type IdObj Hask (,) = ()
+ idl ((), a) = a
+ idr (a, ()) = a
+ coidl a = ((), a)
+ coidr a = (a, ())
+
+--------------------------------------------------------------------------------
+
+type Op :: forall k (r :: Repr). Cat k r -> Cat k r
+newtype Op cat a b = Op (cat b a)
+
+instance (Category cat) => Category (Op cat) where
+ identity = Op identity
+ compose (Op f) (Op g) = Op (compose g f)
+
+--------------------------------------------------------------------------------
+
+type Funct :: forall k0 k1 (r0 :: Repr) (r1 :: Repr). Cat k0 r0 -> Cat k1 r1 -> Cat (k0 -> k1) r1
+newtype Funct _cat0 cat1 f g = Funct (forall a. cat1 (f a) (g a))
+
+type Endofunct :: forall k (r :: Repr). Cat k r -> Cat (k -> k) r
+type Endofunct cat = Funct cat cat
+
+instance (Category cat0, Category cat1) => Category (Funct cat0 cat1) where
+ identity = Funct identity
+ compose (Funct f) (Funct g) = Funct (compose f g)
+
+type Id :: (TypeL -> TypeL) -> (TypeL -> TypeL)
+newtype Id f a = Id {unId :: f a}
+instance Functor (Endofunct Hask) (Endofunct Hask) Id where
+ -- map :: Endofunct Hask f g -> Endofunct Hask (Id f) (Id g)
+ -- (forall a. f a -> g a) (forall a. Id f a -> Id g a)
+ map (Funct n) = Funct (Id `compose` n `compose` unId)
+
+type Compose :: (TypeL -> TypeL) -> (TypeL -> TypeL) -> (TypeL -> TypeL)
+newtype Compose f g a = Compose {unCompose :: f (g a)}
+instance LFunctor (Endofunct Hask) (Endofunct Hask) Compose where
+ lmap (Funct n) = Funct (Compose `compose` n `compose` unCompose)
+instance RFunctor (Endofunct Hask) (Endofunct Hask) Compose where
+ rmap (Funct n) = Funct (Compose `compose` n `compose` unCompose)
+
+--------------------------------------------------------------------------------
+
+-- type HypoMonoid :: forall r. Type r -> Constraint
+-- class HypoMonoid a where
+-- combine :: a -> a -> a
+-- type Monoid :: forall r. Type r -> Constraint
+-- class (HypoMonoid a) => Monoid a where
+-- unit :: a
