commit 93a5e6c5f53b3ea8f11a226c43ffc34701946fc1
parent 3c311c8c62b2c5234d57ff5fc7023be6d4838173
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 4 Sep 2026 21:23:36 -0700
Remove puns
Diffstat:
9 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/src/Lude/Algebra/Algebra.hs b/src/Lude/Algebra/Algebra.hs
@@ -40,7 +40,7 @@ class DefaultRecursive p 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) \\ witnessMor (wrap @(Nt p q) @f @r)
+ defaultCata f@(MkNt _) = h where h = MkNt (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
@@ -69,7 +69,7 @@ class DefaultCorecursive p 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) \\ witnessMor (peel @(Nt p q) @g @s)
+ defaultAna g@(MkNt _) = h where h = MkNt (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/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -125,19 +125,19 @@ instance (FunctorialOn p p f) => EndofunctorialOn p f
-- 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}
+data Nt p q f g = (FunctorialOn p q f, FunctorialOn p q g) => MkNt {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
type instance Canonical Witnesses (Nt p q f g) = Mor (Nt p q) f g
instance Nt p q f g `Witnesses` Mor (Nt p q) f g where
- witness _ (Nt _) = Evidence
+ witness _ (MkNt _) = MkEvidence
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)
+ identity @f = MkNt \ @a -> identity \\ (preserveObj :: Obj p a :- Obj q (f a))
+ compose (MkNt a) (MkNt b) = MkNt (compose a b)
--------------------------------------------------------------------------------
-- Function
@@ -150,7 +150,7 @@ type Function @r = (->)
instance Categorical Function where
identity x = x
- compose f g x = f (g x)
+ compose f g = \x -> f (g x)
-- | Natural transformations to `Function`/`->`
type (~>) :: forall k r. Cat (k -> Type @r)
@@ -163,7 +163,7 @@ type f ~> g = forall x. f x -> g x
instance Categorical Entailment where
identity = entails
- compose (Entailment f) (Entailment g) = Entailment (f \\ g)
+ compose (MkEntailment f) (MkEntailment g) = MkEntailment (f \\ g)
-- | Natural transformations to `Entailment`/`:-`
type (:~) :: forall k. Cat (k -> Constraint)
diff --git a/src/Lude/Algebra/Category/Dual.hs b/src/Lude/Algebra/Category/Dual.hs
@@ -9,7 +9,7 @@ import Lude.Constraint.Evidence
--------------------------------------------------------------------------------
type Dual :: forall i. Cat i -> Cat i
-newtype Dual p a b = Dual {unDual :: p b a}
+newtype Dual p a b = MkDual {unDual :: p b a}
type instance Canonical Witnesses (Dual p a b) = Mor (Dual p) a b
instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b where
@@ -17,5 +17,5 @@ instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b 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)
+ identity = MkDual identity
+ compose (MkDual f) (MkDual g) = MkDual (compose g f)
diff --git a/src/Lude/Algebra/Category/Object.hs b/src/Lude/Algebra/Category/Object.hs
@@ -30,7 +30,7 @@ instance HasTerminalObject Function where
instance HasTerminalObject Entailment where
type Terminal Entailment = Verum
- terminate = Entailment Evidence
+ terminate = MkEntailment MkEvidence
--------------------------------------------------------------------------------
@@ -49,4 +49,4 @@ instance HasInitialObject Function where
instance HasInitialObject Entailment where
type Initial Entailment = Falsum
- initiate = Entailment contradiction
+ initiate = MkEntailment contradiction
diff --git a/src/Lude/Constraint/Core.hs b/src/Lude/Constraint/Core.hs
@@ -30,13 +30,13 @@ instance (a `r` b, b ~ Canonical r a) => Canonically r a b
-- | Evidence of a constraint
type Evidence :: Constraint -> Type
-data Evidence a = (a) => Evidence
+data Evidence a = (a) => MkEvidence
-- | 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)
+newtype Entailment a b = MkEntailment ((a) => Evidence b)
-- | Infix alias for `Entailment`
type (:-) :: Cat Constraint
diff --git a/src/Lude/Constraint/Entailment.hs b/src/Lude/Constraint/Entailment.hs
@@ -10,8 +10,8 @@ import Lude.Constraint.Core
--------------------------------------------------------------------------------
pattern Duh :: forall a b. (a) => (b) => a :- b
-pattern Duh = Entailment Evidence
+pattern Duh = MkEntailment MkEvidence
{-# COMPLETE Duh #-}
entails :: forall a b. ((a) => b) => a :- b
-entails = Entailment Evidence
+entails = MkEntailment MkEvidence
diff --git a/src/Lude/Constraint/Evidence.hs b/src/Lude/Constraint/Evidence.hs
@@ -44,18 +44,18 @@ consider :: forall a b. (a :=> b) => Witness a b
consider = witness b
tautology :: forall a b. (b) => Witness a b
-tautology _ = Evidence
+tautology _ = MkEvidence
-- | Given that `a` (canonically) witnesses `c`, resolve a `c`-predicated
-- `b` with an `a`
because, (\\) :: forall b a c. (a :=> c) => ((c) => b) -> a -> b
-b `because` a = case consider a of Evidence -> b
+b `because` a = case consider a of MkEvidence -> b
(\\) = because
-- | Given that `a` (canonically) witnesses `b` and `b` implies `c`, we know
-- that `a` witnesses `c`
deduce :: forall c a b. (a :=> b, (b) => c) => Witness a c
-deduce = (Evidence \\)
+deduce = (MkEvidence \\)
--------------------------------------------------------------------------------
-- Instances
@@ -66,4 +66,4 @@ instance forall a. Evidence a `Witnesses` a where
type instance forall a b. Canonical Witnesses (a :- b) = b
instance forall a b. (a) => (a :- b) `Witnesses` b where
- witness _ (Entailment b) = b
+ witness _ (MkEntailment b) = b
diff --git a/src/Lude/Constraint/Predicate.hs b/src/Lude/Constraint/Predicate.hs
@@ -20,10 +20,10 @@ class Always x
instance forall x. Always x
instance {-# INCOHERENT #-} forall a x. a `Witnesses` Always x where
- witness _ _ = Evidence
+ witness _ _ = MkEvidence
always :: forall a x. a :- Always x
-always = Entailment Evidence
+always = MkEntailment MkEvidence
--------------------------------------------------------------------------------
@@ -31,4 +31,4 @@ type Never :: forall {i}. Predicate i
class (Falsum) => Never x
never :: forall x a. Never x :- a
-never = Entailment contradiction
+never = MkEntailment contradiction
diff --git a/src/Lude/Constraint/Verum.hs b/src/Lude/Constraint/Verum.hs
@@ -13,4 +13,4 @@ class Verum
instance Verum
instance {-# INCOHERENT #-} forall a. a `Witnesses` Verum where
- witness _ _ = Evidence
+ witness _ _ = MkEvidence
