lude

commit 8888a4c875636eb311f7f8693f41814e206a978c
parent 93a5e6c5f53b3ea8f11a226c43ffc34701946fc1
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri,  4 Sep 2026 22:26:38 -0700

Make Evidence into a functor

Diffstat:
M
src/Lude/Algebra/Category/Core.hs
 | 
23
++++++++++++++++++-----
M
src/Lude/Constraint/Core.hs
 | 
2
+-

2 files changed, 19 insertions(+), 6 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -85,11 +85,14 @@ type DefaultFunctorial :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constrai
 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?
+-- TODO: Should these be incoherent?
+instance DefaultFunctorial p Function f where
+    defaultPreserveObj = always
+instance DefaultFunctorial p Entailment f where
+    defaultPreserveObj = always
+
 -- 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
@@ -162,9 +165,19 @@ type f ~> g = forall x. f x -> g x
 -- We implement this here to avoid orphans.
 
 instance Categorical Entailment where
-    identity = entails
-    compose (MkEntailment f) (MkEntailment g) = MkEntailment (f \\ g)
+    identity = MkEntailment MkEvidence
+    compose f g = MkEntailment (MkEvidence \\ f \\ g)
 
 -- | Natural transformations to `Entailment`/`:-`
 type (:~) :: forall k. Cat (k -> Constraint)
 type f :~ g = forall x. f x :- g x
+
+--------------------------------------------------------------------------------
+
+instance Functorial Evidence where
+    type Dom Evidence = Entailment
+    type Cod Evidence = Function
+    map (MkEntailment f) = because f
+
+-- Dual functor Type -> Constraint? What's it do? Provide an element of the type?
+-- Yes: See Ed Kmett's reflection package / the paper it's based on.
diff --git a/src/Lude/Constraint/Core.hs b/src/Lude/Constraint/Core.hs
@@ -36,7 +36,7 @@ data Evidence a = (a) => MkEvidence
 --
 -- `Entailment` (`:-`) is to `Constraint` what `Function` (`->`) is to `Type`.
 type Entailment :: Cat Constraint
-newtype Entailment a b = MkEntailment ((a) => Evidence b)
+newtype Entailment a b = MkEntailment {unEntailment :: (a) => Evidence b}
 
 -- | Infix alias for `Entailment`
 type (:-) :: Cat Constraint