lude

commit f685675d274d40dcb120afb707a44bd201e74de9
parent 21ff37a2cec6b24b5d54caeb010fc04ed36e1a04
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu,  3 Sep 2026 11:28:06 -0700

Clean up

Diffstat:
M
src/Lude/Constraint.hs
 | 
36
++++++++++++++++++++++++++++++------
M
src/Lude/Kind.hs
 | 
5
+++++

2 files changed, 35 insertions(+), 6 deletions(-)
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -24,12 +24,25 @@ module Lude.Constraint (
     --
     Never1 (..),
     never1,
+    --
+    Both,
+    (:&),
 ) where
 
+import Prelude.Experimental qualified as GHC
+
 import Lude.Kind
 
 --------------------------------------------------------------------------------
 
+infixl 4 \\
+infixl 7 :&
+infixr 9 :=>, :-
+
+--------------------------------------------------------------------------------
+-- Evidence
+
+-- | Evidence of a constraint
 type Evidence :: Constraint -> Type
 data Evidence a = (a) => Evidence
 
@@ -38,29 +51,33 @@ type Evidence1 :: forall {i}. Constraint1 i -> Type1 i
 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 (:=>) = Witnesses
-infixr 9 :=>
+-- | Infix alias for `Witnesses`
+type (:=>) = Witnesses -- NOTE: Add signature once GHC#16754 is resolved
 
+-- | Given that `a` 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
 (\\) = because
-infixl 4 \\
 
 instance forall a. Witnesses (Evidence a) a where
     witness e = e
 
 --------------------------------------------------------------------------------
+-- Entailment
 
+-- | Evidence that one constraint entails another
 type Entailment :: Constraint -> Constraint -> Type
 newtype Entailment a b = Entailment ((a) => Evidence b)
 
-type (:-) = Entailment
-infixr 9 :-
+-- | 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
@@ -98,7 +115,14 @@ never = Entailment contradiction
 --------------------------------------------------------------------------------
 
 type Never1 :: forall {i}. Constraint1 i
-class Never1 x where contradiction1 :: b
+class Never1 x where contradiction1 :: a
 
 never1 :: forall x a. Never1 x :- a
 never1 @x = Entailment (contradiction1 @x)
+
+--------------------------------------------------------------------------------
+
+type Both :: Constraint -> Constraint -> Constraint
+type Both = GHC.CTuple2
+
+type (:&) = Both -- NOTE: Add signature once GHC#16754 is resolved
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -44,6 +44,7 @@ type TypeU = Type @Repr.BoxU
 type Type1 :: forall (r :: Repr). Kind -> Kind
 type Type1 @r i = i -> Type @r
 
+-- TODO: What's this for? I forget.
 type AnyType :: Kind
 data AnyType = forall (r :: Repr). MkAnyType (Type @r)
 
@@ -78,6 +79,10 @@ type BiEndo :: Kind -> Kind
 type BiEndo k = k -> k -> k
 
 --------------------------------------------------------------------------------
+-- Defunctionalization
+
+-- TODO: All this is tentative. It's mostly for functors which aren't determined
+-- by their object map.
 
 -- | An empty kind with a phantom kind index, used to make @T k@ opaque
 type T' :: Kind -> Kind