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 isn't possible to implement the id function so it's implementation is undefined. However comp can be and this partial class implementation exists just to make the code more readable.

Please use identity instead.

Defined in LAoP.Relation.Internal

Methods

id :: 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 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 CountableDimensions a b = (Countable a, Countable b)

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

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

type FromListsN a b = FromLists Boolean (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 TrivialE a b = Normalize (Either a b) ~ Either (Normalize a) (Normalize b)

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

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

Primitives

empty :: Relation Zero Zero

Empty matrix constructor

one :: Boolean -> Relation One One

Unit matrix constructor

junc :: TrivialE a b => Relation a c -> Relation b c -> Relation (Either a b) c

Boolean Matrix Junc constructor, also known as relational coproduct.

See eitherR.

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

Boolean Matrix Junc constructor

See eitherR.

split :: TrivialE a b => Relation c a -> Relation c b -> Relation c (Either a b)

Boolean Matrix Split constructor, also known as relational product.

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

Boolean Matrix Split 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 0 = Void

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 d = FromNat (Count d)

Matrix construction and conversion

class FromLists e 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 bery much like an inductive definition but on types.

Minimal complete definition

fromLists

Instances

FromLists e () ()

Defined in LAoP.Matrix.Internal

Methods

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

FromLists e Void Void

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e Void Void

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

fromLists :: FromListsN 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, CountableDimensionsN c d, FromListsN 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.

fromF' :: (Liftable a b, CountableDimensionsN a b, FromListsN b a) => (a -> b) -> Relation a b

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

toRel :: (Liftable a b, CountableDimensionsN a b, FromListsN 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, CountableDimensionsN a b, FromListsN a One, FromListsN 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, CountableDimensionsN (List a) a, FromListsN a (List a)) => Relation (List a) a

Belongs relation

relationBuilder :: (FromListsN a b, CountableDimensionsN a b) => ((Int, Int) -> Boolean) -> Relation a b

Matrix builder function. Constructs a matrix provided with a construction function.

zeros :: (FromListsN a b, CountableDimensionsN 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 or empty Relation.

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

ones :: (FromListsN a b, CountableDimensionsN 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 :: (FromListsN a One, CountableN a) => Relation a One

The T (Top) row vector relation.

point :: (Bounded a, Enum a, Eq a, CountableN a, FromListsN 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 conjunction.

(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 disjunction.

(r `union` s) `union` t == r `union (s `union` t)
r `union` s `sse` x == r `sse` x && s `sse` x
r `comp` (s `union` t) == (r `comp` s) `union` (r `comp` t)
(s `union` t) `comp` r ==  (s `comp` r) `union` (t `comp` 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 `comp` r
ker r == img (conv r)

img :: Relation a b -> Relation b b

Relation Image

img r == r `comp` conv r
img r == ker (conv r)

Taxonomy of binary relations

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

A Relation r is injective iff coreflexive (ker r)

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

A Relation r is entire iff reflexive (ker r)

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

A Relation r is simple iff coreflexive (img r)

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

A Relation r is surjective iff reflexive (img r)

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

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

function :: (CountableDimensionsN a b, FromListsN a a, FromListsN 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 `comp` r `sse` s == r `sse` f `comp` s
r `comp` f `sse` s == r `sse` s `comp` f

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

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

injection :: (CountableDimensionsN a b, FromListsN a a, FromListsN b b) => Relation a b -> Bool

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

surjection :: (CountableDimensionsN a b, FromListsN a a, FromListsN b b) => Relation a b -> Bool

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

bijection :: (CountableDimensionsN a b, FromListsN b b, FromListsN a a) => Relation a b -> Bool

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

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

Relational domain.

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

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

Relational range.

For functions, range and img (image) coincide, since img f `sse` identity 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 `comp` 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 :: (FromListsN 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 :: (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)

Relational pairing.

NOTE: That this is not a true categorical product, see for instance:

               | p1 `comp` splitR a b `sse` a 
splitR a b =   |
               | p2 `comp` splitR a b `sse` b

Emphasis on the sse.

splitR r s `comp` f == splitR (r `comp` f) (s `comp` f)
(R >< S) `comp` splitR p q == splitR (r `comp` p) (s `comp` q)
conv (splitR r s) `comp` splitR x y == (conv r `comp` x) `intersection` (conv s `comp` y)

eitherR (splitR r s) (splitR t v) == splitR (eitherR r t) (eitherR s v)

Projections

p1 :: forall a b. (CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) a, TrivialP a b) => Relation (a, b) a

Relational pairing first component projection

p1 `comp` splitR r s `sse` r

p2 :: forall a b. (CountableDimensionsN a b, CountableN (a, b), FromListsN (a, b) b, TrivialP a b) => Relation (a, b) b

Relational pairing second component projection

p2 `comp` splitR r s `sse` s

Bifunctor

(><) :: (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) infixl 4

Relational pairing functor

r >< s == splitR (r `comp` p1) (s `comp` p2)
(r >< s) `comp` (p >< q) == (r `comp` p) >< (s `comp` q)

Relational coproduct

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

Relational coproduct.

               | eitherR a b `comp` i1 == a
eitherR a b =  |
               | eitherR a b `comp` i2 == b

eitherR r s `comp` conv (eitherR t u) == (r `comp` conv t) `union` (s `comp` conv u)

eitherR (splitR r s) (splitR t v) == splitR (eitherR r t) (eitherR s v)

Injections

i1 :: (CountableDimensionsN a b, FromListsN b a, FromListsN a a, TrivialE a b) => Relation a (Either a b)

Relational coproduct first component injection

img i1 `union` img i2 == identity
i1 `comp` i2 = zeros

i2 :: (CountableDimensionsN a b, FromListsN a b, FromListsN b b, TrivialE a b) => Relation b (Either a b)

Relational coproduct second component injection

img i1 `union` img i2 == identity
i1 `comp` i2 = zeros

Bifunctor

(-|-) :: (CountableDimensionsN b d, FromListsN b b, FromListsN d b, FromListsN b d, FromListsN d d, TrivialE a c, TrivialE b d) => Relation a b -> Relation c d -> Relation (Either a c) (Either b d) infixl 5

Relational coproduct functor.

r -|- s == eitherR (i1 `comp` r) (i2 `comp` s)

Relational "currying"

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), TrivialP2 a b, TrivialP2 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 :: (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), TrivialP2 a b, TrivialP2 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, FromListsN a a) => Relation a a -> Bool

A Relation r is reflexive iff identity `sse` r

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

A Relation r is coreflexive iff r `sse` identity

transitive :: Relation a a -> Bool

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

symmetric :: Relation a a -> Bool

A Relation r is symmetric iff r == conv r

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

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

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

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

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

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

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

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

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

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

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

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

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

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

partialEquivalence :: (CountableN a, FromListsN 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 `comp` conv r `comp` r == r

Conditionals

equalizer :: (CountableN a, FromListsN 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 == identity
equalizer (point True) (point False) == zeros

McCarthy's Conditional

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

Transforms predicate p into a correflexive relation.

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

predR q `comp` predR p == predR q `union` predR p

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

Relational conditional guard.

guard p = i2 `overriddenBy` i1 `comp` predR p

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

Relational McCarthy's conditional.

Relational composition and lifting

identity :: (FromListsN a a, CountableN a) => Relation a a

Identity matrix

identity `comp` r == r == r `comp` identity

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

Relational composition

r `comp` (s `comp` p) = (r `comp` s) `comp` p

fromF :: (Liftable a b, CountableDimensionsN c d, FromListsN 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.

fromF' :: (Liftable a b, CountableDimensionsN a b, FromListsN b a) => (a -> b) -> Relation a b

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

Relational application

pointAp :: (Liftable a b, Eq a, CountableDimensionsN a b, FromListsN a One, FromListsN 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, CountableDimensionsN a b, FromListsN a One, FromListsN b One) => a -> b -> Relation a b -> Bool

Relational application

The same as pointAp but converts Boolean to Bool

Matrix printing

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

Relation pretty printing

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

Relation pretty printing