commit 3c311c8c62b2c5234d57ff5fc7023be6d4838173
parent b0e23b53beb3c1aa813beef938bdd30842dcf866
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 4 Sep 2026 21:10:23 -0700
Improve Canonically
Diffstat:
6 files changed, 17 insertions(+), 9 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -130,9 +130,9 @@ data Nt p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Nt {comp :: forall
-- 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
-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
diff --git a/src/Lude/Algebra/Category/Dual.hs b/src/Lude/Algebra/Category/Dual.hs
@@ -11,9 +11,9 @@ import Lude.Constraint.Evidence
type Dual :: forall i. Cat i -> Cat i
newtype Dual p a b = Dual {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
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
diff --git a/src/Lude/Constraint/Core.hs b/src/Lude/Constraint/Core.hs
@@ -1,6 +1,7 @@
{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Constraint.Core (
+ Canonical,
Canonically,
Evidence (..),
Entailment (..),
@@ -15,10 +16,17 @@ infixr 1 :-
--------------------------------------------------------------------------------
+type Canonical :: forall {k} {l}. Relation k l -> k -> l
+type family Canonical r a
+
-- | 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
+class (a `r` b, b ~ Canonical r a) => Canonically r a b
+
+instance (a `r` b, b ~ Canonical r a) => Canonically r a b
+
+--------------------------------------------------------------------------------
-- | Evidence of a constraint
type Evidence :: Constraint -> Type
diff --git a/src/Lude/Constraint/Evidence.hs b/src/Lude/Constraint/Evidence.hs
@@ -60,10 +60,10 @@ deduce = (Evidence \\)
--------------------------------------------------------------------------------
-- Instances
-instance forall a. Witnesses (Evidence a) a where
+type instance forall a. Canonical Witnesses (Evidence a) = a
+instance forall a. Evidence a `Witnesses` a where
witness _ e = e
-instance forall a. Canonically Witnesses (Evidence a) a
-instance forall a b. (a) => Witnesses (a :- b) b 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
-instance forall a b. (a) => Canonically Witnesses (a :- b) b
diff --git a/src/Lude/Constraint/Predicate.hs b/src/Lude/Constraint/Predicate.hs
@@ -19,7 +19,7 @@ type Always :: forall {i}. Predicate i
class Always x
instance forall x. Always x
-instance forall a x. Witnesses a (Always x) where
+instance {-# INCOHERENT #-} forall a x. a `Witnesses` Always x where
witness _ _ = Evidence
always :: forall a x. a :- Always x
diff --git a/src/Lude/Constraint/Verum.hs b/src/Lude/Constraint/Verum.hs
@@ -12,5 +12,5 @@ type Verum :: Constraint
class Verum
instance Verum
-instance forall a. Witnesses a Verum where
+instance {-# INCOHERENT #-} forall a. a `Witnesses` Verum where
witness _ _ = Evidence
