@@ -0,0 +1,1042 @@
1+{-# LANGUAGE GADTs #-}
2+{-# LANGUAGE UndecidableInstances #-}
3+{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE TypeApplications #-}
5+{-# LANGUAGE ScopedTypeVariables #-}
6+{-# LANGUAGE StandaloneDeriving #-}
7+{-# LANGUAGE DerivingVia #-}
8+{-# LANGUAGE DataKinds #-}
9+
10+-----------------------------------------------------------------------------
11+-- |
12+-- Module : LAoP.Relation.Internal
13+-- Copyright : (c) Armando Santos 2019-2020
14+-- Maintainer : armandoifsantos@gmail.com
15+-- Stability : experimental
16+--
17+-- The AoP discipline generalises functions to relations which are
18+-- Boolean matrices.
19+--
20+-- This module offers many of the combinators of the Algebra of
21+-- Programming discipline. It is still under construction and very
22+-- experimental.
23+--
24+-- This is an Internal module and it is no supposed to be imported.
25+--
26+-----------------------------------------------------------------------------
27+
28+module LAoP.Relation.Internal
29+ ( -- | This definition makes use of the fact that 'Void' is
30+ -- isomorphic to 0 and 'One' to 1 and captures matrix
31+ -- dimensions as stacks of 'Either's.
32+ --
33+ -- There exists two type families that make it easier to write
34+ -- matrix dimensions: 'FromNat' and 'Count'. This approach
35+ -- leads to a very straightforward implementation
36+ -- of LAoP combinators.
37+
38+ -- * Relation data type
39+ Relation (..),
40+ Boolean,
41+
42+ -- * Primitives
43+ empty,
44+ one,
45+ junc,
46+ (|||),
47+ split,
48+ (===),
49+
50+ -- * Auxiliary type families
51+ I.FromNat,
52+ I.Count,
53+ I.Normalize,
54+
55+ -- * Matrix construction and conversion
56+ I.FromLists,
57+ fromLists,
58+ fromF,
59+ fromF',
60+ toRel,
61+ toLists,
62+ toList,
63+ toBool,
64+ pt,
65+ belongs,
66+ relationBuilder,
67+ zeros,
68+ ones,
69+ bang,
70+ point,
71+
72+ -- * Relational operations
73+ conv,
74+ intersection,
75+ union,
76+ sse,
77+ implies,
78+ iff,
79+ ker,
80+ img,
81+
82+ -- * Taxonomy of binary relations
83+ injective,
84+ entire,
85+ simple,
86+ surjective,
87+ representation,
88+ function,
89+ abstraction,
90+ injection,
91+ surjection,
92+ bijection,
93+ domain,
94+ range,
95+
96+ -- * Function division
97+ divisionF,
98+
99+ -- * Relation division
100+ divR,
101+ divL,
102+ divS,
103+ shrunkBy,
104+ overriddenBy,
105+
106+ -- * Relational pairing
107+ splitR,
108+
109+ -- ** Projections
110+ p1,
111+ p2,
112+ -- ** Bifunctor
113+ (><),
114+ -- * Relational coproduct
115+ eitherR,
116+ -- ** Injections
117+ i1,
118+ i2,
119+ -- ** Bifunctor
120+ (-|-),
121+
122+ -- * Relational "currying"
123+ trans,
124+ untrans,
125+
126+ -- * (Endo-)Relational properties
127+ reflexive,
128+ coreflexive,
129+ transitive,
130+ symmetric,
131+ antiSymmetric,
132+ irreflexive,
133+ connected,
134+ preorder,
135+ partialOrder,
136+ linearOrder,
137+ equivalence,
138+ partialEquivalence,
139+ difunctional,
140+
141+ -- * Conditionals
142+ equalizer,
143+
144+ -- ** McCarthy's Conditional
145+ predR,
146+ guard,
147+ cond,
148+
149+ -- * Relational composition and lifting
150+ identity,
151+ comp,
152+ fromF,
153+ fromF',
154+
155+ -- ** Relational application
156+ pointAp,
157+ pointApBool,
158+
159+ -- * Matrix printing
160+ pretty,
161+ prettyPrint
162+ )
163+ where
164+
165+import Data.Void
166+import qualified LAoP.Matrix.Internal as I
167+import LAoP.Utils.Internal
168+import Control.DeepSeq
169+import qualified Control.Category as C
170+import Data.Bool
171+import GHC.TypeLits
172+
173+-- | Boolean type synonym for working with boolean matrices
174+type Boolean = Natural 0 1
175+
176+-- | Relation data type.
177+newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
178+ deriving (Show, Eq, Ord, NFData) via (I.Matrix (Natural 1 1) (I.Normalize a) (I.Normalize b))
179+
180+deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
181+
182+-- | It isn't possible to implement the 'id' function so it's
183+-- implementation is 'undefined'. However 'comp' can be and this partial
184+-- class implementation exists just to make the code more readable.
185+--
186+-- Please use 'identity' instead.
187+instance C.Category Relation where
188+ id = undefined
189+ (.) = comp
190+
191+instance Num (Relation a b) where
192+ -- | Matrix addition becomes Boolean matrix disjunction
193+ (R a) + (R b) = R (I.orM a b)
194+
195+ -- | Matrix subtraction becomes Relational subtraction
196+ (R a) - (R b) = R (I.subM a b)
197+
198+ -- | Matrix multiplication becomes Boolean matrix conjunction
199+ (R a) * (R b) = R (I.andM a b)
200+
201+ -- | Matrix negation becomes Boolean matrix negation
202+ negate (R a) = R (I.negateM a)
203+
204+-- Type alias
205+type Zero = Void
206+type One = ()
207+
208+-- Primitives
209+
210+-- | Empty matrix constructor
211+empty :: Relation Zero Zero
212+empty = R I.Empty
213+
214+-- | Unit matrix constructor
215+one :: Boolean -> Relation One One
216+one = R . I.One
217+
218+-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
219+--
220+-- See 'eitherR'.
221+junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
222+ => Relation a c -> Relation b c -> Relation (Either a b) c
223+junc (R a) (R b) = R (I.Junc a b)
224+
225+infixl 3 |||
226+-- | Boolean Matrix 'Junc' constructor
227+--
228+-- See 'eitherR'.
229+(|||) ::
230+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
231+ Relation a c ->
232+ Relation b c ->
233+ Relation (Either a b) c
234+(|||) = junc
235+
236+-- | Boolean Matrix 'Split' constructor, also known as relational product.
237+split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
238+ => Relation c a -> Relation c b -> Relation c (Either a b)
239+split (R a) (R b) = R (I.Split a b)
240+
241+infixl 2 ===
242+-- | Boolean Matrix 'Split' constructor
243+(===) ::
244+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
245+ Relation c a ->
246+ Relation c b ->
247+ Relation c (Either a b)
248+(===) = split
249+
250+-- Construction
251+
252+-- | Build a matrix out of a list of list of elements. Throws a runtime
253+-- error if the dimensions do not match.
254+fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
255+fromLists = R . I.fromLists
256+
257+-- | Matrix builder function. Constructs a matrix provided with
258+-- a construction function.
259+relationBuilder ::
260+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
261+ ((Int, Int) -> Boolean) ->
262+ Relation a b
263+relationBuilder = R . I.matrixBuilder
264+
265+-- | Lifts functions to matrices with arbitrary dimensions.
266+--
267+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
268+-- types @a@ or @b@ allows.
269+fromF ::
270+ ( Bounded a,
271+ Bounded b,
272+ Enum a,
273+ Enum b,
274+ Eq b,
275+ KnownNat (I.Count (I.Normalize c)),
276+ KnownNat (I.Count (I.Normalize d)),
277+ I.FromLists Boolean (I.Normalize d) (I.Normalize c)
278+ )
279+ => (a -> b) -> Relation c d
280+fromF f = R (I.fromFRel f)
281+
282+-- | Lifts functions to matrices with dimensions matching @a@ and @b@
283+-- cardinality's.
284+fromF' ::
285+ ( Bounded b,
286+ Bounded a,
287+ Enum a,
288+ Enum b,
289+ Eq b,
290+ KnownNat (I.Count (I.Normalize a)),
291+ KnownNat (I.Count (I.Normalize b)),
292+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)
293+ )
294+ => (a -> b) -> Relation a b
295+fromF' f = R (I.fromFRel' f)
296+
297+-- | Lifts relation functions to 'Relation'
298+toRel ::
299+ ( Bounded b,
300+ Bounded a,
301+ Enum a,
302+ Enum b,
303+ Eq b,
304+ KnownNat (I.Count (I.Normalize a)),
305+ KnownNat (I.Count (I.Normalize b)),
306+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)
307+ )
308+ => (a -> b -> Bool) -> Relation a b
309+toRel = R . I.toRel
310+
311+-- | Lowers a 'Relation' to a function
312+fromRel ::
313+ ( Bounded a,
314+ Bounded b,
315+ Enum a,
316+ Enum b,
317+ Eq a,
318+ Eq b,
319+ KnownNat (I.Count (I.Normalize a)),
320+ KnownNat (I.Count (I.Normalize b)),
321+ I.FromLists Boolean (I.Normalize a) One,
322+ I.FromLists Boolean (I.Normalize b) One
323+ )
324+ => Relation a b -> (a -> b -> Bool)
325+fromRel r a b = pointApBool a b r
326+
327+-- Conversion
328+
329+-- | Converts a matrix to a list of lists of elements.
330+toLists :: Relation a b -> [[Boolean]]
331+toLists (R m) = I.toLists m
332+
333+-- | Converts a matrix to a list of elements.
334+toList :: Relation a b -> [Boolean]
335+toList (R m) = I.toList m
336+
337+-- | Converts a well typed 'Relation' to 'Bool'.
338+toBool :: Relation One One -> Bool
339+toBool r = case toList r of
340+ [Nat 0] -> False
341+ _ -> True
342+
343+-- | Power transpose.
344+--
345+-- Maps a relation to a set valued function.
346+pt ::
347+ ( Bounded a,
348+ Bounded b,
349+ Enum a,
350+ Enum b,
351+ Eq a,
352+ Eq b,
353+ KnownNat (I.Count (I.Normalize a)),
354+ KnownNat (I.Count (I.Normalize b)),
355+ I.FromLists Boolean (I.Normalize a) One,
356+ I.FromLists Boolean (I.Normalize b) One
357+ )
358+ => Relation a b -> (a -> Powerset b)
359+pt r a =
360+ let (PS lb) = maxBound
361+ in PS [ b | b <- lb, toBool (pointAp a b r) ]
362+
363+-- | Belongs relation
364+belongs ::
365+ ( Bounded a,
366+ Enum a,
367+ Eq a,
368+ KnownNat (I.Count (I.Normalize (Powerset a))),
369+ KnownNat (I.Count (I.Normalize a)),
370+ I.FromLists Boolean (I.Normalize a) (I.Normalize (Powerset a))
371+ )
372+ => Relation (Powerset a) a
373+belongs = toRel (flip elemR)
374+ where
375+ elemR x (PS l) = x `elem` l
376+
377+-- Zeros Matrix
378+
379+-- | The zero relation. A relation where no element of type @a@ relates
380+-- with elements of type @b@.
381+--
382+-- Also known as ⊥ (Bottom) Relation or empty Relation.
383+--
384+-- @
385+-- r ``comp`` ⊥ == ⊥ ``comp`` r == ⊥
386+-- ⊥ ``sse`` R && R ``sse`` T == True
387+-- @
388+zeros ::
389+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
390+ Relation a b
391+zeros = relationBuilder (const (nat 0))
392+
393+-- Ones Matrix
394+
395+-- | The ones relation. A relation where every element of type @a@ relates
396+-- with every element of type @b@.
397+--
398+-- Also known as T (Top) Relation or universal Relation.
399+--
400+-- @
401+-- ⊥ ``sse`` R && R ``sse`` T == True
402+-- @
403+ones ::
404+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
405+ Relation a b
406+ones = relationBuilder (const (nat 1))
407+
408+-- Bang Matrix
409+
410+-- | The T (Top) row vector relation.
411+bang ::
412+ (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
413+ Relation a One
414+bang = ones
415+
416+-- | Point constant relation
417+point ::
418+ ( Bounded a,
419+ Enum a,
420+ Eq a,
421+ KnownNat (I.Count (I.Normalize a)),
422+ I.FromLists Boolean (I.Normalize a) One
423+ ) => a -> Relation One a
424+point = fromF' . const
425+
426+-- Identity Matrix
427+
428+-- | Identity matrix
429+--
430+-- @
431+-- 'identity' ``comp`` r == r == r ``comp`` 'identity'
432+-- @
433+identity ::
434+ (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
435+ Relation a a
436+identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
437+
438+-- | Relational composition
439+--
440+-- @
441+-- r ``comp`` (s ``comp`` p) = (r ``comp`` s) ``comp`` p
442+-- @
443+comp :: Relation b c -> Relation a b -> Relation a c
444+comp (R a) (R b) = R (I.compRel a b)
445+
446+-- | Relational right division
447+--
448+-- @'divR' x y@ is the largest relation @z@ which,
449+-- pre-composed with @y@, approximates @x@.
450+divR :: Relation b c -> Relation b a -> Relation a c
451+divR (R x) (R y) = R (I.divR x y)
452+
453+-- | Relational left division
454+--
455+-- The dual division operator:
456+--
457+-- @
458+-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' y)
459+-- @
460+divL :: Relation c b -> Relation a b -> Relation a c
461+divL (R x) (R y) = R (I.divL x y)
462+
463+-- | Relational symmetric division
464+--
465+-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@
466+-- are related to exactly the same outputs by @r@ and by @s@.
467+divS :: Relation c a -> Relation b a -> Relation c b
468+divS (R x) (R y) = R (I.divS x y)
469+
470+-- | Relational shrinking.
471+--
472+-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
473+-- if it yields an output for an input @x@, it must be a maximum,
474+-- with respect to @s@, among all possible outputs of @x@ by @r@.
475+shrunkBy :: Relation b a -> Relation a a -> Relation b a
476+shrunkBy r s = r `intersection` divR s (conv r)
477+
478+-- | Relational overriding.
479+--
480+-- @r ``overriddenBy`` s@ yields the relation which contains the
481+-- whole of @s@ and that part of @r@ where @s@ is undefined.
482+--
483+-- @
484+-- 'zeros' ``overriddenBy`` s == s
485+-- r ``overriddenBy`` 'zeros' == r
486+-- r ``overriddenBy`` r == r
487+-- @
488+overriddenBy ::
489+ ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
490+ KnownNat (I.Count (I.Normalize b))
491+ ) => Relation a b -> Relation a b -> Relation a b
492+overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
493+
494+-- | Relational application.
495+--
496+-- If @a@ and @b@ are related by 'Relation' @r@
497+-- then @'pointAp' a b r == 'one' ('nat' 1)@
498+pointAp ::
499+ ( Bounded a,
500+ Bounded b,
501+ Enum a,
502+ Enum b,
503+ Eq a,
504+ Eq b,
505+ KnownNat (I.Count (I.Normalize a)),
506+ KnownNat (I.Count (I.Normalize b)),
507+ I.FromLists Boolean (I.Normalize a) One,
508+ I.FromLists Boolean (I.Normalize b) One
509+ ) => a -> b -> Relation a b -> Relation One One
510+pointAp a b r = conv (point b) `comp` r `comp` point a
511+
512+-- | Relational application
513+--
514+-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
515+pointApBool ::
516+ ( Bounded a,
517+ Bounded b,
518+ Enum a,
519+ Enum b,
520+ Eq a,
521+ Eq b,
522+ KnownNat (I.Count (I.Normalize a)),
523+ KnownNat (I.Count (I.Normalize b)),
524+ I.FromLists Boolean (I.Normalize a) One,
525+ I.FromLists Boolean (I.Normalize b) One
526+ ) => a -> b -> Relation a b -> Bool
527+pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
528+
529+-- | Relational converse
530+--
531+-- Given binary 'Relation' r, writing @'pointAp' a b r@
532+-- (read: “@b@ is related to @a@ by @r@”) means the same as
533+-- @'pointAp' b a ('conv' r)@, where @'conv' r@ is said to be
534+-- the converse of @r@.
535+-- In terms of grammar, @'conv' r@ corresponds to the passive voice
536+conv :: Relation a b -> Relation b a
537+conv (R a) = R (I.tr a)
538+
539+-- | Relational inclusion (subset or equal)
540+sse :: Relation a b -> Relation a b -> Bool
541+sse a b = a <= b
542+
543+-- | Relational implication (the same as @'sse'@)
544+implies :: Relation a b -> Relation a b -> Relation a b
545+implies r s = negate r `union` s
546+
547+-- | Relational bi-implication
548+iff :: Relation a b -> Relation a b -> Bool
549+iff r s = r == s
550+
551+-- | Relational intersection
552+--
553+-- Lifts pointwise conjunction.
554+--
555+-- @
556+-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
557+-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s
558+-- @
559+intersection :: Relation a b -> Relation a b -> Relation a b
560+intersection a b = a * b
561+
562+-- | Relational union
563+--
564+-- Lifts pointwise disjunction.
565+--
566+-- @
567+-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
568+-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
569+-- r ``comp`` (s ``union`` t) == (r ``comp`` s) ``union`` (r ``comp`` t)
570+-- (s ``union`` t) ``comp`` r == (s ``comp`` r) ``union`` (t ``comp`` r)
571+-- @
572+union :: Relation a b -> Relation a b -> Relation a b
573+union a b = a + b
574+
575+-- | Relation Kernel
576+--
577+-- @
578+-- 'ker' r == 'conv' r ``comp`` r
579+-- 'ker' r == 'img' ('conv' r)
580+-- @
581+ker :: Relation a b -> Relation a a
582+ker r = conv r `comp` r
583+
584+-- | Relation Image
585+--
586+-- @
587+-- 'img' r == r ``comp`` conv r
588+-- 'img' r == 'ker' ('conv' r)
589+-- @
590+img :: Relation a b -> Relation b b
591+img r = r `comp` conv r
592+
593+-- | Function division. Special case of 'divS'.
594+--
595+-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
596+-- 'entire'.
597+--
598+-- @'divisionF' f g == 'conv' g ``comp`` f@
599+divisionF :: Relation a c -> Relation b c -> Relation a b
600+divisionF f g = conv g `comp` f
601+
602+-- Taxonomy of binary relations
603+
604+-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
605+simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
606+simple = coreflexive . img
607+
608+-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
609+injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
610+injective = coreflexive . ker
611+
612+-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
613+entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
614+entire = reflexive . ker
615+
616+-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
617+surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
618+surjective = reflexive . img
619+
620+-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
621+--
622+-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
623+-- relations:
624+--
625+-- @
626+-- f ``comp`` r ``sse`` s == r ``sse`` f ``comp`` s
627+-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
628+-- @
629+function ::
630+ ( KnownNat (I.Count (I.Normalize b)),
631+ KnownNat (I.Count (I.Normalize a)),
632+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
633+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
634+ )
635+ => Relation a b -> Bool
636+function r = simple r && entire r
637+
638+-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
639+representation ::
640+ ( KnownNat (I.Count (I.Normalize a)),
641+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
642+ )
643+ => Relation a b -> Bool
644+representation r = injective r && entire r
645+
646+-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
647+abstraction ::
648+ ( KnownNat (I.Count (I.Normalize b)),
649+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
650+ )
651+ => Relation a b -> Bool
652+abstraction r = surjective r && simple r
653+
654+-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
655+surjection ::
656+ ( KnownNat (I.Count (I.Normalize b)),
657+ KnownNat (I.Count (I.Normalize a)),
658+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
659+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
660+ )
661+ => Relation a b -> Bool
662+surjection r = function r && abstraction r
663+
664+-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
665+injection ::
666+ ( KnownNat (I.Count (I.Normalize b)),
667+ KnownNat (I.Count (I.Normalize a)),
668+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
669+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
670+ )
671+ => Relation a b -> Bool
672+injection r = function r && representation r
673+
674+-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
675+bijection ::
676+ ( KnownNat (I.Count (I.Normalize b)),
677+ KnownNat (I.Count (I.Normalize a)),
678+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
679+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
680+ ) => Relation a b -> Bool
681+bijection r = injection r && surjection r
682+
683+
684+-- Properties of relations
685+
686+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' ``sse`` r@
687+reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
688+reflexive r = identity <= r
689+
690+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'identity'@
691+coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
692+coreflexive r = r <= identity
693+
694+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
695+transitive :: Relation a a -> Bool
696+transitive r = (r `comp` r) `sse` r
697+
698+-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
699+symmetric :: Relation a a -> Bool
700+symmetric r = r == conv r
701+
702+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'identity'@
703+antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
704+antiSymmetric r = (r `intersection` conv r) `sse` identity
705+
706+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'identity') == 'zeros'@
707+irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
708+irreflexive r = (r `intersection` identity) == zeros
709+
710+-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
711+connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
712+connected r = (r `union` conv r) == ones
713+
714+-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
715+preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
716+preorder r = reflexive r && transitive r
717+
718+-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
719+partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
720+partialOrder r = antiSymmetric r && preorder r
721+
722+-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
723+linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
724+linearOrder r = connected r && partialOrder r
725+
726+-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
727+equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
728+equivalence r = symmetric r && preorder r
729+
730+-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
731+partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
732+partialEquivalence r = partialOrder r && equivalence r
733+
734+-- | A 'Relation' @r@ is 'difunctional' or regular wherever
735+-- @r ``comp`` 'conv' r ``comp`` r == r@
736+difunctional :: Relation a b -> Bool
737+difunctional r = r `comp` conv r `comp` r == r
738+
739+-- Relational pairing
740+
741+-- | Relational pairing.
742+--
743+-- NOTE: That this is not a true categorical product, see for instance:
744+--
745+-- @
746+-- | 'p1' ``comp`` 'splitR' a b ``sse`` a
747+-- 'splitR' a b <=> |
748+-- | 'p2' ``comp`` 'splitR' a b ``sse`` b
749+-- @
750+--
751+-- __Emphasis__ on the 'sse'.
752+--
753+-- @
754+-- 'splitR' r s ``comp`` f == 'splitR' (r ``comp`` f) (s ``comp`` f)
755+-- (R '><' S) ``comp`` 'splitR' p q == 'splitR' (r ``comp`` p) (s ``comp`` q)
756+-- 'conv' ('splitR' r s) ``comp`` 'splitR' x y == ('conv' r ``comp`` x) ``intersection`` ('conv' s ``comp`` y)
757+-- @
758+--
759+-- @
760+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
761+-- @
762+splitR ::
763+ ( KnownNat (I.Count (I.Normalize a)),
764+ KnownNat (I.Count (I.Normalize b)),
765+ KnownNat (I.Count (I.Normalize (a, b))),
766+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
767+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
768+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
769+ )
770+ => Relation c a -> Relation c b -> Relation c (a, b)
771+splitR (R f) (R g) = R (I.khatri f g)
772+
773+-- | Relational pairing first component projection
774+--
775+-- @
776+-- 'p1' ``comp`` 'splitR' r s ``sse`` r
777+-- @
778+p1 ::
779+ forall a b .
780+ ( KnownNat (I.Count (I.Normalize a)),
781+ KnownNat (I.Count (I.Normalize b)),
782+ KnownNat (I.Count (I.Normalize (a, b))),
783+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
784+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
785+ )
786+ => Relation (a, b) a
787+p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
788+
789+-- | Relational pairing second component projection
790+--
791+-- @
792+-- 'p2' ``comp`` 'splitR' r s ``sse`` s
793+-- @
794+p2 ::
795+ forall a b .
796+ ( KnownNat (I.Count (I.Normalize b)),
797+ KnownNat (I.Count (I.Normalize a)),
798+ KnownNat (I.Count (I.Normalize (a, b))),
799+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
800+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
801+ )
802+ => Relation (a, b) b
803+p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
804+
805+-- Relational pairing functor
806+
807+infixl 4 ><
808+-- | Relational pairing functor
809+--
810+-- @
811+-- r '><' s == 'splitR' (r ``comp`` p1) (s ``comp`` p2)
812+-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
813+-- @
814+(><) ::
815+ ( KnownNat (I.Count (I.Normalize a)),
816+ KnownNat (I.Count (I.Normalize b)),
817+ KnownNat (I.Count (I.Normalize c)),
818+ KnownNat (I.Count (I.Normalize d)),
819+ KnownNat (I.Count (I.Normalize (a, c))),
820+ KnownNat (I.Count (I.Normalize (b, d))),
821+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),
822+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),
823+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),
824+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize d),
825+ I.Normalize (a, c) ~ I.Normalize (I.Normalize a, I.Normalize c),
826+ I.Normalize (b, d) ~ I.Normalize (I.Normalize b, I.Normalize d)
827+ )
828+ => Relation a b -> Relation c d -> Relation (a, c) (b, d)
829+(><) (R a) (R b) = R ((I.><) a b)
830+
831+-- Relational co-products
832+
833+-- | Relational coproduct.
834+--
835+-- @
836+-- | 'eitherR' a b ``comp`` 'i1' == a
837+-- 'eitherR' a b <=> |
838+-- | 'eitherR' a b ``comp`` 'i2' == b
839+-- @
840+--
841+-- @
842+-- 'eitherR' r s ``comp`` 'conv' ('eitherR' t u) == (r ``comp`` 'conv' t) ``union`` (s ``comp`` 'conv' u)
843+-- @
844+--
845+-- @
846+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
847+-- @
848+eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
849+ => Relation a c -> Relation b c -> Relation (Either a b) c
850+eitherR = junc
851+
852+-- | Relational coproduct first component injection
853+--
854+-- @
855+-- 'img' 'i1' ``union`` 'img' 'i2' == 'identity'
856+-- 'i1' ``comp`` 'i2' = 'zeros'
857+-- @
858+i1 ::
859+ ( KnownNat (I.Count (I.Normalize b)),
860+ KnownNat (I.Count (I.Normalize a)),
861+ I.FromLists Boolean (I.Normalize b) (I.Normalize a),
862+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
863+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
864+ )
865+ => Relation a (Either a b)
866+i1 = R I.i1
867+
868+-- | Relational coproduct second component injection
869+--
870+-- @
871+-- 'img' 'i1' ``union`` 'img' 'i2' == 'identity'
872+-- 'i1' ``comp`` 'i2' = 'zeros'
873+-- @
874+i2 ::
875+ ( KnownNat (I.Count (I.Normalize b)),
876+ KnownNat (I.Count (I.Normalize a)),
877+ I.FromLists Boolean (I.Normalize a) (I.Normalize b),
878+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
879+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
880+ )
881+ => Relation b (Either a b)
882+i2 = R I.i2
883+
884+infixl 5 -|-
885+
886+-- | Relational coproduct functor.
887+--
888+-- @
889+-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
890+-- @
891+(-|-) ::
892+ ( KnownNat (I.Count (I.Normalize d)),
893+ KnownNat (I.Count (I.Normalize b)),
894+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
895+ I.FromLists Boolean (I.Normalize d) (I.Normalize b),
896+ I.FromLists Boolean (I.Normalize b) (I.Normalize d),
897+ I.FromLists Boolean (I.Normalize d) (I.Normalize d),
898+ I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),
899+ I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)
900+ )
901+ => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
902+(-|-) (R a) (R b) = R ((I.-|-) a b)
903+
904+-- Relational "Currying"
905+
906+-- | Relational 'trans'
907+--
908+-- Every n-ary relation can be expressed as a binary relation through
909+-- 'trans'/'untrans';
910+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
911+trans ::
912+ ( KnownNat (I.Count (I.Normalize (a, b))),
913+ KnownNat (I.Count (I.Normalize a)),
914+ KnownNat (I.Count (I.Normalize (c, b))),
915+ KnownNat (I.Count (I.Normalize b)),
916+ KnownNat (I.Count (I.Normalize c)),
917+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
918+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
919+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
920+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
921+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
922+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
923+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
924+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
925+ )
926+ => Relation (a, b) c -> Relation a (c, b)
927+trans r = splitR r p2 `comp` conv p1
928+
929+-- | Relational 'untrans'
930+--
931+-- Every n-ary relation can be expressed as a binary relation through
932+-- 'trans'/'untrans';
933+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
934+untrans ::
935+ ( KnownNat (I.Count (I.Normalize (a, b))),
936+ KnownNat (I.Count (I.Normalize a)),
937+ KnownNat (I.Count (I.Normalize (c, b))),
938+ KnownNat (I.Count (I.Normalize b)),
939+ KnownNat (I.Count (I.Normalize c)),
940+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
941+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
942+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
943+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
944+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
945+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
946+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
947+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
948+ )
949+ => Relation a (c, b) -> Relation (a, b) c
950+untrans s = p1 `comp` conv (splitR (conv s) p2)
951+
952+-- | Transforms predicate @p@ into a correflexive relation.
953+--
954+-- @
955+-- 'predR' ('const' True) == 'identity'
956+-- 'predR' ('const' False) == 'zeros'
957+-- @
958+--
959+-- @
960+-- 'predR' q ``comp`` 'predR' p == 'predR' q ``union`` 'predR' p
961+-- @
962+predR ::
963+ ( Bounded a,
964+ Enum a,
965+ KnownNat (I.Count (I.Normalize a)),
966+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
967+ I.FromLists Boolean (I.Normalize Bool) (I.Normalize a)
968+ )
969+ => (a -> Bool) -> Relation a a
970+predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
971+
972+-- | Equalizes functions @f@ and @g@.
973+-- That is, @'equalizer' f g@ is the largest coreflexive
974+-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
975+--
976+-- @
977+-- 'equalizer' r r == 'identity'
978+-- 'equalizer' ('point' True) ('point' False) == 'zeros'
979+-- @
980+equalizer ::
981+ ( KnownNat (I.Count (I.Normalize a)),
982+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
983+ )
984+ => Relation a b -> Relation a b -> Relation a a
985+equalizer f g = identity `intersection` divisionF f g
986+
987+-- | Relational conditional guard.
988+--
989+-- @
990+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' ``comp`` 'predR' p
991+-- @
992+guard ::
993+ ( Bounded b,
994+ Enum b,
995+ KnownNat (I.Count (I.Normalize b)),
996+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
997+ I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
998+ I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
999+ ) => (b -> Bool) -> Relation b (Either b b)
1000+guard p = conv (eitherR (predR p) (predR (not . p)))
1001+
1002+-- | Relational McCarthy's conditional.
1003+cond ::
1004+ ( Bounded b,
1005+ Enum b,
1006+ KnownNat (I.Count (I.Normalize b)),
1007+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
1008+ I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
1009+ I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
1010+ )
1011+ => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
1012+cond p r s = eitherR r s `comp` guard p
1013+
1014+-- | Relational domain.
1015+--
1016+-- For injective relations, 'domain' and 'ker'nel coincide,
1017+-- since @'ker' r ``sse`` 'identity'@ in such situations.
1018+domain ::
1019+ ( KnownNat (I.Count (I.Normalize a)),
1020+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
1021+ ) => Relation a b -> Relation a a
1022+domain r = ker r `intersection` identity
1023+
1024+-- | Relational range.
1025+--
1026+-- For functions, 'range' and 'img' (image) coincide,
1027+-- since @'img' f ``sse`` 'identity'@ for any @f@.
1028+range ::
1029+ ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
1030+ KnownNat (I.Count (I.Normalize b))
1031+ ) => Relation a b -> Relation b b
1032+range r = img r `intersection` identity
1033+
1034+-- Relation pretty print
1035+
1036+-- | Relation pretty printing
1037+pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1038+pretty (R a) = I.pretty a
1039+
1040+-- | Relation pretty printing
1041+prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1042+prettyPrint (R a) = I.prettyPrint a