Eq

Eq.markdown

1

Comparing IO a for equality, cannot be captured by Bool.

class EQ a where
  type Logic a
  (=~=) :: a -> a -> Logic a 
  
instance EQ Int where
  type Logic Int = Bool

  (=~=) :: Int -> Int -> Bool
  (=~=) = (==)

instance EQ a => EQ (IO a) where
  type Logic (IO a) = IO (Logic a)

  (=~=) :: IO a -> IO a -> IO (Logic a)
  (=~=) = liftA2 (=~=)

instance EQ b => EQ (a -> b) where
  type Logic (a -> b) = a -> Logic b
 
  (=~=) :: (a -> b) -> (a -> b) -> (a -> Logic b)
  (f =~= g) a = f a =~= g a

>>> :t (randomRIO =~= randomRIO) 
(randomRIO =~= randomRIO)
  :: (EQ a, Random a) => (a, a) -> IO (Logic a)
>>> (randomRIO =~= randomRIO) (0, 2::Int)
True
>>> (randomRIO =~= randomRIO) (0, 2::Int)
False
>>> (randomRIO =~= randomRIO) (0, 2::Int)
False

2

instance EQ a => EQ (IORef a) where
  type Logic (IORef a) = IO (Logic a)

  (=~=) :: IORef a -> IORef a -> IO (Logic a)
  ref₁ =~= ref₂ = do
    val₁ <- readIORef ref₁
    val₂ <- readIORef ref₂
    pure (val₁ =~= val₂)

instance EQ a => EQ (TVar a) where
  type Logic (TVar a) = STM (Logic a)

  (=~=) :: TVar a -> TVar a -> STM (Logic a)
  ref₁ =~= ref₂ = do
    val₁ <- readTVar ref₁
    val₂ <- readTVar ref₂
    pure (val₁ =~= val₂)

3

data Ty = I | B

data E :: Ty -> Type where
  INT  :: Int  -> E I
  BOOL :: Bool -> E B
deriving instance Show (E a)

class EEQ a where
  type ELogic (a :: Ty) :: Ty
  type ELogic (a :: Ty) = B
  eq :: E a -> E a -> E (ELogic a)

instance EEQ I where
  type ELogic I = B
 
  eq :: E I -> E I -> E B
  INT a `eq` INT b = BOOL (a == b)

instance EEQ B where
  type ELogic B = B
 
  eq :: E B -> E B -> E B
  BOOL a `eq` BOOL b = BOOL (a == b)

instance EEQ a => EQ (E a) where
  type Logic (E a) = E (ELogic a)

  (=~=) :: E a -> E a -> E (ELogic a)
  (=~=) = eq

4

instance (EQ (f a), EQ (g a)) => EQ (Product f g a) where
  type Logic (Product f g a) = (Logic (f a), Logic (g a))
  
  (=~=) :: Product f g a -> Product f g a -> (Logic (f a), Logic (g a))
  Pair x y =~= Pair x' y' = 
    (x=~=x', y=~=y')

5

Comparing continuations!

instance EQ r => EQ (Cont r a) where
  type Logic (Cont r a) = (a -> r) -> Logic r

  (=~=) :: Cont r a -> Cont r a -> ((a -> r) -> Logic r)
  (C k1 =~= C k2) k = k1 k =~= k1 k

I don't know how to feel

newtype CodensityLogic :: (k -> Type) -> (Type -> Type) where
  CodLogic :: (forall xx. EQ (m xx) => (a -> m xx) -> Logic (m xx)) -> CodensityLogic m a
  
instance EQ (Codensity m a) where
  type Logic (Codensity m a) = CodensityLogic m a

  (=~=) :: Codensity m a -> Codensity m a -> CodensityLogic m a
  Cod a =~= Cod b = CodLogic (\k -> a k =~= b k)

6

instance EQ Void where
  type Logic Void = Void

  (=~=) :: Void -> Void -> Void
  void =~= _ = absurd void

instance EQ () where
  type Logic () = ()

  (=~=) :: () -> () -> ()
  () =~= () = ()

7

newtype CaseInsensitive = CI String

data CmpHow = CmpCaseInsensitive | CmpCaseSensitive

instance EQ CaseInsensitive where
  type Logic CaseInsensitive = CmpHow -> Bool

  (=~=) :: CaseInsensitive -> CaseInsensitive -> (CmpHow -> Bool)
  CI str1 =~= CI str2 = \case
    CmpCaseInsensitive -> map toLower str1 == map toLower str2
    CmpCaseSensitive   -> str1             == str2

8

instance EQ Dynamic where
  type Logic Dynamic = Maybe Bool

?