laop-0.1.1.0: Matrix programming library

Copyright(c) Armando Santos 2019-2020
Maintainerarmandoifsantos@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

LAoP.Relation.Internal

Contents

Description

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.

Synopsis

Documentation

This definition makes use of the fact that Void is isomorphic to 0 and One 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 Source #

Relation data type.

Constructors

R (Matrix Boolean (Normalize a) (Normalize b)) 
Instances
Category Relation Source #

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

Instance details

Defined in LAoP.Relation.Internal

Associated Types

type Object Relation o :: Constraint Source #

Methods

id :: Object Relation a => Relation a a Source #

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

Eq (Relation a b) Source # 
Instance details

Defined in LAoP.Relation.Internal

Methods

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

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

Num (Relation a b) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in LAoP.Relation.Internal

Show (Relation a b) Source # 
Instance details

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) Source # 
Instance details

Defined in LAoP.Relation.Internal

Methods

rnf :: Relation a b -> () #

type Object Relation a Source # 
Instance details

Defined in LAoP.Relation.Internal

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

type Boolean = Natural 0 1 Source #

Boolean type synonym for working with boolean matrices

Constraint type synonyms

type Countable a = KnownNat (Count a) Source #

Constraint type synonyms to keep the type signatures less convoluted

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

Primitives

one :: Boolean -> Relation One One Source #

Unit matrix constructor

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

Boolean Matrix Join constructor, also known as relational coproduct.

See eitherR.

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

Boolean Matrix Join constructor

See eitherR.

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

Boolean Matrix Fork constructor, also known as relational product.

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

Boolean Matrix Fork constructor

Auxiliary type families

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

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 ... Source #

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 ... Source #

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 Source #

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 () () Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

FromLists () rows => FromLists () (Either () rows) Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

(FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

FromLists cols () => FromLists (Either () cols) () Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

(FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

(FromLists (Either a b) c, FromLists (Either a b) d, Countable c) => FromLists (Either a b) (Either c d) Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

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

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 c d, FLN d c) => (a -> b) -> Relation c d Source #

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, CountableDimsN a b, FLN b a) => (a -> b) -> Relation a b Source #

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

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

Lifts relation functions to Relation

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

Converts a matrix to a list of lists of elements.

toList :: Relation a b -> [Boolean] Source #

Converts a matrix to a list of elements.

toBool :: Relation One One -> Bool Source #

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 Source #

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 Source #

Belongs relation

relationBuilder' :: (FLN a b, CountableDimsN a b) => ((Int, Int) -> Boolean) -> Relation a b Source #

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

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

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 Source #

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 Source #

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 Source #

The T (Top) row vector relation.

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

Point constant relation

Relational operations

conv :: Relation a b -> Relation b a Source #

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 Source #

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 Source #

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 Source #

Relational inclusion (subset or equal)

implies :: Relation a b -> Relation a b -> Relation a b Source #

Relational implication (the same as sse)

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

Relational bi-implication

ker :: Relation a b -> Relation a a Source #

Relation Kernel

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

img :: Relation a b -> Relation b b Source #

Relation Image

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

Taxonomy of binary relations

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

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

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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) Source #

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 Source #

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 Source #

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 Source #

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 Source #

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) Source #

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) Source #

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 Source #

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) Source #

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 Source #

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

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

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

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

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

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

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

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

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

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

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

difunctional :: Relation a b -> Bool Source #

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 Source #

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 Source #

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) Source #

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 Source #

Relational McCarthy's conditional.

Relational composition and lifting

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

iden matrix

iden . r == r == r . iden

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

Relational composition

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

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

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, CountableDimsN a b, FLN b a) => (a -> b) -> Relation a b Source #

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

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 Source #

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 Source #

Relational application

The same as pointAp but converts Boolean to Bool

Matrix printing

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

Relation pretty printing

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

Relation pretty printing