{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}

module Algebra.Category.Relation where

import Algebra.Classes
import Algebra.Types
import Algebra.Category
import Prelude (Bool(..), Eq(..),(&&),flip, ($))

newtype Rel s a b = Rel (a -> b -> s)

instance Additive s => Additive (Rel s a b) where
  Rel a -> b -> s
f + :: Rel s a b -> Rel s a b -> Rel s a b
+ Rel a -> b -> s
g = (a -> b -> s) -> Rel s a b
forall s a b. (a -> b -> s) -> Rel s a b
Rel (a -> b -> s
f (a -> b -> s) -> (a -> b -> s) -> a -> b -> s
forall a. Additive a => a -> a -> a
+ a -> b -> s
g)
  zero :: Rel s a b
zero = (a -> b -> s) -> Rel s a b
forall s a b. (a -> b -> s) -> Rel s a b
Rel a -> b -> s
forall a. Additive a => a
zero

indicate :: Ring s => Bool -> s
indicate :: forall s. Ring s => Bool -> s
indicate = \case
  Bool
True -> s
forall a. Multiplicative a => a
one
  Bool
False -> s
forall a. Additive a => a
zero

instance Ring s => Category (Rel s) where
  type Obj (Rel s) = Finite
  Rel b -> c -> s
p . :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s b c -> Rel s a b -> Rel s a c
. Rel a -> b -> s
q = (a -> c -> s) -> Rel s a c
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\a
i c
j -> [s] -> s
forall (t :: * -> *) a. (Foldable t, Additive a) => t a -> a
sum [b -> c -> s
p b
k c
j s -> s -> s
forall a. Multiplicative a => a -> a -> a
* a -> b -> s
q a
i b
k | b
k <- [b]
forall a. Finite a => [a]
inhabitants])
  id :: forall a. Obj (Rel s) a => Rel s a a
id = (a -> a -> s) -> Rel s a a
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\a
_ a
_ -> s
forall a. Multiplicative a => a
one)

instance Ring s => Autonomous (⊗) One Dual Dual (Rel s) where
  turn :: forall a. Obj (Rel s) a => Rel s One (Dual a ⊗ a)
turn = (One -> (Dual a ⊗ a) -> s) -> Rel s One (Dual a ⊗ a)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\One
_ (DualType a
i `Pair` a
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)) 
  turn' :: forall a. Obj (Rel s) a => Rel s (a ⊗ Dual a) One
turn' =  ((a ⊗ Dual a) -> One -> s) -> Rel s (a ⊗ Dual a) One
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\(a
i `Pair` DualType a
j) One
_ -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j))
instance Ring s => Compact (⊗) One Dual (Rel s)
instance Ring s => Symmetric (⊗) One (Rel s)
instance Ring s => Braided (⊗) One (Rel s) where
  swap :: forall a b. (Obj (Rel s) a, Obj (Rel s) b) => Rel s (a ⊗ b) (b ⊗ a)
swap = ((a ⊗ b) -> (b ⊗ a) -> s) -> Rel s (a ⊗ b) (b ⊗ a)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\(a
i `Pair` b
j) (b
k `Pair` a
l) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
l Bool -> Bool -> Bool
&& b
j b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
k))

instance Ring s => Dagger (Rel s) where
  dagger :: forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
dagger (Rel a -> b -> s
r) = (b -> a -> s) -> Rel s b a
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((a -> b -> s) -> b -> a -> s
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> s
r)

instance Ring s => Monoidal (⊗) One (Rel s) where
  unitorR :: forall a. (Obj (Rel s) a, Obj (Rel s) One) => Rel s a (a ⊗ One)
unitorR = (a -> (a ⊗ One) -> s) -> Rel s a (a ⊗ One)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\a
i (a
i' `Pair` One
_) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i'))
  unitorR_ :: forall a. (Obj (Rel s) a, Obj (Rel s) One) => Rel s (a ⊗ One) a
unitorR_ = Rel s a (a ⊗ One) -> Rel s (a ⊗ One) a
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s a (a ⊗ One)
forall a. (Obj (Rel s) a, Obj (Rel s) One) => Rel s a (a ⊗ One)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  Rel a -> b -> s
p ⊗ :: forall a b c d.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c, Obj (Rel s) d) =>
Rel s a b -> Rel s c d -> Rel s (a ⊗ c) (b ⊗ d)
⊗ Rel c -> d -> s
q = ((a ⊗ c) -> (b ⊗ d) -> s) -> Rel s (a ⊗ c) (b ⊗ d)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\(a
i `Pair` c
j) (b
k `Pair` d
l) -> a -> b -> s
p a
i b
k s -> s -> s
forall a. Multiplicative a => a -> a -> a
* c -> d -> s
q c
j d
l)
  assoc :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = (((a ⊗ b) ⊗ c) -> (a ⊗ (b ⊗ c)) -> s)
-> Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\((a
i `Pair` b
j) `Pair` c
k) (a
i' `Pair` (b
j' `Pair` c
k')) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i' Bool -> Bool -> Bool
&& b
j b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
j' Bool -> Bool -> Bool
&& c
k c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
k'))
  assoc_ :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc_ = Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
-> Rel s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc

instance Ring s => Cartesian (⊗) One (Rel s) where
  dis :: forall a. Obj (Rel s) a => Rel s a One
dis = (a -> One -> s) -> Rel s a One
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\a
_ One
_ -> s
forall a. Multiplicative a => a
one)
  dup :: forall a. Obj (Rel s) a => Rel s a (a ⊗ a)
dup = (a -> (a ⊗ a) -> s) -> Rel s a (a ⊗ a)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (\a
i (a
j `Pair` a
k) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j Bool -> Bool -> Bool
&& a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
k))

instance Ring s => CoCartesian (⊗) One (Rel s) where
  new :: forall a. Obj (Rel s) a => Rel s One a
new = Rel s a One -> Rel s One a
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s a One
forall a. Obj (Rel s) a => Rel s a One
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis
  jam :: forall a. Obj (Rel s) a => Rel s (a ⊗ a) a
jam = Rel s a (a ⊗ a) -> Rel s (a ⊗ a) a
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s a (a ⊗ a)
forall a. Obj (Rel s) a => Rel s a (a ⊗ a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a (x a a)
dup

instance Ring s => Monoidal (⊕) Zero (Rel s) where
  Rel a -> b -> s
p ⊗ :: forall a b c d.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c, Obj (Rel s) d) =>
Rel s a b -> Rel s c d -> Rel s (a ⊕ c) (b ⊕ d)
⊗ Rel c -> d -> s
q = ((a ⊕ c) -> (b ⊕ d) -> s) -> Rel s (a ⊕ c) (b ⊕ d)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (((a ⊕ c) -> (b ⊕ d) -> s) -> Rel s (a ⊕ c) (b ⊕ d))
-> ((a ⊕ c) -> (b ⊕ d) -> s) -> Rel s (a ⊕ c) (b ⊕ d)
forall a b. (a -> b) -> a -> b
$ \case
    (Inj1 a
i) -> \case
      (Inj1 b
j) -> a -> b -> s
p a
i b
j
      (Inj2 d
_) -> s
forall a. Additive a => a
zero
    (Inj2 c
i) -> \case
      (Inj1 b
_) -> s
forall a. Additive a => a
zero
      (Inj2 d
j) -> c -> d -> s
q c
i d
j
  unitorR :: forall a. (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s a (a ⊕ Zero)
unitorR = (a -> (a ⊕ Zero) -> s) -> Rel s a (a ⊕ Zero)
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((a -> (a ⊕ Zero) -> s) -> Rel s a (a ⊕ Zero))
-> (a -> (a ⊕ Zero) -> s) -> Rel s a (a ⊕ Zero)
forall a b. (a -> b) -> a -> b
$ \a
i -> \case
    Inj1 a
j -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)
    Inj2 Zero
j -> case Zero
j of
  assoc :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
assoc = (((a ⊕ b) ⊕ c) -> (a ⊕ (b ⊕ c)) -> s)
-> Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((((a ⊕ b) ⊕ c) -> (a ⊕ (b ⊕ c)) -> s)
 -> Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c)))
-> (((a ⊕ b) ⊕ c) -> (a ⊕ (b ⊕ c)) -> s)
-> Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall a b. (a -> b) -> a -> b
$ \case
    (Inj1 (Inj1 a
i)) -> \case
      Inj1 a
j -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)
      a ⊕ (b ⊕ c)
_ -> s
forall a. Additive a => a
zero
    (Inj1 (Inj2 b
i)) -> \case
      Inj2 (Inj1 b
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (b
i b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
j)
      a ⊕ (b ⊕ c)
_ -> s
forall a. Additive a => a
zero
    (Inj2 c
i) -> \case
      Inj2 (Inj2 c
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (c
i c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
j)
      a ⊕ (b ⊕ c)
_ -> s
forall a. Additive a => a
zero
  unitorR_ :: forall a. (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s (a ⊕ Zero) a
unitorR_ = Rel s a (a ⊕ Zero) -> Rel s (a ⊕ Zero) a
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s a (a ⊕ Zero)
forall a. (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s a (a ⊕ Zero)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  assoc_ :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c)
assoc_ = Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
-> Rel s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c)
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c))
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc

instance Ring s => Symmetric (⊕) Zero (Rel s)
instance Ring s => Braided (⊕) Zero (Rel s) where
  swap :: forall a b. (Obj (Rel s) a, Obj (Rel s) b) => Rel s (a ⊕ b) (b ⊕ a)
swap = ((a ⊕ b) -> (b ⊕ a) -> s) -> Rel s (a ⊕ b) (b ⊕ a)
forall s a b. (a -> b -> s) -> Rel s a b
Rel (((a ⊕ b) -> (b ⊕ a) -> s) -> Rel s (a ⊕ b) (b ⊕ a))
-> ((a ⊕ b) -> (b ⊕ a) -> s) -> Rel s (a ⊕ b) (b ⊕ a)
forall a b. (a -> b) -> a -> b
$ \case
    (Inj1 a
i) -> \case
      (Inj1 b
_) -> s
forall a. Additive a => a
zero
      (Inj2 a
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)
    (Inj2 b
i) -> \case
      (Inj2 a
_) -> s
forall a. Additive a => a
zero
      (Inj1 b
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (b
i b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
j)
    
instance Ring s => CoCartesian (⊕) Zero (Rel s) where
  Rel b -> a -> s
p ▿ :: forall a b c.
(Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) =>
Rel s b a -> Rel s c a -> Rel s (b ⊕ c) a
▿ Rel c -> a -> s
q = ((b ⊕ c) -> a -> s) -> Rel s (b ⊕ c) a
forall s a b. (a -> b -> s) -> Rel s a b
Rel (((b ⊕ c) -> a -> s) -> Rel s (b ⊕ c) a)
-> ((b ⊕ c) -> a -> s) -> Rel s (b ⊕ c) a
forall a b. (a -> b) -> a -> b
$ \case
    (Inj1 b
i) -> \a
j -> b -> a -> s
p b
i a
j
    (Inj2 c
i) -> \a
j -> c -> a -> s
q c
i a
j
  inl :: forall a b. O2 (Rel s) a b => Rel s a (a ⊕ b)
inl = (a -> (a ⊕ b) -> s) -> Rel s a (a ⊕ b)
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((a -> (a ⊕ b) -> s) -> Rel s a (a ⊕ b))
-> (a -> (a ⊕ b) -> s) -> Rel s a (a ⊕ b)
forall a b. (a -> b) -> a -> b
$ \a
i -> \case
    (Inj1 a
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)
    a ⊕ b
_ -> s
forall a. Additive a => a
zero
  inr :: forall a b. O2 (Rel s) a b => Rel s b (a ⊕ b)
inr = (b -> (a ⊕ b) -> s) -> Rel s b (a ⊕ b)
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((b -> (a ⊕ b) -> s) -> Rel s b (a ⊕ b))
-> (b -> (a ⊕ b) -> s) -> Rel s b (a ⊕ b)
forall a b. (a -> b) -> a -> b
$ \b
i -> \case
    (Inj2 b
j) -> Bool -> s
forall s. Ring s => Bool -> s
indicate (b
i b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
j)
    a ⊕ b
_ -> s
forall a. Additive a => a
zero
  new :: forall a. Obj (Rel s) a => Rel s Zero a
new = (Zero -> a -> s) -> Rel s Zero a
forall s a b. (a -> b -> s) -> Rel s a b
Rel ((Zero -> a -> s) -> Rel s Zero a)
-> (Zero -> a -> s) -> Rel s Zero a
forall a b. (a -> b) -> a -> b
$ Zero -> a -> s
\case
  jam :: forall a. Obj (Rel s) a => Rel s (a ⊕ a) a
jam = ((a ⊕ a) -> a -> s) -> Rel s (a ⊕ a) a
forall s a b. (a -> b -> s) -> Rel s a b
Rel (((a ⊕ a) -> a -> s) -> Rel s (a ⊕ a) a)
-> ((a ⊕ a) -> a -> s) -> Rel s (a ⊕ a) a
forall a b. (a -> b) -> a -> b
$ \case
    (Inj1 a
i) -> \a
j -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)
    (Inj2 a
i) -> \a
j -> Bool -> s
forall s. Ring s => Bool -> s
indicate (a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j)

instance Ring s => Cartesian (⊕) Zero (Rel s) where
  exl :: forall a b. O2 (Rel s) a b => Rel s (a ⊕ b) a
exl = Rel s a (a ⊕ b) -> Rel s (a ⊕ b) a
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s a (a ⊕ b)
forall a b. O2 (Rel s) a b => Rel s a (a ⊕ b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat a (x a b)
inl
  exr :: forall a b. O2 (Rel s) a b => Rel s (a ⊕ b) b
exr = Rel s b (a ⊕ b) -> Rel s (a ⊕ b) b
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s b (a ⊕ b)
forall a b. O2 (Rel s) a b => Rel s b (a ⊕ b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat b (x a b)
inr
  dup :: forall a. Obj (Rel s) a => Rel s a (a ⊕ a)
dup = Rel s (a ⊕ a) a -> Rel s a (a ⊕ a)
forall a b. O2 (Rel s) a b => Rel s a b -> Rel s b a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
(Dagger cat, O2 cat a b) =>
cat a b -> cat b a
dagger Rel s (a ⊕ a) a
forall a. Obj (Rel s) a => Rel s (a ⊕ a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat (x a a) a
jam