@@ -1,6 +1,7 @@
11{-# LANGUAGE GADTs #-}
22{-# LANGUAGE UndecidableInstances #-}
33{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE TypeApplications #-}
45{-# LANGUAGE ScopedTypeVariables #-}
56{-# LANGUAGE StandaloneDeriving #-}
67{-# LANGUAGE DerivingVia #-}
@@ -42,7 +43,9 @@ module LAoP.Relation.Internal
4243 empty,
4344 one,
4445 junc,
46+ (|||),
4547 split,
48+ (===),
4649
4750 -- * Auxiliary type families
4851 I.FromNat,
@@ -57,7 +60,7 @@ module LAoP.Relation.Internal
5760 toRel,
5861 toLists,
5962 toList,
60− matrixBuilder,
63+ relationBuilder,
6164 zeros,
6265 ones,
6366 bang,
@@ -71,11 +74,34 @@ module LAoP.Relation.Internal
7174 img,
7275
7376 -- * Taxonomy of binary relations
74− entire,
7577 injective,
76− surjective,
78+ entire,
7779 simple,
78− bijective,
80+ surjective,
81+ representation,
82+ function,
83+ abstraction,
84+ injection,
85+ surjection,
86+ bijection,
87+
88+ -- * Function division
89+ divisionF,
90+
91+ -- * Relational pairing
92+ splitR,
93+ -- ** Projections
94+ p1,
95+ p2,
96+ -- ** Bifunctor
97+ (><),
98+ -- * Relational coproduct
99+ eitherR,
100+ -- ** Injections
101+ i1,
102+ i2,
103+ -- ** Bifunctor
104+ (-|-),
79105
80106 -- * (Endo-)Relational properties
81107 reflexive,
@@ -111,7 +137,6 @@ import qualified LAoP.Matrix.Internal as I
111137import LAoP.Utils
112138import Control.DeepSeq
113139import qualified Control.Category as C
114−import Data.Coerce
115140import Data.Bool
116141import GHC.TypeLits
117142
@@ -157,7 +182,9 @@ empty = R I.Empty
157182one :: Boolean -> Relation One One
158183one = R . I.One
159184
160−-- | Boolean Matrix 'Junc' constructor
185+-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
186+--
187+-- See 'eitherR'.
161188junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
162189 => Relation a c -> Relation b c -> Relation (Either a b) c
163190junc (R a) (R b) = R (I.Junc a b)
@@ -171,7 +198,7 @@ infixl 3 |||
171198 Relation (Either a b) c
172199(|||) = junc
173200
174−-- | Boolean Matrix 'Split' constructor
201+-- | Boolean Matrix 'Split' constructor, also known as relational product.
175202split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
176203 => Relation c a -> Relation c b -> Relation c (Either a b)
177204split (R a) (R b) = R (I.Split a b)
@@ -194,11 +221,11 @@ fromLists = R . I.fromLists
194221
195222-- | Matrix builder function. Constructs a matrix provided with
196223-- a construction function.
197−matrixBuilder ::
224+relationBuilder ::
198225 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
199226 ((Int, Int) -> Boolean) ->
200227 Relation a b
201−matrixBuilder = R . I.matrixBuilder
228+relationBuilder = R . I.matrixBuilder
202229
203230-- | Lifts functions to matrices with arbitrary dimensions.
204231--
@@ -262,7 +289,7 @@ toList (R m) = I.toList m
262289zeros ::
263290 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
264291 Relation a b
265−zeros = matrixBuilder (const (nat 0))
292+zeros = relationBuilder (const (nat 0))
266293
267294-- Ones Matrix
268295
@@ -272,13 +299,13 @@ zeros = matrixBuilder (const (nat 0))
272299ones ::
273300 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
274301 Relation a b
275−ones = matrixBuilder (const (nat 1))
302+ones = relationBuilder (const (nat 1))
276303
277304-- Bang Matrix
278305
279306-- | The T (Top) row vector matrix.
280307bang ::
281− forall e a.
308+ forall a.
282309 (I.FromLists Boolean (I.Normalize a) (), KnownNat (I.Count (I.Normalize a))) =>
283310 Relation a One
284311bang = ones
@@ -289,7 +316,7 @@ bang = ones
289316identity ::
290317 (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
291318 Relation a a
292−identity = matrixBuilder (bool (nat 0) (nat 1) . uncurry (==))
319+identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
293320
294321-- | Relational composition
295322comp :: forall a b c . Relation b c -> Relation a b -> Relation a c
@@ -305,15 +332,15 @@ sse a b = a <= b
305332
306333-- | Relational intersection
307334--
308−-- @M `inter` N = M * N@
335+-- Lifts pointwise conjunction.
309336intersection :: Relation a b -> Relation a b -> Relation a b
310337intersection a b = a * b
311338
312339-- | Relational union
313340--
314−-- @M `union` N = M + N - M * N
341+-- Lifts pointwise disjunction.
315342union :: Relation a b -> Relation a b -> Relation a b
316−union a b = a + b - a * b
343+union a b = a + b
317344
318345-- | Relation Kernel
319346ker :: Relation a b -> Relation a a
@@ -323,15 +350,16 @@ ker r = conv r `comp` r
323350img :: Relation a b -> Relation b b
324351img r = r `comp` conv r
325352
326−-- | Properties of relations
327−
328−-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
329−reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
330−reflexive r = identity <= r
353+-- | Function division.
354+--
355+-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
356+-- 'entire'.
357+--
358+-- @division f g == conv g `'comp'` f@
359+divisionF :: Relation a c -> Relation b c -> Relation a b
360+divisionF f g = conv g `comp` f
331361
332−-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
333−coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
334−coreflexive r = r <= identity
362+-- Taxonomy of binary relations
335363
336364-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@
337365simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
@@ -349,14 +377,79 @@ entire = reflexive . ker
349377surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
350378surjective = reflexive . img
351379
352−-- | A 'Relation' @r@ is bijective iff @'injective' r && 'surjective' r@
353−bijective ::
380+-- | A 'Relation' @r@ is a function iff @'simple' r && 'entire' r@
381+--
382+-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
383+-- relations:
384+--
385+-- @
386+-- f `'comp'` r `'sse'` s == r `'sse'` f `'comp'` s
387+-- r `'comp'` f `'sse'` s == r `'sse'` s `'comp'` f
388+-- @
389+function ::
390+ ( KnownNat (I.Count (I.Normalize b)),
391+ KnownNat (I.Count (I.Normalize a)),
392+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
393+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
394+ )
395+ => Relation a b -> Bool
396+function r = simple r && entire r
397+
398+-- | A 'Relation' @r@ is a representation iff @'injective' r && 'entire' r@
399+representation ::
400+ ( KnownNat (I.Count (I.Normalize a)),
401+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
402+ )
403+ => Relation a b -> Bool
404+representation r = injective r && entire r
405+
406+-- | A 'Relation' @r@ is an abstraction iff @'surjective' r && 'simple' r@
407+abstraction ::
408+ ( KnownNat (I.Count (I.Normalize b)),
409+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
410+ )
411+ => Relation a b -> Bool
412+abstraction r = surjective r && simple r
413+
414+-- | A 'Relation' @r@ is a surjection iff @'function' r && 'abstraction' r@
415+surjection ::
416+ ( KnownNat (I.Count (I.Normalize b)),
417+ KnownNat (I.Count (I.Normalize a)),
418+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
419+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
420+ )
421+ => Relation a b -> Bool
422+surjection r = function r && abstraction r
423+
424+-- | A 'Relation' @r@ is a injection iff @'function' r && 'representation' r@
425+injection ::
426+ ( KnownNat (I.Count (I.Normalize b)),
427+ KnownNat (I.Count (I.Normalize a)),
428+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
429+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
430+ )
431+ => Relation a b -> Bool
432+injection r = function r && representation r
433+
434+-- | A 'Relation' @r@ is an bijection iff @'injection' r && 'surjection' r@
435+bijection ::
354436 ( KnownNat (I.Count (I.Normalize b)),
355437 KnownNat (I.Count (I.Normalize a)),
356438 I.FromLists Boolean (I.Normalize b) (I.Normalize b),
357439 I.FromLists Boolean (I.Normalize a) (I.Normalize a)
358440 ) => Relation a b -> Bool
359−bijective r = injective r && surjective r
441+bijection r = injection r && surjection r
442+
443+
444+-- Properties of relations
445+
446+-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
447+reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
448+reflexive r = identity <= r
449+
450+-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
451+coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
452+coreflexive r = r <= identity
360453
361454-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
362455transitive :: Relation a a -> Bool
@@ -398,6 +491,121 @@ equivalence r = symmetric r && preorder r
398491partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
399492partialEquivalence r = partialOrder r && equivalence r
400493
494+-- Relational pairing
495+
496+-- | Relational pairing.
497+--
498+-- NOTE: That this is not a true categorical product, see for instance:
499+--
500+-- @
501+-- | 'p1' `'comp'` 'splitR' a b `'sse'` a
502+-- 'splitR' a b <=> |
503+-- | 'p2' `'comp'` 'splitR' a b `'sse'` b
504+-- @
505+--
506+-- __Emphasis__ on the 'sse'.
507+splitR ::
508+ ( KnownNat (I.Count (I.Normalize a)),
509+ KnownNat (I.Count (I.Normalize b)),
510+ KnownNat (I.Count (I.Normalize (a, b))),
511+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
512+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
513+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
514+ )
515+ => Relation c a -> Relation c b -> Relation c (a, b)
516+splitR (R f) (R g) = R (I.khatri f g)
517+
518+-- | Relational pairing first component projection
519+p1 ::
520+ forall a b .
521+ ( KnownNat (I.Count (I.Normalize a)),
522+ KnownNat (I.Count (I.Normalize b)),
523+ KnownNat (I.Count (I.Normalize (a, b))),
524+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
525+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
526+ )
527+ => Relation (a, b) a
528+p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
529+
530+-- | Relational pairing second component projection
531+p2 ::
532+ forall a b .
533+ ( KnownNat (I.Count (I.Normalize b)),
534+ KnownNat (I.Count (I.Normalize a)),
535+ KnownNat (I.Count (I.Normalize (a, b))),
536+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
537+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
538+ )
539+ => Relation (a, b) b
540+p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
541+
542+-- Relational pairing functor
543+
544+infixl 4 ><
545+-- | Relational pairing functor
546+(><) ::
547+ ( KnownNat (I.Count (I.Normalize a)),
548+ KnownNat (I.Count (I.Normalize b)),
549+ KnownNat (I.Count (I.Normalize c)),
550+ KnownNat (I.Count (I.Normalize d)),
551+ KnownNat (I.Count (I.Normalize (a, c))),
552+ KnownNat (I.Count (I.Normalize (b, d))),
553+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),
554+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),
555+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),
556+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize d),
557+ I.Normalize (a, c) ~ I.Normalize (I.Normalize a, I.Normalize c),
558+ I.Normalize (b, d) ~ I.Normalize (I.Normalize b, I.Normalize d)
559+ )
560+ => Relation a b -> Relation c d -> Relation (a, c) (b, d)
561+(><) (R a) (R b) = R ((I.><) a b)
562+
563+-- Relational co-products
564+
565+-- | Relational coproduct.
566+eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
567+ => Relation a c -> Relation b c -> Relation (Either a b) c
568+eitherR = junc
569+
570+-- | Relational coproduct first component injection
571+i1 ::
572+ ( KnownNat (I.Count (I.Normalize b)),
573+ KnownNat (I.Count (I.Normalize a)),
574+ I.FromLists Boolean (I.Normalize b) (I.Normalize a),
575+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
576+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
577+ )
578+ => Relation a (Either a b)
579+i1 = R I.i1
580+
581+-- | Relational coproduct second component injection
582+i2 ::
583+ ( KnownNat (I.Count (I.Normalize b)),
584+ KnownNat (I.Count (I.Normalize a)),
585+ I.FromLists Boolean (I.Normalize a) (I.Normalize b),
586+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
587+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
588+ )
589+ => Relation b (Either a b)
590+i2 = R I.i2
591+
592+infixl 5 -|-
593+
594+-- | Relational coproduct functor.
595+(-|-) ::
596+ ( KnownNat (I.Count (I.Normalize d)),
597+ KnownNat (I.Count (I.Normalize b)),
598+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
599+ I.FromLists Boolean (I.Normalize d) (I.Normalize b),
600+ I.FromLists Boolean (I.Normalize b) (I.Normalize d),
601+ I.FromLists Boolean (I.Normalize d) (I.Normalize d),
602+ I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),
603+ I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)
604+ )
605+ => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
606+(-|-) (R a) (R b) = R ((I.-|-) a b)
607+
608+
401609-- Relation pretty print
402610
403611-- | Relation pretty printing