lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Equivalence.hs (2692B)

      1 {-# LANGUAGE UndecidableInstances #-}
      2 
      3 module Lude.Equivalence (
      4     Equivalential (..),
      5     (==),
      6     (/=),
      7     (≠),
      8 ) where
      9 
     10 import Data.Coerce
     11 import Numeric.Natural qualified as Base
     12 import Prelude qualified as Base
     13 
     14 import Lude.Bool
     15 import Lude.Function
     16 import Lude.Haskell
     17 
     18 --------------------------------------------------------------------------------
     19 
     20 type Equivalential :: forall {r :: Repr}. Type# r -> Constraint
     21 class Equivalential (a :: Type# r) where
     22     {-# MINIMAL eq | ne #-}
     23 
     24     eq :: a -> a -> Bool
     25     default eq :: (Functional# r) => a -> a -> Bool
     26     eq = lam2# \x y -> not (app2# ne x y)
     27     {-# INLINE eq #-}
     28 
     29     ne :: a -> a -> Bool
     30     default ne :: (Functional# r) => a -> a -> Bool
     31     ne = lam2# \x y -> not (app2# eq x y)
     32     {-# INLINE ne #-}
     33 
     34 (==), (/=), (≠) :: forall {r :: Repr} (a :: Type# r). (Equivalential a) => a -> a -> Bool
     35 (==) = eq
     36 (/=) = ne
     37 (≠) = ne
     38 infix 4 ==, /=, ≠
     39 
     40 --------------------------------------------------------------------------------
     41 -- Generics
     42 
     43 instance Equivalential (GVoid p) where
     44     eq = elimGVoid
     45     ne = elimGVoid
     46 
     47 instance Equivalential (GUnit p) where
     48     eq MkGUnit MkGUnit = True
     49     ne MkGUnit MkGUnit = False
     50 
     51 instance (Equivalential a) => Equivalential (GConst i a p) where
     52     eq = eq `on` unGConst
     53     ne = ne `on` unGConst
     54 
     55 instance (Equivalential (f p)) => Equivalential (GMeta i t f p) where
     56     eq = eq `on` unGMeta
     57     ne = ne `on` unGMeta
     58 
     59 instance (Equivalential (f p), Equivalential (g p)) => Equivalential (GSum f g p) where
     60     eq (GLeft x0) (GLeft x1) = eq x0 x1
     61     eq (GRight y0) (GRight y1) = eq y0 y1
     62     eq (GLeft _) (GRight _) = False
     63     eq (GRight _) (GLeft _) = False
     64     ne (GLeft x0) (GLeft x1) = ne x0 x1
     65     ne (GRight y0) (GRight y1) = ne y0 y1
     66     ne (GLeft _) (GRight _) = True
     67     ne (GRight _) (GLeft _) = True
     68 
     69 instance (Equivalential (f p), Equivalential (g p)) => Equivalential (GProd f g p) where
     70     eq (GPair x0 y0) (GPair x1 y1) = eq x0 x1 && eq y0 y1
     71     ne (GPair x0 y0) (GPair x1 y1) = ne x0 x1 || ne y0 y1
     72 
     73 -- TODO: URec instances
     74 
     75 instance (Generically Equivalential a) => Equivalential (Genericity a) where
     76     eq = eq `on` grep
     77     ne = ne `on` grep
     78 
     79 --------------------------------------------------------------------------------
     80 -- Interop
     81 
     82 instance (Base.Eq a) => Equivalential (BaseInterop a) where
     83     eq = coerce (Base.==)
     84     ne = coerce (Base./=)
     85 
     86 deriving via BaseInterop Base.Ordering instance Equivalential Base.Ordering
     87 deriving via BaseInterop Base.Natural instance Equivalential Base.Natural
     88 deriving via BaseInterop Base.Integer instance Equivalential Base.Integer
     89 deriving via BaseInterop Base.Rational instance Equivalential Base.Rational