commit 2f411f6a6242544a7795051312651328b8c37932
parent ded67be251b3a619bf3ceddb15251389842b24c2
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 4 Sep 2026 20:21:06 -0700
Reorganize
Diffstat:
14 files changed, 463 insertions(+), 353 deletions(-)
diff --git a/Todo/Constraint.hs b/Todo/Constraint.hs
@@ -0,0 +1,28 @@
+--------------------------------------------------------------------------------
+
+-- infixl 7 :&
+
+--------------------------------------------------------------------------------
+
+-- 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
+
+-- 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 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 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/Algebra/Algebra.hs b/src/Lude/Algebra/Algebra.hs
@@ -1,4 +1,4 @@
-module Algebra.Algebra (
+module Lude.Algebra.Algebra (
Algebra,
Algebraic,
--
@@ -37,10 +37,10 @@ type DefaultRecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
class DefaultRecursive p f r where
defaultCata :: (Algebraic p f r) => forall a. Algebra p f a -> r `p` a
-instance (Coalgebraic Hask f r) => DefaultRecursive Hask f r where
+instance (Coalgebraic Function f r) => DefaultRecursive Function f r where
defaultCata f = h where h = f . map h . peel
instance (Categorical p, Categorical q, Coalgebraic (Nt p q) f r) => DefaultRecursive (Nt p q) f r where
- defaultCata f@(Nt _) = h where h = Nt (comp f . comp (map h) . comp peel) \\ witnessObj (wrap @(Nt p q) @f @r)
+ defaultCata f@(Nt _) = h where h = Nt (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(Nt p q) @f @r)
-- | A type equipped with an initial algebra for an endofunctor.
type Recursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
@@ -66,10 +66,10 @@ type DefaultCorecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
class DefaultCorecursive p g s where
defaultAna :: (Coalgebraic p g s) => forall b. Coalgebra p g b -> b `p` s
-instance (Algebraic Hask g s) => DefaultCorecursive Hask g s where
+instance (Algebraic Function g s) => DefaultCorecursive Function g s where
defaultAna g = h where h = wrap . map h . g
instance (Categorical p, Categorical q, Algebraic (Nt p q) g s) => DefaultCorecursive (Nt p q) g s where
- defaultAna g@(Nt _) = h where h = Nt (comp wrap . comp (map h) . comp g) \\ witnessObj (peel @(Nt p q) @g @s)
+ defaultAna g@(Nt _) = h where h = Nt (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(Nt p q) @g @s)
-- | A type equipped with a final coalgebra for an endofunctor.
type Corecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -1,175 +1,22 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
-
module Lude.Algebra.Category (
- Cat,
- DefaultCat,
- --
- DefaultCategorical (..),
- Categorical (..),
- Mor,
- (.),
- --
- Hask,
- Dual (..),
- --
- DefaultFunctorial (..),
- Functorial (..),
- FunctorialOn,
- Endofunctorial,
- EndofunctorialOn,
- --
- type (~>),
- Nt (..),
+ module X,
) where
-import Lude.Constraint
-import Lude.Kind
-
--- TODO: Semicategory
+import Lude.Algebra.Category.Core as X
+import Lude.Algebra.Category.Dual as X
+import Lude.Algebra.Category.Object as X
--- TODO: Allow non-BoxL morphism Repr?
+-- TODO: Semicategory?
-- TODO: Filterable is functor from Kleisli Option to Hask
---------------------------------------------------------------------------------
-
-infixr 1 ~>
-
---------------------------------------------------------------------------------
-
-type Cat :: Kind -> Kind
-type Cat i = i -> i -> Type
-
-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 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 {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 (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 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)
-
--- 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
-
-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
-
- 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 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 Endofunctorial :: forall {k}. (k -> k) -> Constraint
-class (Functorial f, Dom f ~ Cod f) => Endofunctorial f
-instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f
-
-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
-
---------------------------------------------------------------------------------
-
--- | Natural transformations to Hask
-type (~>) :: forall k r. Cat (k -> Type @r)
-type f ~> g = forall x. f x -> g x
-
-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
-
-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 (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)
-
---------------------------------------------------------------------------------
+-- TODO: Monads and comonads
--- 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 Bildom f = DefaultCat
+-- TODO: Free and cofree
--- type Birdom f :: Cat j
--- type Birdom f = DefaultCat
+-- TODO: Adjunctions and zap
--- type Bicod f :: Cat k
--- type Bicod f = DefaultCat
+-- TODO: Constrained category wrapper (full subcategory with objects subject to
+-- a constraint)
--- lmap :: Bildom f a b ->
+-- TODO: Eilenberg-Moore (co)algebras?
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Lude.Algebra.Category.Core (
+ Cat,
+ DefaultCat,
+ --
+ DefaultCategorical (..),
+ Categorical (..),
+ Mor,
+ (.),
+ --
+ DefaultFunctorial (..),
+ Functorial (..),
+ FunctorialOn,
+ Endofunctorial,
+ EndofunctorialOn,
+ --
+ Nt (..),
+ --
+ Function,
+ type (~>),
+ Entailment,
+ (:-),
+ (:~),
+) where
+
+import Lude.Constraint.Core
+import Lude.Constraint.Entailment
+import Lude.Constraint.Evidence
+import Lude.Constraint.Predicate
+import Lude.Kind
+
+-- TODO: Allow non-BoxL morphism Repr?
+
+--------------------------------------------------------------------------------
+
+infixr 1 ~>
+
+--------------------------------------------------------------------------------
+
+type DefaultCat :: forall i -> Cat i
+type family DefaultCat i
+type instance DefaultCat (Type @r) = Function @r
+type instance DefaultCat (k -> l) = Nt (DefaultCat k) (DefaultCat l)
+
+-- NOTE: This is not allowed, because Type = Constraint :(
+-- type instance DefaultCat Constraint = Entailment
+
+--------------------------------------------------------------------------------
+-- Categories
+
+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
+
+ witnessMor :: forall a b. Witness (a `p` b) (Mor p a b)
+ default witnessMor :: (DefaultCategorical (Obj p) p) => forall a b. Witness (a `p` b) (Mor p a b)
+ witnessMor = 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
+
+--------------------------------------------------------------------------------
+-- Functors
+
+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)
+
+-- 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
+
+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
+
+ 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 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 Endofunctorial :: forall {k}. (k -> k) -> Constraint
+class (Functorial f, Dom f ~ Cod f) => Endofunctorial f
+instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f
+
+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
+
+-- TODO: Bifunctors? Profunctors? Etc... (other kinds of functors?)
+-- That would allow being a functor in multiple ways (without losing coherence).
+-- E.g., lists could be mappable "normally" and filterable (choose is map).
+
+--------------------------------------------------------------------------------
+-- Natural Transformations
+
+type Nt :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
+data Nt p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Nt {comp :: forall a. (Obj p a) => f a `q` g a}
+
+-- at :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j). forall (a :: i) -> (Obj p a) => Nt p q f g -> f a `q` g a
+-- at _ m = comp m
+
+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 (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)
+
+--------------------------------------------------------------------------------
+-- Function
+
+-- We implement this here to avoid orphans.
+
+-- TODO: If Entailment doesn't belong here, then neither does Function. Move it.
+type Function :: forall r. Cat (Type @r)
+type Function @r = (->)
+
+instance Categorical Function where
+ identity x = x
+ compose f g x = f (g x)
+
+-- | Natural transformations to `Function`/`->`
+type (~>) :: forall k r. Cat (k -> Type @r)
+type f ~> g = forall x. f x -> g x
+
+--------------------------------------------------------------------------------
+-- Entailment
+
+-- We implement this here to avoid orphans.
+
+instance Categorical Entailment where
+ identity = entails
+ compose (Entailment f) (Entailment g) = Entailment (f \\ g)
+
+-- | Natural transformations to `Entailment`/`:-`
+type (:~) :: forall k. Cat (k -> Constraint)
+type f :~ g = forall x. f x :- g x
diff --git a/src/Lude/Algebra/Category/Dual.hs b/src/Lude/Algebra/Category/Dual.hs
@@ -0,0 +1,21 @@
+module Lude.Algebra.Category.Dual (
+ Dual (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Constraint.Core
+import Lude.Constraint.Evidence
+
+--------------------------------------------------------------------------------
+
+type Dual :: forall i. Cat i -> Cat i
+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 . witnessMor . unDual
+instance (Categorical p) => Canonically Witnesses (Dual p a b) (Mor (Dual p) a b)
+
+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)
diff --git a/src/Lude/Algebra/Category/Object.hs b/src/Lude/Algebra/Category/Object.hs
@@ -0,0 +1,21 @@
+module Lude.Algebra.Category.Object (
+ HasTerminalObject (..),
+ HasInitialObject (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Kind
+
+--------------------------------------------------------------------------------
+
+type HasTerminalObject :: forall {k}. Cat k -> Constraint
+class (Categorical p) => HasTerminalObject (p :: Cat k) where
+ type Terminal p :: k
+ terminate :: forall a. a `p` Terminal p
+
+--------------------------------------------------------------------------------
+
+type HasInitialObject :: forall {k}. Cat k -> Constraint
+class (Categorical p) => HasInitialObject (p :: Cat k) where
+ type Initial p :: k
+ initiate :: forall a. Initial p `p` a
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -1,45 +1,13 @@
-{-# 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,
- Never,
- never,
- --
- -- Both,
- -- (:&),
- -- Simul,
- --
- -- AllSatisfy,
- -- BothSatisfy,
+ module X,
) where
-import Lude.Kind
+import Lude.Constraint.Core as X
+import Lude.Constraint.Entailment as X
+import Lude.Constraint.Evidence as X
+import Lude.Constraint.Falsum as X
+import Lude.Constraint.Predicate as X
+import Lude.Constraint.Verum as X
-- TODO: "Dual" concept to Witnesses? (Swap roles of types and constraints.)
--
@@ -50,148 +18,4 @@ import Lude.Kind
-- 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 :&
-
---------------------------------------------------------------------------------
-
--- | 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
-
--- | Evidence of a constraint
-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
-
---------------------------------------------------------------------------------
--- Witnesses
-
-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
-
--- | `witness` without the required type argument
-consider :: forall a b. (a :=> b) => Witness a b
-consider = witness b
-
--- | 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 consider a of Evidence -> b
-(\\) = because
-
---------------------------------------------------------------------------------
--- Entailment
-
--- | Evidence that one constraint entails another
-type Entailment :: Constraint -> Constraint -> Type
-newtype Entailment a b = Entailment ((a) => Evidence b)
-
--- | Infix alias for `Entailment`
-type (:-) = Entailment -- NOTE: Add signature once GHC#16754 is resolved
-
-pattern Duh :: forall a b. (a) => (b) => a :- b
-pattern Duh = Entailment Evidence
-{-# COMPLETE Duh #-}
-
-instance forall a b. (a) => Witnesses (a :- b) b where
- 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 Verum :: Constraint
-class Verum
-instance Verum
-
-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 Falsum :: Constraint
-class Falsum where contradiction :: a
-
--- TODO: Generalize to initial objects for any category (also `never`?)
-absurd :: forall a. Falsum :- a
-absurd = Entailment contradiction
-
---------------------------------------------------------------------------------
-
-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 x a. Never x :- a
-never = Entailment contradiction
-
---------------------------------------------------------------------------------
-
--- 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
-
--- 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 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 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
+-- TODO: "Both"/"And" and "Either"/"Or" on constraints
diff --git a/src/Lude/Constraint/Core.hs b/src/Lude/Constraint/Core.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Lude.Constraint.Core (
+ Canonically,
+ Evidence (..),
+ Entailment (..),
+ (:-),
+) where
+
+import Lude.Kind
+
+--------------------------------------------------------------------------------
+
+infixr 1 :-
+
+--------------------------------------------------------------------------------
+
+-- | 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 of a constraint
+type Evidence :: Constraint -> Type
+data Evidence a = (a) => Evidence
+
+-- | Evidence that one constraint entails another
+--
+-- `Entailment` (`:-`) is to `Constraint` what `Function` (`->`) is to `Type`.
+type Entailment :: Cat Constraint
+newtype Entailment a b = Entailment ((a) => Evidence b)
+
+-- | Infix alias for `Entailment`
+type (:-) :: Cat Constraint
+type (:-) = Entailment
diff --git a/src/Lude/Constraint/Entailment.hs b/src/Lude/Constraint/Entailment.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Constraint.Entailment (
+ pattern Duh,
+ entails,
+) where
+
+import Lude.Constraint.Core
+
+--------------------------------------------------------------------------------
+
+pattern Duh :: forall a b. (a) => (b) => a :- b
+pattern Duh = Entailment Evidence
+{-# COMPLETE Duh #-}
+
+entails :: forall a b. ((a) => b) => a :- b
+entails = Entailment Evidence
diff --git a/src/Lude/Constraint/Evidence.hs b/src/Lude/Constraint/Evidence.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Constraint.Evidence (
+ deduce,
+ Witness,
+ Witnesses (..),
+ (:=>),
+ tautology,
+ consider,
+ because,
+ (\\),
+) where
+
+import Lude.Constraint.Core
+import Lude.Kind
+
+--------------------------------------------------------------------------------
+
+infixr 1 :=>
+infixl 4 \\
+
+--------------------------------------------------------------------------------
+
+-- TODO: Can we replace deduce with consider?
+
+-- | Given that `a` implies `b`, deduce evidence of `b` from evidence of `a`
+deduce :: ((a) => b) => Evidence a -> Evidence b
+deduce Evidence = Evidence
+
+--------------------------------------------------------------------------------
+-- Witnesses
+
+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 a conclusion `b` of `a`
+ --
+ -- `a` does not determine `b`, so we require a type argument.
+ 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
+
+-- | Witness the canonical conclusion `b` of `a`
+--
+-- Unlike `witness`, `a` determines `b`, so we don't require a type argument.
+consider :: forall a b. (a :=> b) => Witness a b
+consider = witness b
+
+-- | 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 consider a of Evidence -> b
+(\\) = because
+
+--------------------------------------------------------------------------------
+-- Instances
+
+instance forall a. Witnesses (Evidence a) a where
+ witness _ e = e
+instance forall a. Canonically Witnesses (Evidence a) a
+
+instance forall a b. (a) => Witnesses (a :- b) b where
+ witness _ (Entailment b) = b
+instance forall a b. (a) => Canonically Witnesses (a :- b) b
diff --git a/src/Lude/Constraint/Falsum.hs b/src/Lude/Constraint/Falsum.hs
@@ -0,0 +1,16 @@
+module Lude.Constraint.Falsum (
+ Falsum (..),
+ absurd,
+) where
+
+import Lude.Constraint.Core
+import Lude.Kind
+
+--------------------------------------------------------------------------------
+
+type Falsum :: Constraint
+class Falsum where contradiction :: a
+
+-- TODO: Generalize to initial objects for any category (also `never`?)
+absurd :: forall a. Falsum :- a
+absurd = Entailment contradiction
diff --git a/src/Lude/Constraint/Predicate.hs b/src/Lude/Constraint/Predicate.hs
@@ -0,0 +1,34 @@
+module Lude.Constraint.Predicate (
+ Always,
+ Never,
+ always,
+ never,
+) where
+
+import Lude.Constraint.Core
+import Lude.Constraint.Evidence
+import Lude.Constraint.Falsum
+import Lude.Kind
+
+-- TODO: I don't like this organization. Why isn't Always/Never treated the
+-- same as Verum/Falsum?
+
+--------------------------------------------------------------------------------
+
+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 x a. Never x :- a
+never = Entailment contradiction
diff --git a/src/Lude/Constraint/Verum.hs b/src/Lude/Constraint/Verum.hs
@@ -0,0 +1,21 @@
+module Lude.Constraint.Verum (
+ Verum,
+ trivial,
+) where
+
+import Lude.Constraint.Core
+import Lude.Constraint.Evidence
+import Lude.Kind
+
+--------------------------------------------------------------------------------
+
+type Verum :: Constraint
+class Verum
+instance Verum
+
+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
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -22,6 +22,7 @@ module Lude.Kind (
Lev,
Endo,
BiEndo,
+ Cat,
) where
import Data.Tuple.Experimental qualified as GHC
@@ -95,6 +96,9 @@ type Endo k = k -> k
type BiEndo :: Kind -> Kind
type BiEndo k = k -> k -> k
+type Cat :: Kind -> Kind
+type Cat i = i -> i -> Type
+
--------------------------------------------------------------------------------
-- Defunctionalization
