lude

commit e6f249e06ca946d1bd99c0e2b754e1906e267984
parent cdc3b2b3e893c8bb76c34d9153c6ed4944cda950
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 16 Sep 2026 13:14:55 -0700

Add Equivalence module

Diffstat:
M
src/Lude/Bool.hs
 | 
5
++++-
A
src/Lude/Equivalence.hs
 | 
90
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
M
src/Lude/Function.hs
 | 
5
+++--

3 files changed, 97 insertions(+), 3 deletions(-)
diff --git a/src/Lude/Bool.hs b/src/Lude/Bool.hs
@@ -1,8 +1,11 @@
 module Lude.Bool (
     Bool (..),
+    not,
+    (&&),
+    (||),
 ) where
 
-import Data.Bool (Bool (..))
+import Data.Bool (Bool (..), not, (&&), (||))
 
 -- TODO: Instances
 
diff --git a/src/Lude/Equivalence.hs b/src/Lude/Equivalence.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Equivalence (
+    Equivalential (..),
+    (==),
+    (<>),
+    InteropEq (..),
+) where
+
+import Data.Coerce
+import Prelude qualified as Base
+
+import Lude.Bool
+import Lude.Function
+import Lude.Haskell
+
+--------------------------------------------------------------------------------
+
+infix 4 ==, <>
+
+--------------------------------------------------------------------------------
+
+type Equivalential :: forall {r :: Repr}. Type @r -> Constraint
+class Equivalential (a :: Type @r) where
+    {-# MINIMAL eq | ne #-}
+
+    eq :: a -> a -> Bool
+    default eq :: (Functional# r) => a -> a -> Bool
+    eq = lam2# \x y -> not (app2# ne x y)
+    {-# INLINE eq #-}
+
+    ne :: a -> a -> Bool
+    default ne :: (Functional# r) => a -> a -> Bool
+    ne = lam2# \x y -> not (app2# eq x y)
+    {-# INLINE ne #-}
+
+(==), (<>) :: forall {r :: Repr} (a :: Type @r). (Equivalential a) => a -> a -> Bool
+(==) = eq
+(<>) = ne
+
+--------------------------------------------------------------------------------
+-- Generics
+
+instance Equivalential (GVoid p) where
+    eq = elimGVoid
+    ne = elimGVoid
+
+instance Equivalential (GUnit p) where
+    eq MkGUnit MkGUnit = True
+    ne MkGUnit MkGUnit = False
+
+instance (Equivalential a) => Equivalential (GConst i a p) where
+    eq = eq `on` unGConst
+    ne = ne `on` unGConst
+
+instance (Equivalential (f p)) => Equivalential (GMeta i t f p) where
+    eq = eq `on` unGMeta
+    ne = ne `on` unGMeta
+
+instance (Equivalential (f p), Equivalential (g p)) => Equivalential (GSum f g p) where
+    eq (GLeft x0) (GLeft x1) = eq x0 x1
+    eq (GRight y0) (GRight y1) = eq y0 y1
+    eq (GLeft _) (GRight _) = False
+    eq (GRight _) (GLeft _) = False
+    ne (GLeft x0) (GLeft x1) = ne x0 x1
+    ne (GRight y0) (GRight y1) = ne y0 y1
+    ne (GLeft _) (GRight _) = True
+    ne (GRight _) (GLeft _) = True
+
+instance (Equivalential (f p), Equivalential (g p)) => Equivalential (GProd f g p) where
+    eq (GPair x0 y0) (GPair x1 y1) = eq x0 x1 && eq y0 y1
+    ne (GPair x0 y0) (GPair x1 y1) = ne x0 x1 || ne y0 y1
+
+-- TODO: URec instances
+
+instance (Generically Equivalential a) => Equivalential (Genericity a) where
+    eq = eq `on` grep
+    ne = ne `on` grep
+
+--------------------------------------------------------------------------------
+-- Interop
+
+type InteropEq :: Endo Type
+newtype InteropEq a = MkInteropEq {unInteropEq :: a}
+
+instance (Base.Eq a) => Equivalential (InteropEq a) where
+    eq = coerce (Base.==)
+    ne = coerce (Base./=)
+
+deriving via InteropEq Base.Ordering instance Equivalential Base.Ordering
diff --git a/src/Lude/Function.hs b/src/Lude/Function.hs
@@ -1,11 +1,12 @@
 module Lude.Function (
-    flip,
     const,
+    flip,
+    on,
     ($),
     (&),
 ) where
 
-import Data.Function
+import Data.Function (const, flip, on, ($), (&))
 
 -- TODO: Generalize some of this? E.g., for CCCs?