{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DataKinds #-}
module LAoP.Relation.Internal
(
Relation (..),
Boolean,
Countable,
CountableDimensions,
CountableN,
CountableDimensionsN,
FromListsN,
Liftable,
Trivial,
TrivialP,
empty,
one,
join,
(|||),
fork,
(===),
I.FromNat,
I.Count,
I.Normalize,
I.FromLists,
fromLists,
fromF',
fromF,
toRel,
toLists,
toList,
toBool,
pt,
belongs,
relationBuilder',
relationBuilder,
zeros,
ones,
bang,
point,
conv,
intersection,
union,
sse,
implies,
iff,
ker,
img,
injective,
entire,
simple,
surjective,
representation,
function,
abstraction,
injection,
surjection,
bijection,
domain,
range,
divisionF,
divR,
divL,
divS,
shrunkBy,
overriddenBy,
splitR,
fstR,
sndR,
(><),
eitherR,
i1,
i2,
(-|-),
trans,
untrans,
reflexive,
coreflexive,
transitive,
symmetric,
antiSymmetric,
irreflexive,
connected,
preorder,
partialOrder,
linearOrder,
equivalence,
partialEquivalence,
difunctional,
equalizer,
predR,
guard,
cond,
iden,
comp,
fromF',
fromF,
pointAp,
pointApBool,
pretty,
prettyPrint
)
where
import Data.Void
import qualified LAoP.Matrix.Internal as I
import LAoP.Utils.Internal
import Control.DeepSeq
import Data.Bool
import GHC.TypeLits
import Prelude hiding (id, (.))
type Boolean = Natural 0 1
type Powerset a = List (List a)
newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
deriving (Int -> Relation a b -> ShowS
[Relation a b] -> ShowS
Relation a b -> String
(Int -> Relation a b -> ShowS)
-> (Relation a b -> String)
-> ([Relation a b] -> ShowS)
-> Show (Relation a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. Int -> Relation a b -> ShowS
forall a b. [Relation a b] -> ShowS
forall a b. Relation a b -> String
showList :: [Relation a b] -> ShowS
$cshowList :: forall a b. [Relation a b] -> ShowS
show :: Relation a b -> String
$cshow :: forall a b. Relation a b -> String
showsPrec :: Int -> Relation a b -> ShowS
$cshowsPrec :: forall a b. Int -> Relation a b -> ShowS
Show, Relation a b -> Relation a b -> Bool
(Relation a b -> Relation a b -> Bool)
-> (Relation a b -> Relation a b -> Bool) -> Eq (Relation a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. Relation a b -> Relation a b -> Bool
/= :: Relation a b -> Relation a b -> Bool
$c/= :: forall a b. Relation a b -> Relation a b -> Bool
== :: Relation a b -> Relation a b -> Bool
$c== :: forall a b. Relation a b -> Relation a b -> Bool
Eq, Eq (Relation a b)
Eq (Relation a b) =>
(Relation a b -> Relation a b -> Ordering)
-> (Relation a b -> Relation a b -> Bool)
-> (Relation a b -> Relation a b -> Bool)
-> (Relation a b -> Relation a b -> Bool)
-> (Relation a b -> Relation a b -> Bool)
-> (Relation a b -> Relation a b -> Relation a b)
-> (Relation a b -> Relation a b -> Relation a b)
-> Ord (Relation a b)
Relation a b -> Relation a b -> Bool
Relation a b -> Relation a b -> Ordering
Relation a b -> Relation a b -> Relation a b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. Eq (Relation a b)
forall a b. Relation a b -> Relation a b -> Bool
forall a b. Relation a b -> Relation a b -> Ordering
forall a b. Relation a b -> Relation a b -> Relation a b
min :: Relation a b -> Relation a b -> Relation a b
$cmin :: forall a b. Relation a b -> Relation a b -> Relation a b
max :: Relation a b -> Relation a b -> Relation a b
$cmax :: forall a b. Relation a b -> Relation a b -> Relation a b
>= :: Relation a b -> Relation a b -> Bool
$c>= :: forall a b. Relation a b -> Relation a b -> Bool
> :: Relation a b -> Relation a b -> Bool
$c> :: forall a b. Relation a b -> Relation a b -> Bool
<= :: Relation a b -> Relation a b -> Bool
$c<= :: forall a b. Relation a b -> Relation a b -> Bool
< :: Relation a b -> Relation a b -> Bool
$c< :: forall a b. Relation a b -> Relation a b -> Bool
compare :: Relation a b -> Relation a b -> Ordering
$ccompare :: forall a b. Relation a b -> Relation a b -> Ordering
$cp1Ord :: forall a b. Eq (Relation a b)
Ord, Relation a b -> ()
(Relation a b -> ()) -> NFData (Relation a b)
forall a. (a -> ()) -> NFData a
forall a b. Relation a b -> ()
rnf :: Relation a b -> ()
$crnf :: forall a b. Relation a b -> ()
NFData) via (I.Matrix (Natural 1 1) (I.Normalize a) (I.Normalize b))
deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
type Countable a = KnownNat (I.Count a)
type CountableDimensions a b = (Countable a, Countable b)
type CountableN a = KnownNat (I.Count (I.Normalize a))
type CountableDimensionsN a b = (CountableN a, CountableN b)
type FromListsN a b = I.FromLists Boolean (I.Normalize a) (I.Normalize b)
type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)
type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
instance Category Relation where
type Object Relation a = (FromListsN a a, CountableN a)
id :: Relation a a
id = Relation a a
forall a. (FromListsN a a, CountableN a) => Relation a a
iden
. :: Relation b c -> Relation a b -> Relation a c
(.) = Relation b c -> Relation a b -> Relation a c
forall b c a. Relation b c -> Relation a b -> Relation a c
comp
instance Num (Relation a b) where
(R a :: Matrix Boolean (Normalize a) (Normalize b)
a) + :: Relation a b -> Relation a b -> Relation a b
+ (R b :: Matrix Boolean (Normalize a) (Normalize b)
b) = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
I.orM Matrix Boolean (Normalize a) (Normalize b)
a Matrix Boolean (Normalize a) (Normalize b)
b)
(R a :: Matrix Boolean (Normalize a) (Normalize b)
a) - :: Relation a b -> Relation a b -> Relation a b
- (R b :: Matrix Boolean (Normalize a) (Normalize b)
b) = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
I.subM Matrix Boolean (Normalize a) (Normalize b)
a Matrix Boolean (Normalize a) (Normalize b)
b)
(R a :: Matrix Boolean (Normalize a) (Normalize b)
a) * :: Relation a b -> Relation a b -> Relation a b
* (R b :: Matrix Boolean (Normalize a) (Normalize b)
b) = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
I.andM Matrix Boolean (Normalize a) (Normalize b)
a Matrix Boolean (Normalize a) (Normalize b)
b)
negate :: Relation a b -> Relation a b
negate (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
forall cols rows. Relation cols rows -> Relation cols rows
I.negateM Matrix Boolean (Normalize a) (Normalize b)
a)
type Zero = Void
type One = ()
empty :: Relation Zero Zero
empty :: Relation Zero Zero
empty = Matrix Boolean (Normalize Zero) (Normalize Zero)
-> Relation Zero Zero
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R Matrix Boolean (Normalize Zero) (Normalize Zero)
forall e. Matrix e Zero Zero
I.Empty
one :: Boolean -> Relation One One
one :: Boolean -> Relation () ()
one = Matrix Boolean () () -> Relation () ()
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean () () -> Relation () ())
-> (Boolean -> Matrix Boolean () ()) -> Boolean -> Relation () ()
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Boolean -> Matrix Boolean () ()
forall e. e -> Matrix e () ()
I.One
join :: Relation a c -> Relation b c -> Relation (Either a b) c
join :: Relation a c -> Relation b c -> Relation (Either a b) c
join (R a :: Matrix Boolean (Normalize a) (Normalize c)
a) (R b :: Matrix Boolean (Normalize b) (Normalize c)
b) = Matrix Boolean (Normalize (Either a b)) (Normalize c)
-> Relation (Either a b) c
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize c)
-> Matrix Boolean (Normalize b) (Normalize c)
-> Matrix
Boolean (Either (Normalize a) (Normalize b)) (Normalize c)
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
I.Join Matrix Boolean (Normalize a) (Normalize c)
a Matrix Boolean (Normalize b) (Normalize c)
b)
infixl 3 |||
(|||) ::
Relation a c ->
Relation b c ->
Relation (Either a b) c
||| :: Relation a c -> Relation b c -> Relation (Either a b) c
(|||) = Relation a c -> Relation b c -> Relation (Either a b) c
forall a c b.
Relation a c -> Relation b c -> Relation (Either a b) c
join
fork :: Relation c a -> Relation c b -> Relation c (Either a b)
fork :: Relation c a -> Relation c b -> Relation c (Either a b)
fork (R a :: Matrix Boolean (Normalize c) (Normalize a)
a) (R b :: Matrix Boolean (Normalize c) (Normalize b)
b) = Matrix Boolean (Normalize c) (Normalize (Either a b))
-> Relation c (Either a b)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize c) (Normalize a)
-> Matrix Boolean (Normalize c) (Normalize b)
-> Matrix
Boolean (Normalize c) (Either (Normalize a) (Normalize b))
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
I.Fork Matrix Boolean (Normalize c) (Normalize a)
a Matrix Boolean (Normalize c) (Normalize b)
b)
infixl 2 ===
(===) ::
Relation c a ->
Relation c b ->
Relation c (Either a b)
=== :: Relation c a -> Relation c b -> Relation c (Either a b)
(===) = Relation c a -> Relation c b -> Relation c (Either a b)
forall c a b.
Relation c a -> Relation c b -> Relation c (Either a b)
fork
fromLists :: (FromListsN a b) => [[Boolean]] -> Relation a b
fromLists :: [[Boolean]] -> Relation a b
fromLists = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b) -> Relation a b)
-> ([[Boolean]] -> Matrix Boolean (Normalize a) (Normalize b))
-> [[Boolean]]
-> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. [[Boolean]] -> Matrix Boolean (Normalize a) (Normalize b)
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
I.fromLists
relationBuilder' ::
(FromListsN a b, CountableDimensionsN a b) =>
((Int, Int) -> Boolean) -> Relation a b
relationBuilder' :: ((Int, Int) -> Boolean) -> Relation a b
relationBuilder' = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b) -> Relation a b)
-> (((Int, Int) -> Boolean)
-> Matrix Boolean (Normalize a) (Normalize b))
-> ((Int, Int) -> Boolean)
-> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. ((Int, Int) -> Boolean)
-> Matrix Boolean (Normalize a) (Normalize b)
forall e cols rows.
(FromLists e cols rows, CountableDimensions cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
I.matrixBuilder'
relationBuilder ::
( FromListsN a b,
Enum a,
Enum b,
Bounded a,
Bounded b,
Eq a,
CountableDimensionsN a b
) => ((a, b) -> Boolean) -> Relation a b
relationBuilder :: ((a, b) -> Boolean) -> Relation a b
relationBuilder = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b) -> Relation a b)
-> (((a, b) -> Boolean)
-> Matrix Boolean (Normalize a) (Normalize b))
-> ((a, b) -> Boolean)
-> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> Boolean) -> Matrix Boolean (Normalize a) (Normalize b)
forall e a b.
(FromListsN e a b, CountableN b, Enum a, Enum b, Bounded a,
Bounded b, Eq a, CountableDimensionsN a b) =>
((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
I.matrixBuilder
fromF' ::
( Liftable a b,
CountableDimensionsN c d,
FromListsN d c
)
=> (a -> b) -> Relation c d
fromF' :: (a -> b) -> Relation c d
fromF' f :: a -> b
f = Matrix Boolean (Normalize c) (Normalize d) -> Relation c d
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R ((a -> b) -> Matrix Boolean (Normalize c) (Normalize d)
forall a b cols rows.
(Liftable Boolean a b, CountableDimensions cols rows,
FromLists Boolean rows cols) =>
(a -> b) -> Relation cols rows
I.fromFRel' a -> b
f)
fromF ::
( Liftable a b,
CountableDimensionsN a b,
FromListsN b a
)
=> (a -> b) -> Relation a b
fromF :: (a -> b) -> Relation a b
fromF f :: a -> b
f = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R ((a -> b) -> Matrix Boolean (Normalize a) (Normalize b)
forall a b.
(Liftable Boolean a b, CountableDimensionsN a b,
FromLists Boolean (Normalize b) (Normalize a)) =>
(a -> b) -> Relation (Normalize a) (Normalize b)
I.fromFRel a -> b
f)
toRel ::
( Liftable a b,
CountableDimensionsN a b,
FromListsN b a
)
=> (a -> b -> Bool) -> Relation a b
toRel :: (a -> b -> Bool) -> Relation a b
toRel = Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b) -> Relation a b)
-> ((a -> b -> Bool) -> Matrix Boolean (Normalize a) (Normalize b))
-> (a -> b -> Bool)
-> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. (a -> b -> Bool) -> Matrix Boolean (Normalize a) (Normalize b)
forall a b.
(Bounded a, Bounded b, Enum a, Enum b, Eq b,
CountableDimensionsN a b, FromListsN Boolean b a) =>
(a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
I.toRel
fromRel ::
( Liftable a b,
Eq a,
CountableDimensionsN a b,
FromListsN a One,
FromListsN b One
)
=> Relation a b -> (a -> b -> Bool)
fromRel :: Relation a b -> a -> b -> Bool
fromRel r :: Relation a b
r a :: a
a b :: b
b = a -> b -> Relation a b -> Bool
forall a b.
(Liftable a b, Eq a, CountableDimensionsN a b, FromListsN a (),
FromListsN b ()) =>
a -> b -> Relation a b -> Bool
pointApBool a
a b
b Relation a b
r
toLists :: Relation a b -> [[Boolean]]
toLists :: Relation a b -> [[Boolean]]
toLists (R m :: Matrix Boolean (Normalize a) (Normalize b)
m) = Matrix Boolean (Normalize a) (Normalize b) -> [[Boolean]]
forall e cols rows. Matrix e cols rows -> [[e]]
I.toLists Matrix Boolean (Normalize a) (Normalize b)
m
toList :: Relation a b -> [Boolean]
toList :: Relation a b -> [Boolean]
toList (R m :: Matrix Boolean (Normalize a) (Normalize b)
m) = Matrix Boolean (Normalize a) (Normalize b) -> [Boolean]
forall e cols rows. Matrix e cols rows -> [e]
I.toList Matrix Boolean (Normalize a) (Normalize b)
m
toBool :: Relation One One -> Bool
toBool :: Relation () () -> Bool
toBool r :: Relation () ()
r = case Relation () () -> [Boolean]
forall a b. Relation a b -> [Boolean]
toList Relation () ()
r of
[Nat 0] -> Bool
False
_ -> Bool
True
pt ::
( Liftable a b,
Eq a,
CountableDimensionsN a b,
FromListsN a One,
FromListsN b One
)
=> Relation a b -> (a -> List b)
pt :: Relation a b -> a -> List b
pt r :: Relation a b
r a :: a
a =
let (L lb :: [b]
lb) = List b
forall a. Bounded a => a
maxBound
in [b] -> List b
forall a. [a] -> List a
L [ b
b | b
b <- [b]
lb, Relation () () -> Bool
toBool (a -> b -> Relation a b -> Relation () ()
forall a b.
(Liftable a b, Eq a, CountableDimensionsN a b, FromListsN a (),
FromListsN b ()) =>
a -> b -> Relation a b -> Relation () ()
pointAp a
a b
b Relation a b
r) ]
belongs ::
( Bounded a,
Enum a,
Eq a,
CountableDimensionsN (List a) a,
FromListsN a (List a)
)
=> Relation (List a) a
belongs :: Relation (List a) a
belongs = (List a -> a -> Bool) -> Relation (List a) a
forall a b.
(Liftable a b, CountableDimensionsN a b, FromListsN b a) =>
(a -> b -> Bool) -> Relation a b
toRel List a -> a -> Bool
forall a. Eq a => List a -> a -> Bool
elemR
where
elemR :: List a -> a -> Bool
elemR (L l :: [a]
l) x :: a
x = a
x a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
l
zeros ::
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
zeros :: Relation a b
zeros = ((Int, Int) -> Boolean) -> Relation a b
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
((Int, Int) -> Boolean) -> Relation a b
relationBuilder' (Boolean -> (Int, Int) -> Boolean
forall a b. a -> b -> a
const (Int -> Boolean
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat 0))
ones ::
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
ones :: Relation a b
ones = ((Int, Int) -> Boolean) -> Relation a b
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
((Int, Int) -> Boolean) -> Relation a b
relationBuilder' (Boolean -> (Int, Int) -> Boolean
forall a b. a -> b -> a
const (Int -> Boolean
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat 1))
bang ::
(FromListsN a One, CountableN a) =>
Relation a One
bang :: Relation a ()
bang = Relation a ()
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
ones
point ::
( Bounded a,
Enum a,
Eq a,
CountableN a,
FromListsN a One
) => a -> Relation One a
point :: a -> Relation () a
point = (() -> a) -> Relation () a
forall a b.
(Liftable a b, CountableDimensionsN a b, FromListsN b a) =>
(a -> b) -> Relation a b
fromF ((() -> a) -> Relation () a)
-> (a -> () -> a) -> a -> Relation () a
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. a -> () -> a
forall a b. a -> b -> a
const
iden ::
(FromListsN a a, CountableN a) => Relation a a
iden :: Relation a a
iden = ((Int, Int) -> Boolean) -> Relation a a
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
((Int, Int) -> Boolean) -> Relation a b
relationBuilder' (Boolean -> Boolean -> Bool -> Boolean
forall a. a -> a -> Bool -> a
bool (Int -> Boolean
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat 0) (Int -> Boolean
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat 1) (Bool -> Boolean) -> ((Int, Int) -> Bool) -> (Int, Int) -> Boolean
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==))
comp :: Relation b c -> Relation a b -> Relation a c
comp :: Relation b c -> Relation a b -> Relation a c
comp (R a :: Matrix Boolean (Normalize b) (Normalize c)
a) (R b :: Matrix Boolean (Normalize a) (Normalize b)
b) = Matrix Boolean (Normalize a) (Normalize c) -> Relation a c
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize b) (Normalize c)
-> Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize c)
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
I.compRel Matrix Boolean (Normalize b) (Normalize c)
a Matrix Boolean (Normalize a) (Normalize b)
b)
divR :: Relation b c -> Relation b a -> Relation a c
divR :: Relation b c -> Relation b a -> Relation a c
divR (R x :: Matrix Boolean (Normalize b) (Normalize c)
x) (R y :: Matrix Boolean (Normalize b) (Normalize a)
y) = Matrix Boolean (Normalize a) (Normalize c) -> Relation a c
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize b) (Normalize c)
-> Matrix Boolean (Normalize b) (Normalize a)
-> Matrix Boolean (Normalize a) (Normalize c)
forall b c a. Relation b c -> Relation b a -> Relation a c
I.divR Matrix Boolean (Normalize b) (Normalize c)
x Matrix Boolean (Normalize b) (Normalize a)
y)
divL :: Relation c b -> Relation a b -> Relation a c
divL :: Relation c b -> Relation a b -> Relation a c
divL (R x :: Matrix Boolean (Normalize c) (Normalize b)
x) (R y :: Matrix Boolean (Normalize a) (Normalize b)
y) = Matrix Boolean (Normalize a) (Normalize c) -> Relation a c
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize c) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize a) (Normalize c)
forall c b a. Relation c b -> Relation a b -> Relation a c
I.divL Matrix Boolean (Normalize c) (Normalize b)
x Matrix Boolean (Normalize a) (Normalize b)
y)
divS :: Relation c a -> Relation b a -> Relation c b
divS :: Relation c a -> Relation b a -> Relation c b
divS (R x :: Matrix Boolean (Normalize c) (Normalize a)
x) (R y :: Matrix Boolean (Normalize b) (Normalize a)
y) = Matrix Boolean (Normalize c) (Normalize b) -> Relation c b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize c) (Normalize a)
-> Matrix Boolean (Normalize b) (Normalize a)
-> Matrix Boolean (Normalize c) (Normalize b)
forall c a b. Relation c a -> Relation b a -> Relation c b
I.divS Matrix Boolean (Normalize c) (Normalize a)
x Matrix Boolean (Normalize b) (Normalize a)
y)
shrunkBy :: Relation b a -> Relation a a -> Relation b a
shrunkBy :: Relation b a -> Relation a a -> Relation b a
shrunkBy r :: Relation b a
r s :: Relation a a
s = Relation b a
r Relation b a -> Relation b a -> Relation b a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a a -> Relation a b -> Relation b a
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Relation a a
s (Relation b a -> Relation a b
forall a b. Relation a b -> Relation b a
conv Relation b a
r)
overriddenBy ::
( FromListsN b b,
CountableN b
) => Relation a b -> Relation a b -> Relation a b
overriddenBy :: Relation a b -> Relation a b -> Relation a b
overriddenBy r :: Relation a b
r s :: Relation a b
s = Relation a b
s Relation a b -> Relation a b -> Relation a b
forall a b. Relation a b -> Relation a b -> Relation a b
`union` Relation a b
r Relation a b -> Relation a b -> Relation a b
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation b b -> Relation b a -> Relation a b
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Relation b b
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
zeros (Relation a b -> Relation b a
forall a b. Relation a b -> Relation b a
conv Relation a b
s)
pointAp ::
( Liftable a b,
Eq a,
CountableDimensionsN a b,
FromListsN a One,
FromListsN b One
) => a -> b -> Relation a b -> Relation One One
pointAp :: a -> b -> Relation a b -> Relation () ()
pointAp a :: a
a b :: b
b r :: Relation a b
r = Relation () b -> Relation b ()
forall a b. Relation a b -> Relation b a
conv (b -> Relation () b
forall a.
(Bounded a, Enum a, Eq a, CountableN a, FromListsN a ()) =>
a -> Relation () a
point b
b) Relation b () -> Relation a b -> Relation a ()
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b
r Relation a () -> Relation () a -> Relation () ()
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. a -> Relation () a
forall a.
(Bounded a, Enum a, Eq a, CountableN a, FromListsN a ()) =>
a -> Relation () a
point a
a
pointApBool ::
( Liftable a b,
Eq a,
CountableDimensionsN a b,
FromListsN a One,
FromListsN b One
) => a -> b -> Relation a b -> Bool
pointApBool :: a -> b -> Relation a b -> Bool
pointApBool a :: a
a b :: b
b r :: Relation a b
r = Relation () () -> Bool
toBool (Relation () () -> Bool) -> Relation () () -> Bool
forall a b. (a -> b) -> a -> b
$ Relation () b -> Relation b ()
forall a b. Relation a b -> Relation b a
conv (b -> Relation () b
forall a.
(Bounded a, Enum a, Eq a, CountableN a, FromListsN a ()) =>
a -> Relation () a
point b
b) Relation b () -> Relation a b -> Relation a ()
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b
r Relation a () -> Relation () a -> Relation () ()
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. a -> Relation () a
forall a.
(Bounded a, Enum a, Eq a, CountableN a, FromListsN a ()) =>
a -> Relation () a
point a
a
conv :: Relation a b -> Relation b a
conv :: Relation a b -> Relation b a
conv (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) = Matrix Boolean (Normalize b) (Normalize a) -> Relation b a
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize b) (Normalize a)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
I.tr Matrix Boolean (Normalize a) (Normalize b)
a)
sse :: Relation a b -> Relation a b -> Bool
sse :: Relation a b -> Relation a b -> Bool
sse a :: Relation a b
a b :: Relation a b
b = Relation a b
a Relation a b -> Relation a b -> Bool
forall a. Ord a => a -> a -> Bool
<= Relation a b
b
implies :: Relation a b -> Relation a b -> Relation a b
implies :: Relation a b -> Relation a b -> Relation a b
implies r :: Relation a b
r s :: Relation a b
s = Relation a b -> Relation a b
forall a. Num a => a -> a
negate Relation a b
r Relation a b -> Relation a b -> Relation a b
forall a b. Relation a b -> Relation a b -> Relation a b
`union` Relation a b
s
iff :: Relation a b -> Relation a b -> Bool
iff :: Relation a b -> Relation a b -> Bool
iff r :: Relation a b
r s :: Relation a b
s = Relation a b
r Relation a b -> Relation a b -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a b
s
intersection :: Relation a b -> Relation a b -> Relation a b
intersection :: Relation a b -> Relation a b -> Relation a b
intersection a :: Relation a b
a b :: Relation a b
b = Relation a b
a Relation a b -> Relation a b -> Relation a b
forall a. Num a => a -> a -> a
* Relation a b
b
union :: Relation a b -> Relation a b -> Relation a b
union :: Relation a b -> Relation a b -> Relation a b
union a :: Relation a b
a b :: Relation a b
b = Relation a b
a Relation a b -> Relation a b -> Relation a b
forall a. Num a => a -> a -> a
+ Relation a b
b
ker :: Relation a b -> Relation a a
ker :: Relation a b -> Relation a a
ker r :: Relation a b
r = Relation a b -> Relation b a
forall a b. Relation a b -> Relation b a
conv Relation a b
r Relation b a -> Relation a b -> Relation a a
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b
r
img :: Relation a b -> Relation b b
img :: Relation a b -> Relation b b
img r :: Relation a b
r = Relation a b
r Relation a b -> Relation b a -> Relation b b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation b a
forall a b. Relation a b -> Relation b a
conv Relation a b
r
divisionF :: Relation a c -> Relation b c -> Relation a b
divisionF :: Relation a c -> Relation b c -> Relation a b
divisionF f :: Relation a c
f g :: Relation b c
g = Relation b c -> Relation c b
forall a b. Relation a b -> Relation b a
conv Relation b c
g Relation c b -> Relation a c -> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a c
f
simple :: (CountableN b, FromListsN b b) => Relation a b -> Bool
simple :: Relation a b -> Bool
simple = Relation b b -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
coreflexive (Relation b b -> Bool)
-> (Relation a b -> Relation b b) -> Relation a b -> Bool
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation b b
forall a b. Relation a b -> Relation b b
img
injective :: (CountableN a, FromListsN a a) => Relation a b -> Bool
injective :: Relation a b -> Bool
injective = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
coreflexive (Relation a a -> Bool)
-> (Relation a b -> Relation a a) -> Relation a b -> Bool
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation a a
forall a b. Relation a b -> Relation a a
ker
entire :: (CountableN a, FromListsN a a) => Relation a b -> Bool
entire :: Relation a b -> Bool
entire = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
reflexive (Relation a a -> Bool)
-> (Relation a b -> Relation a a) -> Relation a b -> Bool
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation a a
forall a b. Relation a b -> Relation a a
ker
surjective :: (CountableN b, FromListsN b b) => Relation a b -> Bool
surjective :: Relation a b -> Bool
surjective = Relation b b -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
reflexive (Relation b b -> Bool)
-> (Relation a b -> Relation b b) -> Relation a b -> Bool
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation b b
forall a b. Relation a b -> Relation b b
img
function ::
( CountableDimensionsN a b,
FromListsN a a,
FromListsN b b
)
=> Relation a b -> Bool
function :: Relation a b -> Bool
function r :: Relation a b
r = Relation a b -> Bool
forall b a. (CountableN b, FromListsN b b) => Relation a b -> Bool
simple Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall a b. (CountableN a, FromListsN a a) => Relation a b -> Bool
entire Relation a b
r
representation ::
( CountableN a,
FromListsN a a
)
=> Relation a b -> Bool
representation :: Relation a b -> Bool
representation r :: Relation a b
r = Relation a b -> Bool
forall a b. (CountableN a, FromListsN a a) => Relation a b -> Bool
injective Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall a b. (CountableN a, FromListsN a a) => Relation a b -> Bool
entire Relation a b
r
abstraction ::
( CountableN b,
FromListsN b b
)
=> Relation a b -> Bool
abstraction :: Relation a b -> Bool
abstraction r :: Relation a b
r = Relation a b -> Bool
forall b a. (CountableN b, FromListsN b b) => Relation a b -> Bool
surjective Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall b a. (CountableN b, FromListsN b b) => Relation a b -> Bool
simple Relation a b
r
surjection ::
( CountableDimensionsN a b,
FromListsN a a,
FromListsN b b
)
=> Relation a b -> Bool
surjection :: Relation a b -> Bool
surjection r :: Relation a b
r = Relation a b -> Bool
forall a b.
(CountableDimensionsN a b, FromListsN a a, FromListsN b b) =>
Relation a b -> Bool
function Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall b a. (CountableN b, FromListsN b b) => Relation a b -> Bool
abstraction Relation a b
r
injection ::
( CountableDimensionsN a b,
FromListsN a a,
FromListsN b b
)
=> Relation a b -> Bool
injection :: Relation a b -> Bool
injection r :: Relation a b
r = Relation a b -> Bool
forall a b.
(CountableDimensionsN a b, FromListsN a a, FromListsN b b) =>
Relation a b -> Bool
function Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall a b. (CountableN a, FromListsN a a) => Relation a b -> Bool
representation Relation a b
r
bijection ::
( CountableDimensionsN a b,
FromListsN b b,
FromListsN a a
) => Relation a b -> Bool
bijection :: Relation a b -> Bool
bijection r :: Relation a b
r = Relation a b -> Bool
forall a b.
(CountableDimensionsN a b, FromListsN a a, FromListsN b b) =>
Relation a b -> Bool
injection Relation a b
r Bool -> Bool -> Bool
&& Relation a b -> Bool
forall a b.
(CountableDimensionsN a b, FromListsN a a, FromListsN b b) =>
Relation a b -> Bool
surjection Relation a b
r
reflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
reflexive :: Relation a a -> Bool
reflexive r :: Relation a a
r = Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id Relation a a -> Relation a a -> Bool
forall a. Ord a => a -> a -> Bool
<= Relation a a
r
coreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
coreflexive :: Relation a a -> Bool
coreflexive r :: Relation a a
r = Relation a a
r Relation a a -> Relation a a -> Bool
forall a. Ord a => a -> a -> Bool
<= Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id
transitive :: Relation a a -> Bool
transitive :: Relation a a -> Bool
transitive r :: Relation a a
r = (Relation a a
r Relation a a -> Relation a a -> Relation a a
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a a
r) Relation a a -> Relation a a -> Bool
forall a b. Relation a b -> Relation a b -> Bool
`sse` Relation a a
r
symmetric :: Relation a a -> Bool
symmetric :: Relation a a -> Bool
symmetric r :: Relation a a
r = Relation a a
r Relation a a -> Relation a a -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a a -> Relation a a
forall a b. Relation a b -> Relation b a
conv Relation a a
r
antiSymmetric :: (CountableN a, FromListsN a a) => Relation a a -> Bool
antiSymmetric :: Relation a a -> Bool
antiSymmetric r :: Relation a a
r = (Relation a a
r Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a a -> Relation a a
forall a b. Relation a b -> Relation b a
conv Relation a a
r) Relation a a -> Relation a a -> Bool
forall a b. Relation a b -> Relation a b -> Bool
`sse` Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id
irreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
irreflexive :: Relation a a -> Bool
irreflexive r :: Relation a a
r = (Relation a a
r Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id) Relation a a -> Relation a a -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a a
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
zeros
connected :: (CountableN a, FromListsN a a) => Relation a a -> Bool
connected :: Relation a a -> Bool
connected r :: Relation a a
r = (Relation a a
r Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`union` Relation a a -> Relation a a
forall a b. Relation a b -> Relation b a
conv Relation a a
r) Relation a a -> Relation a a -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a a
forall a b.
(FromListsN a b, CountableDimensionsN a b) =>
Relation a b
ones
preorder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
preorder :: Relation a a -> Bool
preorder r :: Relation a a
r = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
reflexive Relation a a
r Bool -> Bool -> Bool
&& Relation a a -> Bool
forall a. Relation a a -> Bool
transitive Relation a a
r
partialOrder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
partialOrder :: Relation a a -> Bool
partialOrder r :: Relation a a
r = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
antiSymmetric Relation a a
r Bool -> Bool -> Bool
&& Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
preorder Relation a a
r
linearOrder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
linearOrder :: Relation a a -> Bool
linearOrder r :: Relation a a
r = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
connected Relation a a
r Bool -> Bool -> Bool
&& Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
partialOrder Relation a a
r
equivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool
equivalence :: Relation a a -> Bool
equivalence r :: Relation a a
r = Relation a a -> Bool
forall a. Relation a a -> Bool
symmetric Relation a a
r Bool -> Bool -> Bool
&& Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
preorder Relation a a
r
partialEquivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool
partialEquivalence :: Relation a a -> Bool
partialEquivalence r :: Relation a a
r = Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
partialOrder Relation a a
r Bool -> Bool -> Bool
&& Relation a a -> Bool
forall a. (CountableN a, FromListsN a a) => Relation a a -> Bool
equivalence Relation a a
r
difunctional :: Relation a b -> Bool
difunctional :: Relation a b -> Bool
difunctional r :: Relation a b
r = Relation a b
r Relation a b -> Relation b a -> Relation b b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b -> Relation b a
forall a b. Relation a b -> Relation b a
conv Relation a b
r Relation b b -> Relation a b -> Relation a b
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation a b
r Relation a b -> Relation a b -> Bool
forall a. Eq a => a -> a -> Bool
== Relation a b
r
splitR ::
( CountableDimensionsN a b,
CountableN (a, b),
FromListsN (a, b) a,
FromListsN (a, b) b,
TrivialP a b
)
=> Relation c a -> Relation c b -> Relation c (a, b)
splitR :: Relation c a -> Relation c b -> Relation c (a, b)
splitR (R f :: Matrix Boolean (Normalize c) (Normalize a)
f) (R g :: Matrix Boolean (Normalize c) (Normalize b)
g) = Matrix Boolean (Normalize c) (Normalize (a, b))
-> Relation c (a, b)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize c) (Normalize a)
-> Matrix Boolean (Normalize c) (Normalize b)
-> Matrix
Boolean (Normalize c) (Normalize (Normalize a, Normalize b))
forall e cols a b.
(Num e, CountableDimensions a b, CountableN (a, b),
FromLists e (Normalize (a, b)) a,
FromLists e (Normalize (a, b)) b) =>
Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
I.kr Matrix Boolean (Normalize c) (Normalize a)
f Matrix Boolean (Normalize c) (Normalize b)
g)
fstR ::
forall a b .
( CountableDimensionsN a b,
CountableN (a, b),
FromListsN (a, b) a,
TrivialP a b
)
=> Relation (a, b) a
fstR :: Relation (a, b) a
fstR = Matrix Boolean (Normalize (a, b)) (Normalize a)
-> Relation (a, b) a
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R ((Num Boolean, CountableDimensions (Normalize b) (Normalize a),
FromLists
Boolean (Normalize (Normalize a, Normalize b)) (Normalize a),
CountableN (Normalize a, Normalize b)) =>
Matrix Boolean (Normalize (Normalize a, Normalize b)) (Normalize a)
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) m,
CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
sndR ::
forall a b .
( CountableDimensionsN a b,
CountableN (a, b),
FromListsN (a, b) b,
TrivialP a b
)
=> Relation (a, b) b
sndR :: Relation (a, b) b
sndR = Matrix Boolean (Normalize (a, b)) (Normalize b)
-> Relation (a, b) b
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R ((Num Boolean, CountableDimensions (Normalize b) (Normalize a),
FromLists
Boolean (Normalize (Normalize a, Normalize b)) (Normalize b),
CountableN (Normalize a, Normalize b)) =>
Matrix Boolean (Normalize (Normalize a, Normalize b)) (Normalize b)
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) k,
CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))
infixl 4 ><
(><) ::
( CountableDimensionsN a b,
CountableDimensionsN c d,
CountableDimensionsN (a, c) (b, d),
FromListsN (a, c) a,
FromListsN (a, c) c,
FromListsN (b, d) b,
FromListsN (b, d) d,
TrivialP a c,
TrivialP b d
)
=> Relation a b -> Relation c d -> Relation (a, c) (b, d)
>< :: Relation a b -> Relation c d -> Relation (a, c) (b, d)
(><) (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) (R b :: Matrix Boolean (Normalize c) (Normalize d)
b) = Matrix Boolean (Normalize (a, c)) (Normalize (b, d))
-> Relation (a, c) (b, d)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize c) (Normalize d)
-> Matrix
Boolean
(Normalize (Normalize a, Normalize c))
(Normalize (Normalize b, Normalize d))
forall e m p n q.
(Num e, CountableDimensions m n, CountableDimensions p q,
CountableDimensionsN (m, n) (p, q),
FromLists e (Normalize (m, n)) m, FromLists e (Normalize (m, n)) n,
FromLists e (Normalize (p, q)) p,
FromLists e (Normalize (p, q)) q) =>
Matrix e m p
-> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
(I.><) Matrix Boolean (Normalize a) (Normalize b)
a Matrix Boolean (Normalize c) (Normalize d)
b)
eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c
eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c
eitherR = Relation a c -> Relation b c -> Relation (Either a b) c
forall a c b.
Relation a c -> Relation b c -> Relation (Either a b) c
join
i1 ::
( CountableDimensionsN a b,
FromListsN b a,
FromListsN a a
)
=> Relation a (Either a b)
i1 :: Relation a (Either a b)
i1 = Matrix Boolean (Normalize a) (Normalize (Either a b))
-> Relation a (Either a b)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R Matrix Boolean (Normalize a) (Normalize (Either a b))
forall e n m.
(Num e, CountableDimensions n m, FromLists e n m,
FromLists e m m) =>
Matrix e m (Either m n)
I.i1
i2 ::
( CountableDimensionsN a b,
FromListsN a b,
FromListsN b b
)
=> Relation b (Either a b)
i2 :: Relation b (Either a b)
i2 = Matrix Boolean (Normalize b) (Normalize (Either a b))
-> Relation b (Either a b)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R Matrix Boolean (Normalize b) (Normalize (Either a b))
forall e n m.
(Num e, CountableDimensions n m, FromLists e m n,
FromLists e n n) =>
Matrix e n (Either m n)
I.i2
infixl 5 -|-
(-|-) ::
( CountableDimensionsN b d,
FromListsN b b,
FromListsN d b,
FromListsN b d,
FromListsN d d
)
=> Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
-|- :: Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
(-|-) (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) (R b :: Matrix Boolean (Normalize c) (Normalize d)
b) = Matrix Boolean (Normalize (Either a c)) (Normalize (Either b d))
-> Relation (Either a c) (Either b d)
forall a b.
Matrix Boolean (Normalize a) (Normalize b) -> Relation a b
R (Matrix Boolean (Normalize a) (Normalize b)
-> Matrix Boolean (Normalize c) (Normalize d)
-> Matrix
Boolean
(Either (Normalize a) (Normalize c))
(Either (Normalize b) (Normalize d))
forall e n k m j.
(Num e, CountableDimensions j k, FromLists e k k, FromLists e j k,
FromLists e k j, FromLists e j j) =>
Matrix e n k -> Matrix e m j -> Matrix e (Either n m) (Either k j)
(I.-|-) Matrix Boolean (Normalize a) (Normalize b)
a Matrix Boolean (Normalize c) (Normalize d)
b)
trans ::
( CountableDimensionsN a b,
CountableN c,
CountableDimensionsN (a, b) (c, b),
FromListsN (c, b) c,
FromListsN (c, b) b,
FromListsN (a, b) a,
FromListsN (a, b) b,
Trivial (a, b),
Trivial (c, b),
TrivialP a b,
TrivialP c b
)
=> Relation (a, b) c -> Relation a (c, b)
trans :: Relation (a, b) c -> Relation a (c, b)
trans r :: Relation (a, b) c
r = Relation (a, b) c -> Relation (a, b) b -> Relation (a, b) (c, b)
forall a b c.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) a,
FromListsN (a, b) b, TrivialP a b) =>
Relation c a -> Relation c b -> Relation c (a, b)
splitR Relation (a, b) c
r Relation (a, b) b
forall a b.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) b,
TrivialP a b) =>
Relation (a, b) b
sndR Relation (a, b) (c, b) -> Relation a (a, b) -> Relation a (c, b)
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation (a, b) a -> Relation a (a, b)
forall a b. Relation a b -> Relation b a
conv Relation (a, b) a
forall a b.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) a,
TrivialP a b) =>
Relation (a, b) a
fstR
untrans ::
( CountableDimensionsN a b,
CountableN c,
CountableDimensionsN (a, b) (c, b),
FromListsN (c, b) c,
FromListsN (c, b) b,
FromListsN (a, b) b,
FromListsN (a, b) a,
Trivial (a, b),
Trivial (c, b),
TrivialP a b,
TrivialP c b
)
=> Relation a (c, b) -> Relation (a, b) c
untrans :: Relation a (c, b) -> Relation (a, b) c
untrans s :: Relation a (c, b)
s = Relation (c, b) c
forall a b.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) a,
TrivialP a b) =>
Relation (a, b) a
fstR Relation (c, b) c -> Relation (a, b) (c, b) -> Relation (a, b) c
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation (c, b) (a, b) -> Relation (a, b) (c, b)
forall a b. Relation a b -> Relation b a
conv (Relation (c, b) a -> Relation (c, b) b -> Relation (c, b) (a, b)
forall a b c.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) a,
FromListsN (a, b) b, TrivialP a b) =>
Relation c a -> Relation c b -> Relation c (a, b)
splitR (Relation a (c, b) -> Relation (c, b) a
forall a b. Relation a b -> Relation b a
conv Relation a (c, b)
s) Relation (c, b) b
forall a b.
(CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) b,
TrivialP a b) =>
Relation (a, b) b
sndR)
predR ::
( Bounded a,
Enum a,
CountableN a,
FromListsN a a,
FromListsN Bool a
)
=> Relation a Bool -> Relation a a
predR :: Relation a Bool -> Relation a a
predR p :: Relation a Bool
p = Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a Bool -> Relation a Bool -> Relation a a
forall a c b. Relation a c -> Relation b c -> Relation a b
divisionF ((a -> Bool) -> Relation a Bool
forall a b.
(Liftable a b, CountableDimensionsN a b, FromListsN b a) =>
(a -> b) -> Relation a b
fromF (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True)) Relation a Bool
p
equalizer ::
( CountableN a,
FromListsN a a
)
=> Relation a b -> Relation a b -> Relation a a
equalizer :: Relation a b -> Relation a b -> Relation a a
equalizer f :: Relation a b
f g :: Relation a b
g = Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a b -> Relation a b -> Relation a a
forall a c b. Relation a c -> Relation b c -> Relation a b
divisionF Relation a b
f Relation a b
g
guard ::
( Bounded b,
Enum b,
CountableN b,
FromListsN b b,
FromListsN Bool b
) => Relation b Bool -> Relation b (Either b b)
guard :: Relation b Bool -> Relation b (Either b b)
guard p :: Relation b Bool
p = Relation (Either b b) b -> Relation b (Either b b)
forall a b. Relation a b -> Relation b a
conv (Relation b b -> Relation b b -> Relation (Either b b) b
forall a c b.
Relation a c -> Relation b c -> Relation (Either a b) c
eitherR (Relation b Bool -> Relation b b
forall a.
(Bounded a, Enum a, CountableN a, FromListsN a a,
FromListsN Bool a) =>
Relation a Bool -> Relation a a
predR Relation b Bool
p) (Relation b Bool -> Relation b b
forall a.
(Bounded a, Enum a, CountableN a, FromListsN a a,
FromListsN Bool a) =>
Relation a Bool -> Relation a a
predR (Relation b Bool -> Relation b Bool
forall a. Num a => a -> a
negate Relation b Bool
p)))
cond ::
( Bounded b,
Enum b,
CountableN b,
FromListsN b b,
FromListsN Bool b
)
=> Relation b Bool -> Relation b c -> Relation b c -> Relation b c
cond :: Relation b Bool -> Relation b c -> Relation b c -> Relation b c
cond p :: Relation b Bool
p r :: Relation b c
r s :: Relation b c
s = Relation b c -> Relation b c -> Relation (Either b b) c
forall a c b.
Relation a c -> Relation b c -> Relation (Either a b) c
eitherR Relation b c
r Relation b c
s Relation (Either b b) c -> Relation b (Either b b) -> Relation b c
forall (k :: * -> * -> *) b c a.
Category k =>
k b c -> k a b -> k a c
. Relation b Bool -> Relation b (Either b b)
forall b.
(Bounded b, Enum b, CountableN b, FromListsN b b,
FromListsN Bool b) =>
Relation b Bool -> Relation b (Either b b)
guard Relation b Bool
p
domain ::
( CountableN a,
FromListsN a a
) => Relation a b -> Relation a a
domain :: Relation a b -> Relation a a
domain r :: Relation a b
r = Relation a b -> Relation a a
forall a b. Relation a b -> Relation a a
ker Relation a b
r Relation a a -> Relation a a -> Relation a a
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation a a
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id
range ::
( CountableN b,
FromListsN b b
) => Relation a b -> Relation b b
range :: Relation a b -> Relation b b
range r :: Relation a b
r = Relation a b -> Relation b b
forall a b. Relation a b -> Relation b b
img Relation a b
r Relation b b -> Relation b b -> Relation b b
forall a b. Relation a b -> Relation a b -> Relation a b
`intersection` Relation b b
forall (k :: * -> * -> *) a. (Category k, Object k a) => k a a
id
pretty :: (CountableDimensionsN a b) => Relation a b -> String
pretty :: Relation a b -> String
pretty (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) = Matrix Boolean (Normalize a) (Normalize b) -> String
forall cols rows e.
(CountableDimensions cols rows, Show e) =>
Matrix e cols rows -> String
I.pretty Matrix Boolean (Normalize a) (Normalize b)
a
prettyPrint :: (CountableDimensionsN a b) => Relation a b -> IO ()
prettyPrint :: Relation a b -> IO ()
prettyPrint (R a :: Matrix Boolean (Normalize a) (Normalize b)
a) = Matrix Boolean (Normalize a) (Normalize b) -> IO ()
forall cols rows e.
(CountableDimensions cols rows, Show e) =>
Matrix e cols rows -> IO ()
I.prettyPrint Matrix Boolean (Normalize a) (Normalize b)
a