commit 346f45333abdf8571385892aa1547d8202c213f0
parent b91992333672bdeaf9c6749b62ded2023baac0e4
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 9 Sep 2026 17:55:21 -0700
Algebra.Category: add Iso
Diffstat:
3 files changed, 45 insertions(+), 47 deletions(-)
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -366,39 +366,6 @@ newtype Fix2 f i j = Fix2 (f (Fix2 f i j) i j)
{-
-class Category (mor :: obj -> obj -> TypeL) where
- -- If we make morphisms representation-polymorphic, we must modify identity:
- -- {-# MINIMAL (identity | identityU), compose #-}
- -- identity :: (ρ ~ LRep) => mor a a
- -- identity = force identityU
- -- identityU :: Thunk (mor a a)
- -- default identityU :: (ρ ~ LRep) => Thunk (mor a a)
- -- identityU () = identity
- identity :: mor a a
- compose :: mor b c -> mor a b -> mor a c
-
-class (Category (DomOf f)) => Functor (f :: domObj -> Type ρ) where
- type DomOf f :: domObj -> domObj -> TypeL
- map :: DomOf f a b -> (f a -> f b)
-
-class (Category (LDomOf f)) => LFunctor (f :: lDomObj -> k -> Type ρ) where
- type LDomOf f :: lDomObj -> lDomObj -> TypeL
-
- mapl :: LDomOf f a b -> (f a c -> f b c)
- default mapl :: (Bifunctor f) => LDomOf f a b -> (f a c -> f b c)
- mapl = flip bimap identity
-
-class (Category (RDomOf f)) => RFunctor (f :: k -> rDomObj -> Type ρ) where
- type RDomOf f :: rDomObj -> rDomObj -> TypeL
-
- mapr :: RDomOf f a b -> (f c a -> f c b)
- default mapr :: (Bifunctor f) => RDomOf f a b -> (f c a -> f c b)
- mapr = bimap identity
-
-class (LFunctor f, RFunctor f, Category (Hask ρ)) => Bifunctor (f :: lDomObj -> rDomObj -> Type ρ) where
- bimap :: LDomOf f a b -> RDomOf f c d -> (f a c -> f b d)
- bimap f g = mapl f ∘ mapr g
-
type Iso (mor :: obj -> obj -> TypeL) a b = (mor a b, mor b a) -- TODO: use strict pair
class (Bifunctor f, LDomOf f ~ Hask ρ, RDomOf f ~ Hask ρ) => Monoidal (f :: Type ρ -> Type ρ -> Type ρ) where
@@ -420,15 +387,6 @@ class (Monoidal f) => Cartesian (f :: Type ρ -> Type ρ -> Type ρ) where
diag :: forall (a :: Type ρ). a -> f a a
diag = pair identity identity
-type Hask ρ = (->) :: Type ρ -> Type ρ -> TypeL
-
-instance Category (Hask RepL) where
- identity x = x
- compose f g x = f (g x)
-
-(∘) :: (Category mor) => mor b c -> mor a b -> mor a c
-(∘) = compose
-
-}
-- | Right-to-left composition.
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -3,17 +3,16 @@ module Lude.Algebra.Category (
) where
import Lude.Algebra.Category.Bifunctor as X
+import Lude.Algebra.Category.Constrained as X
import Lude.Algebra.Category.Core as X
import Lude.Algebra.Category.Discrete as X
import Lude.Algebra.Category.Hom as X
import Lude.Algebra.Category.Initial as X
+import Lude.Algebra.Category.Iso as X
+import Lude.Algebra.Category.Monad as X
import Lude.Algebra.Category.Terminal as X
--- TODO: Semicategory?
-
--- TODO: Filterable is functor from Kleisli Option to Hask
-
--- TODO: Monads and comonads
+-- TODO: Semicategory? Semimonad? Etc... See semigroups package.
-- TODO: Free and cofree
@@ -24,3 +23,5 @@ import Lude.Algebra.Category.Terminal as X
-- TODO: Profunctors? Other special kinds of functors, given distinct names?
-- That would allow being a functor in multiple ways without losing coherence.
-- E.g., lists could be mappable "normally" and filterable (choose is map).
+
+-- TODO: Filterable is functor from Kleisli Option to Hask
diff --git a/src/Lude/Algebra/Category/Iso.hs b/src/Lude/Algebra/Category/Iso.hs
@@ -0,0 +1,39 @@
+module Lude.Algebra.Category.Iso (
+ Iso (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Haskell
+
+-- TODO: Iso is a groupoid.
+
+--------------------------------------------------------------------------------
+
+-- | An isomorphism (in some category)
+--
+-- In other words, @Iso p@ is the *core* of @p@.
+--
+-- Laws:
+-- - @to . fro = identity@
+-- - @fro . to = identity@
+type Iso :: forall {i}. Cat i -> Cat i
+data Iso p a b = MkIso {to :: a `p` b, fro :: b `p` a}
+
+instance (Categorical p) => Iso p a b `Witnesses` Mor (Iso p) a b where
+ witness (MkIso f _) = MkEvidence \\ witnessMor f
+
+instance (Categorical p) => Categorical (Iso p) where
+ type Obj (Iso p) = Obj p
+ identity = MkIso identity identity
+ compose (MkIso f0 f1) (MkIso g0 g1) = MkIso (f0 . g0) (g1 . f1)
+ witnessMor = witness
+
+instance (Categorical p) => Functorial (Iso p a) where
+ type Dom (Iso p a) = Iso p
+ type Cod (Iso p a) = Function
+ map = compose
+
+instance (Categorical p) => Functorial (Iso p) where
+ type Dom (Iso p) = Dual (Iso p)
+ type Cod (Iso p) = Iso p ==> Function
+ map (MkDual f) = Natural (. f)
