laop-0.1.0.5

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

Instance details

Defined in LAoP.Relation.Internal

Methods

id :: Relation a a #

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

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

empty :: Relation Zero Zero Source #

Empty matrix constructor

one :: Boolean -> Relation One One Source #

Unit matrix constructor

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

Boolean Matrix Junc constructor, also known as relational coproduct.

See eitherR.

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

Boolean Matrix Junc constructor

See eitherR.

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

Boolean Matrix Split constructor, also known as relational product.

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

Boolean Matrix Split 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 0 = Void 
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 e 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 e () () Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

FromLists e Void Void Source # 
Instance details

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

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

Defined in LAoP.Matrix.Internal

Methods

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

(FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (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 :: FromListsN 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, CountableDimensionsN c d, FromListsN 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, CountableDimensionsN a b, FromListsN b a) => (a -> b) -> Relation a b Source #

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 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, CountableDimensionsN a b, FromListsN a One, FromListsN 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, CountableDimensionsN (List a) a, FromListsN a (List a)) => Relation (List a) a Source #

Belongs relation

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

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

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

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

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

The T (Top) row vector relation.

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

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 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 `comp` r
ker r == img (conv r)

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

Relation Image

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

Taxonomy of binary relations

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

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

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

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 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 `comp` 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 :: (FromListsN 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 :: (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) Source #

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

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

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

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 :: Relation a c -> Relation b c -> Relation (Either a b) c Source #

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

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

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) => Relation a b -> Relation c d -> Relation (Either a c) (Either b d) infixl 5 Source #

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

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

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

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

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

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

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

Conditionals

equalizer :: (CountableN a, FromListsN 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 == 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 Source #

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) => Relation b Bool -> Relation b (Either b b) Source #

Relational conditional guard.

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

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

Relational McCarthy's conditional.

Relational composition and lifting

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

Identity matrix

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

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

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 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, CountableDimensionsN a b, FromListsN 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, CountableDimensionsN a b, FromListsN a One, FromListsN 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, CountableDimensionsN a b, FromListsN a One, FromListsN b One) => a -> b -> Relation a b -> Bool Source #

Relational application

The same as pointAp but converts Boolean to Bool

Matrix printing

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

Relation pretty printing

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

Relation pretty printing