LAoP.Relation

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.

Documentation

This definition makes use of the fact that Void is isomorphic to 0 and '()' to 1 and captures matrix dimensions as stacks of Eithers.

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

newtype Relation a b

Relation data type.

Constructors

R (Matrix Boolean (Normalize a) (Normalize b))

Instances

Category Relation

It is possible to implement a constrained version of the category type class.

Defined in LAoP.Relation.Internal

Associated Types

type Object Relation o :: Constraint

Methods

id :: Object Relation a => Relation a a

(.) :: Relation b c -> Relation a b -> Relation a c

Eq (Relation a b)

Defined in LAoP.Relation.Internal

Methods

(==) :: Relation a b -> Relation a b -> Bool

(/=) :: Relation a b -> Relation a b -> Bool

Num (Relation a b)

Defined in LAoP.Relation.Internal

Methods

(+) :: Relation a b -> Relation a b -> Relation a b

(-) :: Relation a b -> Relation a b -> Relation a b

(*) :: Relation a b -> Relation a b -> Relation a b

negate :: Relation a b -> Relation a b

abs :: Relation a b -> Relation a b

signum :: Relation a b -> Relation a b

fromInteger :: Integer -> Relation a b

Ord (Relation a b)

Defined in LAoP.Relation.Internal

Methods

compare :: 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

max :: Relation a b -> Relation a b -> Relation a b

min :: Relation a b -> Relation a b -> Relation a b

Read (Matrix Boolean (Normalize a) (Normalize b)) => Read (Relation a b)

Defined in LAoP.Relation.Internal

Methods

readsPrec :: Int -> ReadS (Relation a b)

readList :: ReadS [Relation a b]

readPrec :: ReadPrec (Relation a b)

readListPrec :: ReadPrec [Relation a b]

Show (Relation a b)

Defined in LAoP.Relation.Internal

Methods

showsPrec :: Int -> Relation a b -> ShowS

show :: Relation a b -> String

showList :: [Relation a b] -> ShowS

NFData (Relation a b)

Defined in LAoP.Relation.Internal

Methods

rnf :: Relation a b -> ()

type Object Relation a

Defined in LAoP.Relation.Internal

type Object Relation a = (FLN a a, CountableN a)

type Boolean = Natural 0 1

Boolean type synonym for working with boolean matrices

Constraint type synonyms

type Countable a = KnownNat (Count a)

Constraint type synonyms to keep the type signatures less convoluted

type CountableDims a b = (Countable a, Countable b)

type CountableN a = KnownNat (Count (Normalize a))

type CountableDimsN a b = (CountableN a, CountableN b)

type FLN a b = FromLists (Normalize a) (Normalize b)

type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)

type Trivial a = Normalize a ~ Normalize (Normalize a)

type TrivialP a b = Normalize (a, b) ~ Normalize (Normalize a, Normalize b)

Primitives

one :: Boolean -> Relation One One

Unit matrix constructor

join :: Relation a c -> Relation b c -> Relation (Either a b) c

Boolean Matrix Join constructor, also known as relational coproduct.

See eitherR.

(|||) :: Relation a c -> Relation b c -> Relation (Either a b) c infixl 3

Boolean Matrix Join constructor

See eitherR.

fork :: Relation c a -> Relation c b -> Relation c (Either a b)

Boolean Matrix Fork constructor, also known as relational product.

(===) :: Relation c a -> Relation c b -> Relation c (Either a b) infixl 2

Boolean Matrix Fork constructor

Auxiliary type families

type family FromNat (n :: Nat) :: Type where ...

Type family that computes of a given type dimension from a given natural

Thanks to Li-Yao Xia this type family is super fast.

Equations

FromNat 1 = ()

FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

type family Count (d :: Type) :: Nat where ...

Type family that computes the cardinality of a given type dimension.

It can also count the cardinality of custom types that implement the Generic instance.

Equations

Count (Natural n m) = (m - n) + 1

Count (List a) = (^) 2 (Count a)

Count (Either a b) = (+) (Count a) (Count b)

Count (a, b) = * (Count a) (Count b)

Count (a -> b) = (^) (Count b) (Count a)

Count (M1 _ _ f p) = Count (f p)

Count (K1 _ _ _) = 1

Count (V1 _) = 0

Count (U1 _) = 1

Count ((:*:) a b p) = Count (a p) * Count (b p)

Count ((:+:) a b p) = Count (a p) + Count (b p)

Count d = Count (Rep d R)

type family Normalize (d :: Type) :: Type where ...

Type family that normalizes the representation of a given data structure

Equations

Normalize (Either a b) = Either (Normalize a) (Normalize b)

Normalize d = FromNat (Count d)

Matrix construction and conversion

class FromLists cols rows

Type class for defining the fromList conversion function.

Given that it is not possible to branch on types at the term level type classes are needed very much like an inductive definition but on types.

Minimal complete definition

fromLists

Instances

FromLists () ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () ()

FromLists () rows => FromLists () (Either () rows)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () (Either () rows)

(FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () (Either a b)

FromLists cols () => FromLists (Either () cols) ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either () cols) ()

(FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either a b) ()

(FromLists (Either a b) c, FromLists (Either a b) d, Countable c) => FromLists (Either a b) (Either c d)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either a b) (Either c d)

fromLists :: FLN a b => [[Boolean]] -> Relation a b

Build a matrix out of a list of list of elements. Throws a runtime error if the dimensions do not match.

fromF :: (Liftable a b, CountableDimsN a b, FLN b a) => (a -> b) -> Relation a b

Lifts functions to matrices with dimensions matching a and b cardinality's.

fromF' :: (Liftable a b, CountableDimsN c d, FLN d c) => (a -> b) -> Relation c d

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.

toRel :: (Liftable a b, CountableDimsN a b, FLN b a) => (a -> b -> Bool) -> Relation a b

Lifts relation functions to Relation

toLists :: Relation a b -> [[Boolean]]

Converts a matrix to a list of lists of elements.

toList :: Relation a b -> [Boolean]

Converts a matrix to a list of elements.

toBool :: Relation One One -> Bool

Converts a well typed Relation to Bool.

pt :: (Liftable a b, Eq a, CountableDimsN a b, FLN a One, FLN b One) => Relation a b -> a -> List b

Power transpose.

Maps a relation to a set valued function.

belongs :: (Bounded a, Enum a, Eq a, CountableDimsN (List a) a, FLN a (List a)) => Relation (List a) a

Belongs relation

relationBuilder :: (FLN a b, Enum a, Enum b, Bounded a, Bounded b, Eq a, CountableDimsN a b) => ((a, b) -> Boolean) -> Relation a b

Relation builder function. Constructs a relation provided with a construction function that operates with arbitrary types.

zeros :: (FLN a b, CountableDimsN a b) => Relation a b

The zero relation. A relation where no element of type a relates with elements of type b.

Also known as ⊥ (Bottom) Relation.

  r . ⊥ == ⊥ . r == ⊥
  ⊥ `sse` R && R `sse` T == True
  

ones :: (FLN a b, CountableDimsN a b) => Relation a b

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
  

bang :: (FLN a One, CountableN a) => Relation a One

The T (Top) row vector relation.

point :: (Bounded a, Enum a, Eq a, CountableN a, FLN a One) => a -> Relation One a

Point constant relation

Relational operations

conv :: Relation a b -> Relation b 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

intersection :: Relation a b -> Relation a b -> Relation a b

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

union :: Relation a b -> Relation a b -> Relation a 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)

sse :: Relation a b -> Relation a b -> Bool

Relational inclusion (subset or equal)

implies :: Relation a b -> Relation a b -> Relation a b

Relational implication (the same as sse)

iff :: Relation a b -> Relation a b -> Bool

Relational bi-implication

ker :: Relation a b -> Relation a a

Relation Kernel

ker r == conv r . r
ker r == img (conv r)

img :: Relation a b -> Relation b b

Relation Image

img r == r . conv r
img r == ker (conv r)

Taxonomy of binary relations

injective :: (CountableN a, FLN a a) => Relation a b -> Bool

A Relation r is injective iff coreflexive (ker r)

entire :: (CountableN a, FLN a a) => Relation a b -> Bool

A Relation r is entire iff reflexive (ker r)

simple :: (CountableN b, FLN b b) => Relation a b -> Bool

A Relation r is simple iff coreflexive (img r)

surjective :: (CountableN b, FLN b b) => Relation a b -> Bool

A Relation r is surjective iff reflexive (img r)

representation :: (CountableN a, FLN a a) => Relation a b -> Bool

A Relation r is a representation iff injective r && entire r

function :: (CountableDimsN a b, FLN a a, FLN b b) => Relation a b -> Bool

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

abstraction :: (CountableN b, FLN b b) => Relation a b -> Bool

A Relation r is an abstraction iff surjective r && simple r

injection :: (CountableDimsN a b, FLN a a, FLN b b) => Relation a b -> Bool

A Relation r is a injection iff function r && representation r

surjection :: (CountableDimsN a b, FLN a a, FLN b b) => Relation a b -> Bool

A Relation r is a surjection iff function r && abstraction r

bijection :: (CountableDimsN a b, FLN b b, FLN a a) => Relation a b -> Bool

A Relation r is an bijection iff injection r && surjection r

domain :: (CountableN a, FLN a a) => Relation a b -> Relation a a

Relational domain.

For injective relations, domain and kernel coincide, since ker r `sse` id in such situations.

range :: (CountableN b, FLN b b) => Relation a b -> Relation b b

Relational range.

For functions, range and img (image) coincide, since img f `sse` id for any f.

Function division

divisionF :: Relation a c -> Relation b c -> Relation a b

Function division. Special case of divS.

NOTE: _This is only valid_ if f and g are functions, i.e. simple and entire.

divisionF f g == conv g . f

Relation division

divR :: Relation b c -> Relation b a -> Relation a c

Relational right division

divR x y is the largest relation z which, pre-composed with y, approximates x.

divL :: Relation c b -> Relation a b -> Relation a c

Relational left division

The dual division operator:

divL y x == conv (divR (conv x) (conv y)

divS :: Relation c a -> Relation b a -> Relation c b

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.

shrunkBy :: Relation b a -> Relation a a -> Relation b a

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.

overriddenBy :: (FLN b b, CountableN b) => Relation a b -> Relation a b -> Relation a b

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

Relational pairing

splitR :: (CountableDimsN a b, CountableN (a, b), FLN (a, b) a, FLN (a, b) b, TrivialP a b) => Relation c a -> Relation c b -> Relation c (a, b)

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)

Projections

fstR :: forall a b. (CountableDimsN a b, CountableN (a, b), FLN (a, b) a, TrivialP a b) => Relation (a, b) a

Relational pairing first component projection

fstR . splitR r s `sse` r

sndR :: forall a b. (CountableDimsN a b, CountableN (a, b), FLN (a, b) b, TrivialP a b) => Relation (a, b) b

Relational pairing second component projection

sndR . splitR r s `sse` s

Bifunctor

(><) :: (CountableDimsN a b, CountableDimsN c d, CountableDimsN (a, c) (b, d), FLN (a, c) a, FLN (a, c) c, FLN (b, d) b, FLN (b, d) d, TrivialP a c, TrivialP b d) => Relation a b -> Relation c d -> Relation (a, c) (b, d) infixl 4

Relational pairing functor

r >< s == splitR (r . fstR) (s . sndR)
(r >< s) . (p >< q) == (r . p) >< (s . q)

Relational coproduct

eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c

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)

Injections

i1 :: (CountableDimsN a b, FLN b a, FLN a a) => Relation a (Either a b)

Relational coproduct first component injection

img i1 `union` img i2 == id
i1 . i2 = zeros

i2 :: (CountableDimsN a b, FLN a b, FLN b b) => Relation b (Either a b)

Relational coproduct second component injection

img i1 `union` img i2 == id
i1 . i2 = zeros

Bifunctor

(-|-) :: (CountableDimsN b d, FLN b b, FLN d b, FLN b d, FLN d d) => Relation a b -> Relation c d -> Relation (Either a c) (Either b d) infixl 5

Relational coproduct functor.

r -|- s == eitherR (i1 . r) (i2 . s)

Relational "currying"

trans :: (CountableDimsN a b, CountableN c, CountableDimsN (a, b) (c, b), FLN (c, b) c, FLN (c, b) b, FLN (a, b) a, FLN (a, b) b, Trivial (a, b), Trivial (c, b), TrivialP a b, TrivialP c b) => Relation (a, b) c -> Relation a (c, b)

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.

untrans :: (CountableDimsN a b, CountableN c, CountableDimsN (a, b) (c, b), FLN (c, b) c, FLN (c, b) b, FLN (a, b) b, FLN (a, b) a, Trivial (a, b), Trivial (c, b), TrivialP a b, TrivialP c b) => Relation a (c, b) -> Relation (a, b) c

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.

(Endo-)Relational properties

reflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is reflexive iff id `sse` r

coreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is coreflexive iff r `sse` id

transitive :: Relation a a -> Bool

A Relation r is transitive iff (r . r) `sse` r

symmetric :: Relation a a -> Bool

A Relation r is symmetric iff r == conv r

antiSymmetric :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is anti-symmetric iff (r `intersection` conv r) `sse` id

irreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is irreflexive iff (r `intersection` id) == zeros

connected :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is connected iff (r `union` conv r) == ones

preorder :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is a preorder iff reflexive r && transitive r

partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is a partial-order iff antiSymmetric r && preorder r

linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is a linear-order iff connected r && partialOrder r

equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is an equivalence iff symmetric r && preorder r

partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool

A Relation r is a partial-equivalence iff partialOrder r && equivalence r

difunctional :: Relation a b -> Bool

A Relation r is difunctional or regular wherever r . conv r . r == r

Conditionals

equalizer :: (CountableN a, FLN a a) => Relation a b -> Relation a b -> Relation a a

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

McCarthy's Conditional

predR :: (Bounded a, Enum a, CountableN a, FLN a a, FLN Bool a) => Relation a Bool -> Relation a a

Transforms predicate p into a correflexive relation.

predR (const True) == id
predR (const False) == zeros

predR q . predR p == predR q `union` predR p

guard :: (Bounded b, Enum b, CountableN b, FLN b b, FLN Bool b) => Relation b Bool -> Relation b (Either b b)

Relational conditional guard.

guard p = i2 `overriddenBy` i1 . predR p

cond :: (Bounded b, Enum b, CountableN b, FLN b b, FLN Bool b) => Relation b Bool -> Relation b c -> Relation b c -> Relation b c

Relational McCarthy's conditional.

Relational composition and lifting

iden :: (FLN a a, CountableN a) => Relation a a

iden matrix

iden . r == r == r . iden

comp :: Relation b c -> Relation a b -> Relation a c

Relational composition

r . (s . p) = (r . s) . p

fromF :: (Liftable a b, CountableDimsN a b, FLN b a) => (a -> b) -> Relation a b

Lifts functions to matrices with dimensions matching a and b cardinality's.

fromF' :: (Liftable a b, CountableDimsN c d, FLN d c) => (a -> b) -> Relation c d

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.

Relational application

pointAp :: (Liftable a b, Eq a, CountableDimsN a b, FLN a One, FLN b One) => a -> b -> Relation a b -> Relation One One

Relational application.

If a and b are related by Relation r then pointAp a b r == one (nat 1)

pointApBool :: (Liftable a b, Eq a, CountableDimsN a b, FLN a One, FLN b One) => a -> b -> Relation a b -> Bool

Relational application

The same as pointAp but converts Boolean to Bool

Matrix printing

pretty :: CountableDimsN a b => Relation a b -> String

Relation pretty printing

prettyPrint :: CountableDimsN a b => Relation a b -> IO ()

Relation pretty printing