@@ -27,7 +27,7 @@
2727
2828module LAoP.Relation.Internal
2929 ( -- | This definition makes use of the fact that 'Void' is
30− -- isomorphic to 0 and '()' to 1 and captures matrix
30+ -- isomorphic to 0 and 'One' to 1 and captures matrix
3131 -- dimensions as stacks of 'Either's.
3232 --
3333 -- There exists two type families that make it easier to write
@@ -60,10 +60,13 @@ module LAoP.Relation.Internal
6060 toRel,
6161 toLists,
6262 toList,
63+ toBool,
64+ pt,
6365 relationBuilder,
6466 zeros,
6567 ones,
6668 bang,
69+ point,
6770
6871 -- * Relational operations
6972 conv,
@@ -132,6 +135,9 @@ module LAoP.Relation.Internal
132135 fromF,
133136 fromF',
134137
138+ -- ** Relational application
139+ pointAp,
140+
135141 -- * Matrix printing
136142 pretty,
137143 prettyPrint
@@ -140,7 +146,7 @@ module LAoP.Relation.Internal
140146
141147import Data.Void
142148import qualified LAoP.Matrix.Internal as I
143−import LAoP.Utils
149+import LAoP.Utils.Internal
144150import Control.DeepSeq
145151import qualified Control.Category as C
146152import Data.Bool
@@ -174,6 +180,8 @@ instance Num (Relation a b) where
174180 -- | Matrix multiplication becomes Boolean matrix conjunction
175181 (R a) * (R b) = R (I.andM a b)
176182
183+ negate (R a) = R (I.negateM a)
184+
177185-- Type alias
178186type Zero = Void
179187type One = ()
@@ -289,6 +297,30 @@ toLists (R m) = I.toLists m
289297toList :: Relation a b -> [Boolean]
290298toList (R m) = I.toList m
291299
300+-- | Converts a well typed @'Relation'@ to @'Bool'@.
301+toBool :: Relation One One -> Bool
302+toBool r = case toList r of
303+ [Nat 0] -> False
304+ _ -> True
305+
306+-- | Power transpose
307+pt ::
308+ ( Bounded a,
309+ Bounded b,
310+ Enum a,
311+ Enum b,
312+ Eq a,
313+ Eq b,
314+ KnownNat (I.Count (I.Normalize a)),
315+ KnownNat (I.Count (I.Normalize b)),
316+ I.FromLists Boolean (I.Normalize a) One,
317+ I.FromLists Boolean (I.Normalize b) One
318+ )
319+ => Relation a b -> (a -> [b])
320+pt r a =
321+ let lb = [minBound .. maxBound]
322+ in [ b | b <- lb, toBool (pointAp a b r) ]
323+
292324-- Zeros Matrix
293325
294326-- | The zero matrix. A matrix wholly filled with zeros.
@@ -311,11 +343,20 @@ ones = relationBuilder (const (nat 1))
311343
312344-- | The T (Top) row vector matrix.
313345bang ::
314− forall a.
315− (I.FromLists Boolean (I.Normalize a) (), KnownNat (I.Count (I.Normalize a))) =>
346+ (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
316347 Relation a One
317348bang = ones
318349
350+-- | Point constant relation
351+point ::
352+ ( Bounded a,
353+ Enum a,
354+ Eq a,
355+ KnownNat (I.Count (I.Normalize a)),
356+ I.FromLists Boolean (I.Normalize a) One
357+ ) => a -> Relation One a
358+point a = fromF' (const a)
359+
319360-- Identity Matrix
320361
321362-- | Identity matrix
@@ -325,9 +366,24 @@ identity ::
325366identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
326367
327368-- | Relational composition
328−comp :: forall a b c . Relation b c -> Relation a b -> Relation a c
369+comp :: Relation b c -> Relation a b -> Relation a c
329370comp (R a) (R b) = R (I.compRel a b)
330371
372+-- | Relational application
373+pointAp ::
374+ ( Bounded a,
375+ Bounded b,
376+ Enum a,
377+ Enum b,
378+ Eq a,
379+ Eq b,
380+ KnownNat (I.Count (I.Normalize a)),
381+ KnownNat (I.Count (I.Normalize b)),
382+ I.FromLists Boolean (I.Normalize a) One,
383+ I.FromLists Boolean (I.Normalize b) One
384+ ) => a -> b -> Relation a b -> Relation One One
385+pointAp a b r = conv (point b) `comp` r `comp` point a
386+
331387-- | Relational converse
332388conv :: Relation a b -> Relation b a
333389conv (R a) = R (I.tr a)
@@ -337,12 +393,12 @@ sse :: Relation a b -> Relation a b -> Bool
337393sse a b = a <= b
338394
339395-- | Relational implication (the same as @'sse'@)
340−implies :: Relation a b -> Relation a b -> Bool
341−implies = sse
396+implies :: Relation a b -> Relation a b -> Relation a b
397+implies r s = negate r `union` s
342398
343399-- | Relational bi-implication
344400iff :: Relation a b -> Relation a b -> Bool
345−iff r s = (r `implies` s) && (s `implies` r)
401+iff r s = r == s
346402
347403-- | Relational intersection
348404--