{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DataKinds #-}

-----------------------------------------------------------------------------
-- |
-- Module     : LAoP.Relation.Internal
-- Copyright  : (c) Armando Santos 2019-2020
-- Maintainer : armandoifsantos@gmail.com
-- Stability  : experimental
--
-- The AoP discipline generalises functions to relations which are 
-- Boolean matrices.
--
-- This module offers many of the combinators of the Algebra of
-- Programming discipline. It is still under construction and very
-- experimental.
--
-- This is an Internal module and it is no supposed to be imported.
--
-----------------------------------------------------------------------------

module LAoP.Relation.Internal
  ( -- | This definition makes use of the fact that 'Void' is
    -- isomorphic to 0 and 'One' to 1 and captures matrix
    -- dimensions as stacks of 'Either's.
    --
    -- There exists two type families that make it easier to write
    -- matrix dimensions: 'FromNat' and 'Count'. This approach
    -- leads to a very straightforward implementation 
    -- of LAoP combinators. 

    -- * Relation data type
    Relation (..),
    Boolean,

    -- * Constraint type synonyms
    Countable,
    CountableDimensions,
    CountableN,
    CountableDimensionsN,
    FromListsN,
    Liftable,
    Trivial,
    TrivialP,

    -- * Primitives
    empty,
    one,
    join,
    (|||),
    fork,
    (===),

    -- * Auxiliary type families
    I.FromNat,
    I.Count,
    I.Normalize,

    -- * Matrix construction and conversion
    I.FromLists,
    fromLists,
    fromF',
    fromF,
    toRel,
    toLists,
    toList,
    toBool,
    pt,
    belongs,
    relationBuilder',
    relationBuilder,
    zeros,
    ones,
    bang,
    point,

    -- * Relational operations
    conv,
    intersection,
    union,
    sse,
    implies,
    iff,
    ker,
    img,

    -- * Taxonomy of binary relations
    injective,
    entire,
    simple,
    surjective,
    representation,
    function,
    abstraction,
    injection,
    surjection,
    bijection,
    domain,
    range,

    -- * Function division
    divisionF,

    -- * Relation division
    divR,
    divL,
    divS,
    shrunkBy,
    overriddenBy,

    -- * Relational pairing
    splitR,

    -- ** Projections
    fstR,
    sndR,
    -- ** Bifunctor
    (><),
    -- * Relational coproduct
    eitherR,
    -- ** Injections
    i1,
    i2,
    -- ** Bifunctor
    (-|-),

    -- * Relational "currying"
    trans,
    untrans,

    -- * (Endo-)Relational properties
    reflexive,
    coreflexive,
    transitive,
    symmetric,
    antiSymmetric,
    irreflexive,
    connected,
    preorder,
    partialOrder,
    linearOrder,
    equivalence,
    partialEquivalence,
    difunctional,

    -- * Conditionals
    equalizer,

    -- ** McCarthy's Conditional
    predR,
    guard,
    cond,

    -- * Relational composition and lifting
    iden,
    comp,
    fromF',
    fromF,

    -- ** Relational application
    pointAp,
    pointApBool,

    -- * Matrix printing
    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, (.))

-- | Boolean type synonym for working with boolean matrices
type Boolean = Natural 0 1
type Powerset a = List (List a)

-- | Relation data type.
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)

-- | Constraint type synonyms to keep the type signatures less convoluted
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)

-- | It is possible to implement a constrained version of the category type
-- class.
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
    -- | Matrix addition becomes Boolean matrix disjointion
    (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)

    -- | Matrix subtraction becomes Relational subtraction
    (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)

    -- | Matrix multiplication becomes Boolean matrix conjointion
    (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)

    -- | Matrix negation becomes Boolean matrix negation
    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 alias
type Zero = Void
type One  = ()

-- Primitives

-- | Empty matrix constructor
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

-- | Unit matrix constructor
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

-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.
--
-- See 'eitherR'.
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 |||
-- | Boolean Matrix 'Join' constructor
--
-- See 'eitherR'.
(|||) ::
  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

-- | Boolean Matrix 'Fork' constructor, also known as relational product.
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 ===
-- | Boolean Matrix 'Fork' constructor
(===) ::
  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

-- Construction

-- | Build a matrix out of a list of list of elements. Throws a runtime
-- error if the dimensions do not match.
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

-- | Relation builder function. Constructs a relation provided with
-- a construction function that operates with indices.
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'

-- | Relation builder function. Constructs a relation provided with
-- a construction function that operates with arbitrary types.
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

-- | Lifts functions to matrices with arbitrary dimensions.
--
--   NOTE: Be careful to not ask for a matrix bigger than the cardinality of
-- types @a@ or @b@ allows.
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)

-- | Lifts functions to matrices with dimensions matching @a@ and @b@
-- cardinality's.
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)

-- | Lifts relation functions to 'Relation'
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

-- | Lowers a 'Relation' to a function
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

-- Conversion

-- | Converts a matrix to a list of lists of elements.
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

-- | Converts a matrix to a list of elements.
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

-- | Converts a well typed 'Relation' to 'Bool'.
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

-- | Power transpose.
--
--  Maps a relation to a set valued function.
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 relation
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 Matrix

-- | The zero relation. A relation where no element of type @a@ relates
-- with elements of type @b@.
--
--   Also known as ⊥ (Bottom) Relation or empty Relation.
--
--   @
--   r `.` ⊥ == ⊥ `.` r == ⊥
--   ⊥ ``sse`` R && R ``sse`` T == True
--   @
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 Matrix

-- | The ones relation. A relation where every element of type @a@ relates
-- with every element of type @b@.
--
--   Also known as T (Top) Relation or universal Relation.
--
--   @
--   ⊥ ``sse`` R && R ``sse`` T == True
--   @
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 Matrix

-- | The T (Top) row vector relation.
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 constant relation
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 Matrix

-- | iden matrix
--
-- @
-- 'iden' `.` r == r == r `.` 'iden'
-- @
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
(==))

-- | Relational composition
--
-- @
-- r `.` (s `.` p) = (r `.` s) `.` p
-- @
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)

-- | Relational right division
--
-- @'divR' x y@ is the largest relation @z@ which, 
-- pre-composed with @y@, approximates @x@.
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)

-- | Relational left division
--
-- The dual division operator:
--
-- @
-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' 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)

-- | Relational symmetric division
--
-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@ 
-- are related to exactly the same outputs by @r@ and by @s@.
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)

-- | Relational shrinking.
--
-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
-- if it yields an output for an input @x@, it must be a maximum,
-- with respect to @s@, among all possible outputs of @x@ by @r@.
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)

-- | Relational overriding.
--
-- @r ``overriddenBy`` s@ yields the relation which contains the
-- whole of @s@ and that part of @r@ where @s@ is undefined.
--
-- @
-- 'zeros' ``overriddenBy`` s == s
-- r ``overriddenBy`` 'zeros' == r
-- r ``overriddenBy`` r       == 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)

-- | Relational application.
--
-- If @a@ and @b@ are related by 'Relation' @r@
-- then @'pointAp' a b r == 'one' ('nat' 1)@
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

-- | Relational application
--
-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
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

-- | Relational converse
--
-- Given binary 'Relation' r, writing @'pointAp' a b r@
-- (read: “@b@ is related to @a@ by @r@”) means the same as
-- @'pointAp' b a ('conv' r)@, where @'conv' r@ is said to be 
-- the converse of @r@. 
-- In terms of grammar, @'conv' r@ corresponds to the passive voice
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)

-- | Relational inclusion (subset or equal)
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

-- | Relational implication (the same as @'sse'@)
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

-- | Relational bi-implication
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

-- | Relational intersection
--
-- Lifts pointwise conjointion.
--
-- @
-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` 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

-- | Relational union
--
-- Lifts pointwise disjointion.
--
-- @
-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)
-- (s ``union`` t) `.` r ==  (s `.` r) ``union`` (t `.` r)
-- @
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

-- | Relation Kernel
--
-- @
-- 'ker' r == 'conv' r `.` r
-- 'ker' r == 'img' ('conv' r)
-- @
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

-- | Relation Image
--
-- @
-- 'img' r == r `.` conv r
-- 'img' r == 'ker' ('conv' 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

-- | Function division. Special case of 'divS'.
--
-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
-- 'entire'.
--
-- @'divisionF' f g == 'conv' g `.` f@
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

-- Taxonomy of binary relations

-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
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

-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
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

-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
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

-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
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

-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
--
-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
-- relations:
--
-- @
-- f `.` r ``sse`` s == r ``sse`` f `.` s
-- r `.` f ``sse`` s == r ``sse`` s `.` f
-- @
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

-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' 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

-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' 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

-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' 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

-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' 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

-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' 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

-- Properties of relations

-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` 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

-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
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

-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
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

-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' 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

-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@
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

-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@
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

-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
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

-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
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

-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' 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

-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' 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

-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' 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

-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' 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

-- | A 'Relation' @r@ is 'difunctional' or regular wherever 
-- @r `.` 'conv' r `.` r == 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

-- Relational pairing

-- | Relational pairing.
--
--   NOTE: That this is not a true categorical product, see for instance:
--
-- @
--                | 'fstR' `.` 'splitR' a b ``sse`` a 
-- 'splitR' a b <=>   |
--                | 'sndR' `.` 'splitR' a b ``sse`` b
-- @
--
-- __Emphasis__ on the 'sse'.
--
-- @
-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)
-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)
-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)
-- @
--
-- @
-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
-- @
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)

-- | Relational pairing first component projection
--
-- @
-- 'fstR' `.` 'splitR' r s ``sse`` r
-- @
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))

-- | Relational pairing second component projection
--
-- @
-- 'sndR' `.` 'splitR' r s ``sse`` s
-- @
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))

-- Relational pairing functor

infixl 4 ><
-- | Relational pairing functor
--
-- @
-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
-- @
(><) ::
     ( 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)

-- Relational co-products

-- | Relational coproduct.
--
-- @
--                | 'eitherR' a b `.` 'i1' == a
-- 'eitherR' a b <=>  |
--                | 'eitherR' a b `.` 'i2' == b
-- @
--
-- @
-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)
-- @
--
-- @
-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
-- @
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

-- | Relational coproduct first component injection
--
-- @
-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
-- 'i1' `.` 'i2' = 'zeros'
-- @
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

-- | Relational coproduct second component injection
--
-- @
-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
-- 'i1' `.` 'i2' = 'zeros'
-- @
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 -|-

-- | Relational coproduct functor.
--
-- @
-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
-- @
(-|-) ::
  ( 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)

-- Relational "Currying"

-- | Relational 'trans'
--
-- Every n-ary relation can be expressed as a binary relation through
-- 'trans'/'untrans';
-- more-over, where each particular attribute is placed (input/output) is irrelevant.
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

-- | Relational 'untrans'
--
-- Every n-ary relation can be expressed as a binary relation through
-- 'trans'/'untrans';
-- more-over, where each particular attribute is placed (input/output) is irrelevant.
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)

-- | Transforms predicate @p@ into a correflexive relation.
--
-- @
-- 'predR' ('const' True) == 'id'
-- 'predR' ('const' False) == 'zeros'
-- @
--
-- @
-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p
-- @
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

-- | Equalizes functions @f@ and @g@.
-- That is, @'equalizer' f g@ is the largest coreflexive
-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
--
-- @
-- 'equalizer' r r == 'id'
-- 'equalizer' ('point' True) ('point' False) == 'zeros'
-- @
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

-- | Relational conditional guard.
--
-- @
-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p
-- @
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)))

-- | Relational McCarthy's conditional.
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

-- | Relational domain.
--
-- For injective relations, 'domain' and 'ker'nel coincide,
-- since @'ker' r ``sse`` 'id'@ in such situations.
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

-- | Relational range.
--
-- For functions, 'range' and 'img' (image) coincide,
-- since @'img' f ``sse`` id@ for any @f@.
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

-- Relation pretty print

-- | Relation pretty printing
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

-- | Relation pretty printing
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