commit 0571baab02bb4549c48e76409850ec6cd6ec0bcc
parent f685675d274d40dcb120afb707a44bd201e74de9
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 3 Sep 2026 21:22:11 -0700
Update category stuff
Diffstat:
6 files changed, 288 insertions(+), 341 deletions(-)
diff --git a/Todo/Category.hs b/Todo/Category.hs
@@ -0,0 +1,41 @@
+--------------------------------------------------------------------------------
+
+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)
+
+-- We could simplify this, but this way it's consistent with SumObj.
+type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
+class ProdObj p q a where
+ prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
+ prodObj = Pair1 Evidence1 Evidence1
+
+instance (Categorical p, Categorical q) => Categorical (Prod p q) where
+ type Obj (Prod p q) = ProdObj p q
+ identity @a = case prodObj @_ @_ @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 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 SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
+class SumObj p q a where
+ sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+instance (Obj p a) => SumObj p q (L a) where
+ sumObj = L1 Evidence1
+instance (Obj q a) => SumObj p q (R a) where
+ sumObj = R1 Evidence1
+
+instance (Categorical p, Categorical q) => Categorical (Sum p q) where
+ type Obj (Sum p q) = SumObj p q
+ identity @a = case sumObj @_ @_ @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)
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -1,205 +0,0 @@
-{-# OPTIONS_GHC -Wno-unused-top-binds #-}
-
-module Lude.Algebra (
- Cat,
- Category (..),
- Functor (..),
- Bifunctor (..),
- Hask,
- Op (..),
-) where
-
-import Data.Set (Set)
-import Data.Set qualified as Set
-import Prelude (Ord)
-
-import Lude.Kind
-import Lude.Repr (Repr)
-import Lude.Repr qualified as Repr
-
---------------------------------------------------------------------------------
--- Category
-
-type Cat k r = k -> k -> Type @r
-
-type Category :: forall k r. Cat k r -> Constraint
-class Category (cat :: Cat k r) where
- type Ob @k @(r :: Repr) cat (a :: k) :: Constraint
- type Ob cat a = ()
- identity :: (Ob cat a) => cat a a
- compose :: (Ob3 cat a b c) => cat b c -> cat a b -> cat a c
-
-type Ob2 :: forall k r. Cat k r -> k -> k -> Constraint
-type Ob2 cat a b = (Ob cat a, Ob cat b)
-
-type Ob3 :: forall k r. Cat k r -> k -> k -> k -> Constraint
-type Ob3 cat a b c = (Ob2 cat a b, Ob cat c)
-
-type Ob4 :: forall k r. Cat k r -> k -> k -> k -> k -> Constraint
-type Ob4 cat a b c d = (Ob3 cat a b c, Ob cat d)
-
---------------------------------------------------------------------------------
--- Functor
-
-type Functor :: forall k0 k1 r0 r1. Cat k0 r0 -> Cat k1 r1 -> (k0 -> k1) -> Constraint
-class (Category cat0, Category cat1) => Functor cat0 cat1 f | cat0 f -> cat1, cat1 f -> cat0 where
- map :: (Ob2 cat0 a b, Ob2 cat1 (f a) (f b)) => cat0 a b -> cat1 (f a) (f b)
-
-type Endofunctor :: forall k r. Cat k r -> (k -> k) -> Constraint
-type Endofunctor cat f = Functor cat cat f
-
-type Constrained :: forall k r. Cat k r -> (k -> Constraint) -> k -> k -> TypeL
-newtype Constrained cat obj a b = Constrained ((obj a, obj b) => cat a b)
-
-type (:-) :: forall k r. (k -> Constraint) -> Cat k r -> k -> k -> TypeL
-type obj :- cat = Constrained cat obj
-
-instance (Category cat) => Category (obj :- cat) where
- type Ob (obj :- cat) a = (Ob cat a, obj a)
- identity = Constrained identity
- compose (Constrained f) (Constrained g) = Constrained (compose f g)
-
-instance Functor (Ord :- Hask) Hask Set where
- map (Constrained f) = Set.map f
-
---------------------------------------------------------------------------------
--- Bifunctor
-
-type ObLmap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k0 -> k1 -> Constraint
-type ObLmap cat0 cat1 cat2 f a b c = (Ob2 cat0 a b, Ob cat1 c, Ob2 cat2 (f a c) (f b c))
-
-type OpRmap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k1 -> k1 -> Constraint
-type OpRmap cat0 cat1 cat2 f a c d = (Ob cat0 a, Ob2 cat1 c d, Ob2 cat2 (f a c) (f a d))
-
-type OpBimap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k0 -> k1 -> k1 -> Constraint
-type OpBimap cat0 cat1 cat2 f a b c d = (Ob2 cat0 a b, Ob2 cat1 c d, Ob4 cat2 (f a c) (f a d) (f b c) (f b d))
-
-type BifunctorRep :: Repr -> Repr -> Repr -> Constraint
-class BifunctorRep r0 r1 r2 where
- lmapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a b c. (Bifunctor cat0 cat1 cat2 f, ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
- rmapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a c d. (Bifunctor cat0 cat1 cat2 f, OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
- bimapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a b c d. (Bifunctor cat0 cat1 cat2 f, OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
-
-instance BifunctorRep Repr.BoxL Repr.BoxL Repr.BoxL where
- lmapD l = bimap l identity
- rmapD r = bimap identity r
- bimapD l r = compose (lmap l) (rmap r)
-
-type Bifunctor :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
-class (Category cat0, Category cat1, Category cat2) => Bifunctor @k0 @k1 @k2 @r0 @r1 @r2 cat0 cat1 cat2 f | cat0 f -> cat1 cat2, cat1 f -> cat0 cat2, cat2 f -> cat0 cat1 where
- {-# MINIMAL lmap, rmap | bimap #-}
-
- lmap :: (ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
- default lmap :: (BifunctorRep r0 r1 r2, ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
- lmap = lmapD
-
- rmap :: (OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
- default rmap :: (BifunctorRep r0 r1 r2, OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
- rmap = rmapD
-
- bimap :: (OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
- default bimap :: (BifunctorRep r0 r1 r2, OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
- bimap = bimapD
-
-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 :: (Ob3 cat a b c) => cat (f (f a b) c) (f a (f b c))
- coassoc :: (Ob3 cat a b c) => 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 :: (Ob cat a) => cat (f (IdObj cat f) a) a
- idr :: (Ob cat a) => cat (f a (IdObj cat f)) a
- coidl :: (Ob cat a) => cat a (f (IdObj cat f) a)
- coidr :: (Ob cat a) => 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. Cat (Type @r) Repr.BoxL
-type Hask @r = (->)
-
-instance Category (Hask @Repr.BoxL) 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
- -- lmap f (a, b) = (f a, b)
- -- rmap f (a, b) = (a, f b)
- 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
- type Ob (Op cat) a = Ob cat a
- identity = Op identity
- compose (Op f) (Op g) = Op (compose g f)
-
---------------------------------------------------------------------------------
-
--- | Natural transformations to Hask
-type (~>) :: forall k (r :: Repr). Cat (k -> Type @r) Repr.BoxL
-type f ~> g = forall a. f a -> g a
-
-{-
-
-data Natrans -- TODO: Rename Funct
-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
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -1,16 +1,30 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Algebra.Category (
Cat,
- Category (..),
- Functor (..),
+ DefaultCat,
+ --
+ DefaultCategorical (..),
+ Categorical (..),
+ Mor,
+ (.),
+ --
+ Hask,
+ Dual (..),
+ --
+ DefaultFunctorial (..),
+ Functorial (..),
+ FunctorialOn,
+ Endofunctorial,
+ EndofunctorialOn,
+ --
+ type (~>),
+ Nt (..),
) where
import Lude.Constraint
-import Lude.Either
import Lude.Kind
-import Lude.Pair
-- TODO: Semicategory
@@ -20,119 +34,130 @@ import Lude.Pair
--------------------------------------------------------------------------------
+infixr 1 ~>
+
+--------------------------------------------------------------------------------
+
+type Cat :: Kind -> Kind
type Cat i = i -> i -> Type
-type Category :: forall i. Cat i -> Constraint
-class Category (p :: Cat i) where
- type Obj p :: Constraint1 i
- type Obj p = Always1
- identity :: (Obj p a) => p a a
- compose :: p b c -> p a b -> p a c
+type DefaultCat :: forall i -> Cat i
+type family DefaultCat i
+type instance DefaultCat (Type @r) = Hask @r
+type instance DefaultCat (k -> l) = Nt (DefaultCat k) (DefaultCat l)
+
+--------------------------------------------------------------------------------
+
+type DefaultCategorical :: forall {i}. Predicate i -> Cat i -> Constraint
+class DefaultCategorical obj p where
+ defaultWitnessObj :: (Categorical p, Obj p ~ obj) => forall a b. Witness (a `p` b) (Mor p a b)
+
+instance {-# INCOHERENT #-} (forall a b. p a b `Witnesses` Mor p a b) => DefaultCategorical obj p where
+ defaultWitnessObj = witness _
+instance {-# INCOHERENT #-} DefaultCategorical Always p where
+ defaultWitnessObj = tautology
+
+type Categorical :: forall {i}. Cat i -> Constraint
+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
+
+ witnessObj :: forall a b. Witness (a `p` b) (Mor p a b)
+ default witnessObj :: (DefaultCategorical (Obj p) p) => forall a b. Witness (a `p` b) (Mor p a b)
+ witnessObj = defaultWitnessObj
+
+type Mor :: forall {i}. Cat i -> i -> i -> Constraint
+class (Obj p a, Obj p b) => Mor p a b
+instance (Obj p a, Obj p b) => Mor p a b
+
+(.) :: forall {i} (p :: Cat i) a b c. (Categorical p) => b `p` c -> a `p` b -> a `p` c
+(.) = compose
--------------------------------------------------------------------------------
+-- TODO: Move these?
+
type Hask :: forall r. Cat (Type @r)
type Hask @r = (->)
-instance Category Hask where
+instance Categorical Hask where
identity x = x
compose f g x = f (g x)
---------------------------------------------------------------------------------
-
type Dual :: forall i. Cat i -> Cat i
-newtype Dual p a b = Dual (p b a)
+newtype Dual p a b = Dual {unDual :: p b a}
+
+instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b where
+ witness _ = deduce . witnessObj . unDual
+instance (Categorical p) => Canonically Witnesses (Dual p a b) (Mor (Dual p) a b)
-instance (Category p) => Category (Dual p) where
+instance (Categorical p) => Categorical (Dual p) where
type Obj (Dual p) = Obj p
identity = Dual identity
compose (Dual f) (Dual g) = Dual (compose g f)
--------------------------------------------------------------------------------
-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)
+type DefaultFunctorial :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constraint
+class DefaultFunctorial p q f where
+ defaultPreserveObj :: (Functorial f, Dom f ~ p, Cod f ~ q) => forall a. Obj p a :- Obj q (f a)
--- We could simplify this, but this way it's consistent with SumObj.
-type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
-class ProdObj p q a where
- prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
-instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
- prodObj = Pair1 Evidence1 Evidence1
+-- TODO: DefaultFunctorial instances. Should they be incoherent?
+-- instance (forall a. (Obj p a) => FunctorialOn q r (f a)) => DefaultFunctorial p (Nt q r) f where
+-- defaultPreserveObj = entails
+-- instance DefaultFunctorial p Hask f where
+-- defaultPreserveObj = always
-instance (Category p, Category q) => Category (Prod p q) where
- type Obj (Prod p q) = ProdObj p q
- identity @a = case prodObj @_ @_ @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 Functorial :: forall {i} {j}. (i -> j) -> Constraint
+class (Categorical (Dom f), Categorical (Cod f)) => Functorial (f :: i -> j) where
+ type Dom f :: Cat i
+ type Dom @i f = DefaultCat i
---------------------------------------------------------------------------------
+ type Cod f :: Cat j
+ type Cod @j f = DefaultCat j
-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 SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
-class SumObj p q a where
- sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
-instance (Obj p a) => SumObj p q (L a) where
- sumObj = L1 Evidence1
-instance (Obj q a) => SumObj p q (R a) where
- sumObj = R1 Evidence1
-
-instance (Category p, Category q) => Category (Sum p q) where
- type Obj (Sum p q) = SumObj p q
- identity @a = case sumObj @_ @_ @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)
+ map :: forall a b. Dom f a b -> Cod f (f a) (f b)
---------------------------------------------------------------------------------
+ preserveObj :: forall a. Obj (Dom f) a :- Obj (Cod f) (f a)
+ default preserveObj :: (DefaultFunctorial (Dom f) (Cod f) f) => forall a. Obj (Dom f) a :- Obj (Cod f) (f a)
+ preserveObj = defaultPreserveObj
-type Nt :: forall i j. Cat i -> Cat j -> Cat (i -> j)
-newtype Nt p q f g where
- Nt :: (forall a. (Obj p a) => q (f a) (g a)) -> Nt p q f g
+type FunctorialOn :: forall {k} {l}. Cat k -> Cat l -> (k -> l) -> Constraint
+class (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f | f -> p q
+instance (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f
-type NtObj :: Cat i -> Cat j -> (i -> j) -> Constraint
-class (Functor f, Dom f ~ p, Cod f ~ q) => NtObj p q f
-instance (Functor f, Dom f ~ p, Cod f ~ q) => NtObj p q f
+type Endofunctorial :: forall {k}. (k -> k) -> Constraint
+class (Functorial f, Dom f ~ Cod f) => Endofunctorial f
+instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f
-instance (Category p, Category q) => Category (Nt p q) where
- type Obj (Nt p q) = NtObj p q
- identity @f = Nt \ @a -> identity `because` (preserveObj :: Obj p a :- Obj q (f a))
- compose (Nt a) (Nt b) = Nt (compose a b)
+type EndofunctorialOn :: forall {k}. Cat k -> (k -> k) -> Constraint
+class (FunctorialOn p p f) => EndofunctorialOn p f | f -> p
+instance (FunctorialOn p p f) => EndofunctorialOn p f
--------------------------------------------------------------------------------
-type family DefaultCat :: Cat i
-type instance DefaultCat @(Type @r) = Hask @r
+-- | Natural transformations to Hask
+type (~>) :: forall k r. Cat (k -> Type @r)
+type f ~> g = forall x. f x -> g x
-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
-
- preserveObj :: Obj (Dom f) a :- Obj (Cod f) (f a)
- default preserveObj :: (Obj (Cod f) ~ Always1) => Obj (Dom f) a :- Obj (Cod f) (f a)
- preserveObj = always1
+type Nt :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
+data Nt p q f g where
+ Nt
+ :: (FunctorialOn p q f, FunctorialOn p q g)
+ => (forall a. (Obj p a) => f a `q` g a)
+ -> Nt p q f g
- map :: Dom f a b -> Cod f (f a) (f b)
+instance Nt p q f g `Witnesses` Mor (Nt p q) f g where
+ witness _ (Nt _) = Evidence
+instance Canonically Witnesses (Nt p q f g) (Mor (Nt p q) f g)
-instance Functor (Pair b) where
- map f (b, a) = (b, f a)
-
-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)
+instance (Categorical p, Categorical q) => Categorical (Nt p q) where
+ type Obj (Nt p q) = FunctorialOn p q
+ identity @f = Nt \ @a -> identity \\ (preserveObj :: Obj p a :- Obj q (f a))
+ compose (Nt a) (Nt b) = Nt (compose a b)
--------------------------------------------------------------------------------
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -1,43 +1,70 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Constraint (
+ Canonically,
+ --
Evidence (..),
+ deduce,
Evidence1 (..),
--
+ Witness,
Witnesses (..),
(:=>),
+ tautology,
+ consider,
because,
(\\),
--
Entailment (..),
(:-),
pattern Duh,
+ entails,
+ --
+ Verum,
+ trivial,
+ Falsum (..),
+ absurd,
--
Always,
always,
- --
- Always1,
- always1,
- --
- Never (..),
+ Never,
never,
--
- Never1 (..),
- never1,
+ -- Both,
+ -- (:&),
+ -- Simul,
--
- Both,
- (:&),
+ -- AllSatisfy,
+ -- BothSatisfy,
) where
-import Prelude.Experimental qualified as GHC
-
import Lude.Kind
+-- TODO: "Dual" concept to Witnesses? (Swap roles of types and constraints.)
+--
+-- type Induces :: Constraint -> Type -> Constraint
+-- class Induces a b where
+-- induce :: (a) => b
+
+-- TODO: In multiple places, we have the same thing "normally" and with an
+-- index. This should be abstracted-out.
+
+-- TODO: "Either"/"Or" on constraints
+
--------------------------------------------------------------------------------
+infixr 1 :=>, :-
infixl 4 \\
-infixl 7 :&
-infixr 9 :=>, :-
+
+-- infixl 7 :&
+
+--------------------------------------------------------------------------------
+
+-- | Constrain a relation @a `r` b@ to have a *canonical* `b` per `a` (i.e.,
+-- `r` is a "function")
+type Canonically :: forall {k} {l}. Endo (Relation k l)
+class (a `r` b) => Canonically r a b | r a -> b
--------------------------------------------------------------------------------
-- Evidence
@@ -46,6 +73,13 @@ infixr 9 :=>, :-
type Evidence :: Constraint -> Type
data Evidence a = (a) => Evidence
+instance forall a. Witnesses (Evidence a) a where
+ witness _ e = e
+instance forall a. Canonically Witnesses (Evidence a) a
+
+deduce :: ((a) => b) => Evidence a -> Evidence b
+deduce Evidence = Evidence
+
-- TODO: Delete?
type Evidence1 :: forall {i}. Constraint1 i -> Type1 i
data Evidence1 p a = (p a) => Evidence1
@@ -53,22 +87,31 @@ data Evidence1 p a = (p a) => Evidence1
--------------------------------------------------------------------------------
-- Witnesses
--- | Constrain a type to carry evidence of a constraint
-type Witnesses :: Type -> Constraint -> Constraint
-class Witnesses a b | a -> b where
- witness :: a -> Evidence b
+type Witness :: Type -> Constraint -> Type
+type Witness a b = a -> Evidence b
+
+-- | Relation that a type carries evidence of a constraint
+type Witnesses :: Relation Type Constraint
+class Witnesses a b where
+ witness :: forall b' -> (b' ~ b) => Witness a b'
+
+-- | Infix alias for @Canonically Witnesses@
+type (:=>) :: Relation Type Constraint
+type (:=>) = Canonically Witnesses
+
+tautology :: forall a b. (b) => Witness a b
+tautology _ = Evidence
--- | Infix alias for `Witnesses`
-type (:=>) = Witnesses -- NOTE: Add signature once GHC#16754 is resolved
+-- | `witness` without the required type argument
+consider :: forall a b. (a :=> b) => Witness a b
+consider = witness b
--- | Given that `a` witnesses `c`, resolve a `c`-predicated `b` with an `a`
+-- | Given that `a` (canonically) witnesses `c`, resolve a `c`-predicated
+-- `b` with an `a`
because, (\\) :: forall a b c. (a :=> c) => ((c) => b) -> a -> b
-b `because` a = case witness a of Evidence -> b
+b `because` a = case consider a of Evidence -> b
(\\) = because
-instance forall a. Witnesses (Evidence a) a where
- witness e = e
-
--------------------------------------------------------------------------------
-- Entailment
@@ -84,45 +127,71 @@ pattern Duh = Entailment Evidence
{-# COMPLETE Duh #-}
instance forall a b. (a) => Witnesses (a :- b) b where
- witness (Entailment b) = b
+ witness _ (Entailment b) = b
+instance forall a b. (a) => Canonically Witnesses (a :- b) b
+
+entails :: forall a b. ((a) => b) => a :- b
+entails = Entailment Evidence
--------------------------------------------------------------------------------
-type Always :: Constraint
-class Always
-instance Always
+type Verum :: Constraint
+class Verum
+instance Verum
-always :: forall a. a :- Always
-always = Entailment Evidence
+instance forall a. Witnesses a Verum where
+ witness _ _ = Evidence
---------------------------------------------------------------------------------
+-- TODO: Generalize to terminal objects for any category (also `always`?)
+trivial :: forall a. a :- Verum
+trivial = Entailment Evidence
-type Always1 :: forall {i}. Constraint1 i
-class Always1 x
-instance Always1 x
+type Falsum :: Constraint
+class Falsum where contradiction :: a
-always1 :: forall a x. a :- Always1 x
-always1 = Entailment Evidence
+-- TODO: Generalize to initial objects for any category (also `never`?)
+absurd :: forall a. Falsum :- a
+absurd = Entailment contradiction
--------------------------------------------------------------------------------
-type Never :: Constraint
-class Never where contradiction :: a
+type Always :: forall {i}. Predicate i
+class Always x
+instance forall x. Always x
+
+instance forall a x. Witnesses a (Always x) where
+ witness _ _ = Evidence
+
+always :: forall a x. a :- Always x
+always = Entailment Evidence
+
+type Never :: forall {i}. Predicate i
+class (Falsum) => Never x
-never :: forall a. Never :- a
+never :: forall x a. Never x :- a
never = Entailment contradiction
--------------------------------------------------------------------------------
-type Never1 :: forall {i}. Constraint1 i
-class Never1 x where contradiction1 :: a
+-- type Both :: Constraint -> Constraint -> Constraint
+-- type Both = GHC.CTuple2
+-- type (:&) = Both -- NOTE: Add signature once GHC#16754 is resolved
+-- instance forall a b c. (a `Witnesses` b, a `Witnesses` c) => a `Witnesses` (b :& c) where
+-- witness _ a = Evidence \\ witness b a \\ witness c a
-never1 :: forall x a. Never1 x :- a
-never1 @x = Entailment (contradiction1 @x)
+-- type Simul :: forall {i}. Predicate i -> Predicate i -> Predicate i
+-- class (p i, q i) => Simul p q i
+-- instance (p i, q i) => Simul p q i
--------------------------------------------------------------------------------
-type Both :: Constraint -> Constraint -> Constraint
-type Both = GHC.CTuple2
+-- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint
+-- type family AllSatisfy p xs where
+-- AllSatisfy _ [] = Verum
+-- AllSatisfy p (x : xs) = p x :& AllSatisfy p xs
-type (:&) = Both -- NOTE: Add signature once GHC#16754 is resolved
+-- type BothSatisfy :: forall {i}. Predicate i -> i -> i -> Constraint
+-- class (p x, p y) => BothSatisfy p x y
+-- instance (p x, p y) => BothSatisfy p x y
+-- instance forall a p x y. (a `Witnesses` p x, a `Witnesses` p y) => a `Witnesses` BothSatisfy p x y where
+-- witness _ a = Evidence \\ witness (p x) a \\ witness (p y) a
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -16,6 +16,8 @@ module Lude.Kind (
ConstraintL,
ConstraintU,
Constraint1,
+ Predicate,
+ Relation,
--
Lev,
Endo,
@@ -33,9 +35,13 @@ import Lude.Repr qualified as Repr
type Kind = GHC.TYPE Repr.BoxL
+-- | The kind of "invisibly" `Repr`-generic things
+type KindR :: Kind
+type KindR = forall (r :: Repr). Kind
+
--------------------------------------------------------------------------------
-type Type :: forall (r :: Repr). Kind
+type Type :: KindR
type Type @r = GHC.TYPE r
type TypeL = Type @Repr.BoxL
@@ -44,6 +50,9 @@ type TypeU = Type @Repr.BoxU
type Type1 :: forall (r :: Repr). Kind -> Kind
type Type1 @r i = i -> Type @r
+-- type Fam :: Kind -> KindR
+-- type Fam i @r = i -> Type @r
+
-- TODO: What's this for? I forget.
type AnyType :: Kind
data AnyType = forall (r :: Repr). MkAnyType (Type @r)
@@ -56,8 +65,16 @@ type Constraint @r = GHC.CONSTRAINT r
type ConstraintL = Constraint @Repr.BoxL
type ConstraintU = Constraint @Repr.BoxU
-type Constraint1 :: forall (r :: Repr). Kind -> Kind
-type Constraint1 @r i = i -> Constraint @r
+-- TODO: Delete in favor of Predicate? We'd also need a replacement name for
+-- Type1.
+type Constraint1 :: Kind -> forall (r :: Repr). Kind
+type Constraint1 k @r = Predicate k @r
+
+type Predicate :: Kind -> forall (r :: Repr). Kind
+type Predicate k @r = k -> Constraint @r
+
+type Relation :: Kind -> Kind -> forall (r :: Repr). Kind
+type Relation k l @r = k -> l -> Constraint @r
--------------------------------------------------------------------------------
diff --git a/src/Lude/Pair.hs b/src/Lude/Pair.hs
@@ -19,8 +19,8 @@ import Lude.Bool
import Lude.Kind
import Lude.Repr (Repr)
import Lude.Repr qualified as Repr
-import Prelude.Experimental qualified as GHC
import Prelude qualified
+import Prelude.Experimental qualified as GHC
-- TODO: Generalize fst and snd (and fst1 and snd1?) with Cartesian class.
-- Probably name them outl and outr for symmetry with inl and inr.
