git.iko.soy/laop
on master help sign in
Added constraint type synonyms to the rest
commit43fe3c23f2e314bc8cfda23c31b1944d2ccdebb8 authorArmando Santos <armandoifsantos@gmail.com> dateThu 30 Jan 2020, 00:25 (7 years ago) parent43624a6
4 files changed+317−333
compare with master
unifiedsplit
src/LAoP/Matrix/Nat.hs+117−125 src/LAoP/Matrix/Type.hs+11 src/LAoP/Relation.hs+12 src/LAoP/Relation/Internal.hs+177−208
src/LAoP/Matrix/Nat.hs+117−125
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
12{-# LANGUAGE AllowAmbiguousTypes #-}
23{-# LANGUAGE DataKinds #-}
34{-# LANGUAGE DerivingVia #-}
@@ -53,6 +54,18 @@ module LAoP.Matrix.Nat
5354 -- * Type safe matrix representation
5455 Matrix (..),
5556
57+ -- * Constraint type synonyms
58+ Countable,
59+ CountableDimensions,
60+ CountableN,
61+ CountableNz,
62+ CountableDimensionsN,
63+ FromListsN,
64+ FromListsNz,
65+ Liftable,
66+ TrivialE,
67+ TrivialP,
68+
5669 -- * Primitives
5770 empty,
5871 one,
@@ -147,6 +160,18 @@ import qualified LAoP.Matrix.Internal as I
147160newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148161 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
149162
163+-- | Constraint type synonyms to keep the type signatures less convoluted
164+type Countable a = KnownNat (I.Count a)
165+type CountableDimensions a b = (Countable a, Countable b)
166+type CountableN a = KnownNat (I.Count (I.FromNat a))
167+type CountableNz a = KnownNat (I.Count (I.Normalize a))
168+type CountableDimensionsN a b = (CountableN a, CountableN b)
169+type FromListsN e a b = I.FromLists e (I.FromNat a) (I.FromNat b)
170+type FromListsNz e a b = I.FromLists e (I.Normalize a) (I.Normalize b)
171+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
172+type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)
173+type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
174+
150175-- | It isn't possible to implement the 'id' function so it's
151176-- implementation is 'undefined'. However 'comp' can be and this partial
152177-- class implementation exists just to make the code more readable.
@@ -165,44 +190,43 @@ one :: e -> Matrix e 1 1
165190one = M . I.One
166191
167192junc ::
168− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
169− Matrix e cols1 rows ->
170− Matrix e cols2 rows ->
171− Matrix e cols3 rows
193+ (TrivialE a b) =>
194+ Matrix e a rows ->
195+ Matrix e b rows ->
196+ Matrix e (a + b) rows
172197junc (M a) (M b) = M (I.Junc a b)
173198
174199infixl 3 |||
175200(|||) ::
176− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
177− Matrix e cols1 rows ->
178− Matrix e cols2 rows ->
179− Matrix e cols3 rows
201+ (TrivialE a b) =>
202+ Matrix e a rows ->
203+ Matrix e b rows ->
204+ Matrix e (a + b) rows
180205(|||) = junc
181206
182207split ::
183− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
184− Matrix e cols rows1 ->
185− Matrix e cols rows2 ->
186− Matrix e cols rows3
208+ (TrivialE a b) =>
209+ Matrix e cols a ->
210+ Matrix e cols b ->
211+ Matrix e cols (a + b)
187212split (M a) (M b) = M (I.Split a b)
188213
189214infixl 2 ===
190215(===) ::
191− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
192− Matrix e cols rows1 ->
193− Matrix e cols rows2 ->
194− Matrix e cols rows3
216+ (TrivialE a b) =>
217+ Matrix e cols a ->
218+ Matrix e cols b ->
219+ Matrix e cols (a + b)
195220(===) = split
196221
197222-- Construction
198223
199−fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows
224+fromLists :: (FromListsN e cols rows) => [[e]] -> Matrix e cols rows
200225fromLists = M . I.fromLists
201226
202227matrixBuilder ::
203− (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
204− ((Int, Int) -> e) ->
205− Matrix e cols rows
228+ (FromListsN e cols rows, CountableN cols, CountableN rows)
229+ => ((Int, Int) -> e) -> Matrix e cols rows
206230matrixBuilder = M . I.matrixBuilder
207231
208232col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
@@ -212,32 +236,20 @@ row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1
212236row = M . I.row
213237
214238fromF ::
215− ( Bounded a,
216− Bounded b,
217− Enum a,
218− Enum b,
219− Eq b,
220− Num e,
221− Ord e,
222− KnownNat (I.Count (I.FromNat cols)),
223− KnownNat (I.Count (I.FromNat rows)),
224− I.FromLists e (I.FromNat rows) (I.FromNat cols)
239+ ( Liftable e a b,
240+ CountableN cols,
241+ CountableN rows,
242+ FromListsN e rows cols
225243 ) =>
226244 (a -> b) ->
227245 Matrix e cols rows
228246fromF = M . I.fromF
229247
230248fromF' ::
231− ( Bounded a,
232− Bounded b,
233− Enum a,
234− Enum b,
235− Eq b,
236− Num e,
237− Ord e,
238− KnownNat (I.Count (I.Normalize a)),
239− KnownNat (I.Count (I.Normalize b)),
240− I.FromLists e (I.Normalize b) (I.Normalize a)
249+ ( Liftable e a b,
250+ CountableNz a,
251+ CountableNz b,
252+ FromListsNz e b a
241253 ) =>
242254 (a -> b) ->
243255 Matrix e (I.Count a) (I.Count b)
@@ -254,21 +266,21 @@ toList (M m) = I.toList m
254266-- Zeros Matrix
255267
256268zeros ::
257− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
269+ (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) =>
258270 Matrix e cols rows
259271zeros = M I.zeros
260272
261273-- Ones Matrix
262274
263275ones ::
264− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
276+ (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) =>
265277 Matrix e cols rows
266278ones = M I.ones
267279
268280-- Const Matrix
269281
270282constant ::
271− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
283+ (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) =>
272284 e ->
273285 Matrix e cols rows
274286constant = M . I.constant
@@ -277,14 +289,14 @@ constant = M . I.constant
277289
278290bang ::
279291 forall e cols.
280− (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>
292+ (Num e, Enum e, I.FromLists e (I.FromNat cols) (), CountableN cols) =>
281293 Matrix e cols 1
282294bang = M I.bang
283295
284296-- Identity Matrix
285297
286298identity ::
287− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>
299+ (Num e, FromListsN e cols cols, CountableN cols) =>
288300 Matrix e cols cols
289301identity = M I.identity
290302
@@ -295,22 +307,20 @@ comp (M a) (M b) = M (I.comp a b)
295307
296308p1 ::
297309 ( Num e,
298− KnownNat (I.Count (I.FromNat n)),
299− KnownNat (I.Count (I.FromNat m)),
300− I.FromLists e (I.FromNat n) (I.FromNat m),
301− I.FromLists e (I.FromNat m) (I.FromNat m),
302− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
310+ CountableDimensionsN n m,
311+ FromListsN e n m,
312+ FromListsN e m m,
313+ TrivialE m n
303314 ) =>
304315 Matrix e (m + n) m
305316p1 = M I.p1
306317
307318p2 ::
308319 ( Num e,
309− KnownNat (I.Count (I.FromNat n)),
310− KnownNat (I.Count (I.FromNat m)),
311− I.FromLists e (I.FromNat m) (I.FromNat n),
312− I.FromLists e (I.FromNat n) (I.FromNat n),
313− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
320+ CountableDimensionsN n m,
321+ FromListsN e m n,
322+ FromListsN e n n,
323+ TrivialE m n
314324 ) =>
315325 Matrix e (m + n) n
316326p2 = M I.p2
@@ -319,138 +329,123 @@ p2 = M I.p2
319329
320330i1 ::
321331 ( Num e,
322− KnownNat (I.Count (I.FromNat n)),
323− KnownNat (I.Count (I.FromNat rows)),
324− I.FromLists e (I.FromNat n) (I.FromNat rows),
325− I.FromLists e (I.FromNat rows) (I.FromNat rows),
326− I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)
332+ CountableDimensionsN n rows,
333+ FromListsN e n rows,
334+ FromListsN e rows rows,
335+ TrivialE rows n
327336 ) =>
328337 Matrix e rows (rows + n)
329338i1 = tr p1
330339
331340i2 ::
332341 ( Num e,
333− KnownNat (I.Count (I.FromNat rows)),
334− KnownNat (I.Count (I.FromNat m)),
335− I.FromLists e (I.FromNat m) (I.FromNat rows),
336− I.FromLists e (I.FromNat rows) (I.FromNat rows),
337− I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)
342+ CountableDimensionsN rows m,
343+ FromListsN e m rows,
344+ FromListsN e rows rows,
345+ TrivialE m rows
338346 ) =>
339347 Matrix e rows (m + rows)
340348i2 = tr p2
341349
342350-- Dimensions
343351
344−rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
352+rows :: (CountableN rows) => Matrix e cols rows -> Int
345353rows (M m) = I.rows m
346354
347−columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
355+columns :: (CountableN cols) => Matrix e cols rows -> Int
348356columns (M m) = I.columns m
349357
350−-- Coproduct Bifunctor
351−
358+-- | Coproduct Bifunctor
352359infixl 5 -|-
353360
354361(-|-) ::
355362 ( Num e,
356− KnownNat (I.Count (I.FromNat j)),
357− KnownNat (I.Count (I.FromNat k)),
358− I.FromLists e (I.FromNat k) (I.FromNat k),
359− I.FromLists e (I.FromNat j) (I.FromNat k),
360− I.FromLists e (I.FromNat k) (I.FromNat j),
361− I.FromLists e (I.FromNat j) (I.FromNat j),
362− I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),
363− I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)
363+ CountableDimensionsN j k,
364+ FromListsN e k k,
365+ FromListsN e j k,
366+ FromListsN e k j,
367+ FromListsN e j j,
368+ TrivialE n m,
369+ TrivialE k j
364370 ) =>
365371 Matrix e n k ->
366372 Matrix e m j ->
367373 Matrix e (n + m) (k + j)
368374(-|-) (M a) (M b) = M ((I.-|-) a b)
369375
370−-- Khatri Rao Product and projections
371−
376+-- | Khatri Rao Product and projections
372377kp1 ::
373378 forall e m k .
374379 ( Num e,
375− KnownNat (I.Count (I.FromNat m)),
376− KnownNat (I.Count (I.FromNat k)),
377− KnownNat (I.Count (I.FromNat (m * k))),
378− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
379− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
380+ CountableDimensionsN m k,
381+ CountableN (m * k),
382+ FromListsN e (m * k) m,
383+ TrivialP m k
380384 ) => Matrix e (m * k) m
381385kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
382386
383387kp2 ::
384388 forall e m k.
385389 ( Num e,
386− KnownNat (I.Count (I.FromNat k)),
387− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
388− KnownNat (I.Count (I.FromNat m)),
389− KnownNat (I.Count (I.FromNat (m * k))),
390− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
390+ CountableDimensionsN k m,
391+ FromListsN e (m * k) k,
392+ CountableN (m * k),
393+ TrivialP m k
391394 ) => Matrix e (m * k) k
392395kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
393396
394397khatri ::
395398 forall e cols a b.
396399 ( Num e,
397− KnownNat (I.Count (I.FromNat a)),
398− KnownNat (I.Count (I.FromNat b)),
399− KnownNat (I.Count (I.FromNat (a * b))),
400− I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
401− I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
402− I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
400+ CountableDimensionsN a b,
401+ CountableN (a * b),
402+ FromListsN e (a * b) a,
403+ FromListsN e (a * b) b,
404+ TrivialP a b
403405 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
404406khatri a b =
405407 let kp1' = kp1 @e @a @b
406408 kp2' = kp2 @e @a @b
407409 in comp (tr kp1') a * comp (tr kp2') b
408410
409−-- Product Bifunctor (Kronecker)
410−
411+-- | Product Bifunctor (Kronecker)
411412infixl 4 ><
412413
413414(><) ::
414415 forall e m p n q.
415416 ( Num e,
416− KnownNat (I.Count (I.FromNat m)),
417− KnownNat (I.Count (I.FromNat n)),
418− KnownNat (I.Count (I.FromNat p)),
419− KnownNat (I.Count (I.FromNat q)),
420− KnownNat (I.Count (I.FromNat (m * n))),
421− KnownNat (I.Count (I.FromNat (p * q))),
422− I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
423− I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
424− I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
425− I.FromLists e (I.FromNat (p * q)) (I.FromNat q),
426− I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),
427− I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))
417+ CountableDimensionsN m n,
418+ CountableDimensionsN p q,
419+ CountableDimensionsN (m * n) (p * q),
420+ FromListsN e (m * n) m,
421+ FromListsN e (m * n) n,
422+ FromListsN e (p * q) p,
423+ FromListsN e (p * q) q,
424+ TrivialP m n,
425+ TrivialP p q
428426 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
429427(><) a b =
430428 let kp1' = kp1 @e @m @n
431429 kp2' = kp2 @e @m @n
432430 in khatri (comp a kp1') (comp b kp2')
433431
434−-- Matrix abide Junc Split
435−
432+-- | Matrix abide Junc Split
436433abideJS :: Matrix e cols rows -> Matrix e cols rows
437434abideJS (M m) = M (I.abideJS m)
438435
439−-- Matrix abide Split Junc
440−
436+-- | Matrix abide Split Junc
441437abideSJ :: Matrix e cols rows -> Matrix e cols rows
442438abideSJ (M m) = M (I.abideSJ m)
443439
444−-- Matrix transposition
445−
440+-- | Matrix transposition
446441tr :: Matrix e cols rows -> Matrix e rows cols
447442tr (M m) = M (I.tr m)
448443
449444-- Selective 'select' operator
450445select ::
451446 ( Num e,
452− I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
453− KnownNat (I.Count (I.FromNat rows1)),
447+ FromListsN e rows1 rows1,
448+ CountableN rows1,
454449 I.FromNat rows2 ~ I.FromNat rows1,
455450 I.FromNat cols1 ~ I.FromNat cols2,
456451 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -461,14 +456,11 @@ select (M m) (M y) = M (I.select m y)
461456
462457cond ::
463458 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
464− KnownNat (I.Count (I.FromNat cols)),
459+ CountableN cols,
465460 I.FromLists e () (I.FromNat cols),
466461 I.FromLists e (I.FromNat cols) (),
467− I.FromLists e (I.FromNat cols) (I.FromNat cols),
468− Bounded a,
469− Enum a,
470− Num e,
471− Ord e
462+ FromListsN e cols cols,
463+ Liftable e a Bool
472464 )
473465 =>
474466 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
@@ -476,8 +468,8 @@ cond p (M a) (M b) = M (I.cond p a b)
476468
477469-- Pretty print
478470
479−pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String
471+pretty :: (CountableN cols, Show e) => Matrix e cols rows -> String
480472pretty (M m) = I.pretty m
481473
482−prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()
474+prettyPrint :: (CountableN cols, Show e) => Matrix e cols rows -> IO ()
483475prettyPrint (M m) = I.prettyPrint m
src/LAoP/Matrix/Type.hs+11
@@ -56,6 +56,17 @@ module LAoP.Matrix.Type
5656 -- * Type safe matrix representation
5757 Matrix (..),
5858
59+ -- * Constraint type aliases
60+ Countable,
61+ CountableDimensions,
62+ CountableN,
63+ CountableDimensionsN,
64+ FromListsN,
65+ Liftable,
66+ Trivial,
67+ TrivialE,
68+ TrivialP,
69+
5970 -- * Type aliases
6071 Zero,
6172 One,
src/LAoP/Relation.hs+12
@@ -30,6 +30,18 @@ module LAoP.Relation
3030 Relation (..),
3131 Boolean,
3232
33+ -- * Constraint type synonyms
34+ Countable,
35+ CountableDimensions,
36+ CountableN,
37+ CountableDimensionsN,
38+ FromListsN,
39+ Liftable,
40+ Trivial,
41+ TrivialE,
42+ TrivialP,
43+ TrivialP2,
44+
3345 -- * Primitives
3446 empty,
3547 one,
src/LAoP/Relation/Internal.hs+177−208
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
12{-# LANGUAGE GADTs #-}
23{-# LANGUAGE UndecidableInstances #-}
34{-# LANGUAGE FlexibleContexts #-}
@@ -39,6 +40,18 @@ module LAoP.Relation.Internal
3940 Relation (..),
4041 Boolean,
4142
43+ -- * Constraint type synonyms
44+ Countable,
45+ CountableDimensions,
46+ CountableN,
47+ CountableDimensionsN,
48+ FromListsN,
49+ Liftable,
50+ Trivial,
51+ TrivialE,
52+ TrivialP,
53+ TrivialP2,
54+
4255 -- * Primitives
4356 empty,
4457 one,
@@ -179,6 +192,18 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
179192
180193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
181194
195+-- | Constraint type synonyms to keep the type signatures less convoluted
196+type Countable a = KnownNat (I.Count a)
197+type CountableDimensions a b = (Countable a, Countable b)
198+type CountableN a = KnownNat (I.Count (I.Normalize a))
199+type CountableDimensionsN a b = (CountableN a, CountableN b)
200+type FromListsN a b = I.FromLists Boolean (I.Normalize a) (I.Normalize b)
201+type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)
202+type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
203+type TrivialE a b = I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
204+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
205+type TrivialP2 a b = I.Normalize (I.Normalize a, I.Normalize b) ~ I.Normalize (I.Normalize (a, b))
206+
182207-- | It isn't possible to implement the 'id' function so it's
183208-- implementation is 'undefined'. However 'comp' can be and this partial
184209-- class implementation exists just to make the code more readable.
@@ -218,7 +243,7 @@ one = R . I.One
218243-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
219244--
220245-- See 'eitherR'.
221−junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
246+junc :: (TrivialE a b)
222247 => Relation a c -> Relation b c -> Relation (Either a b) c
223248junc (R a) (R b) = R (I.Junc a b)
224249
@@ -227,21 +252,21 @@ infixl 3 |||
227252--
228253-- See 'eitherR'.
229254(|||) ::
230− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
255+ (TrivialE a b) =>
231256 Relation a c ->
232257 Relation b c ->
233258 Relation (Either a b) c
234259(|||) = junc
235260
236261-- | Boolean Matrix 'Split' constructor, also known as relational product.
237−split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
262+split :: (TrivialE a b)
238263 => Relation c a -> Relation c b -> Relation c (Either a b)
239264split (R a) (R b) = R (I.Split a b)
240265
241266infixl 2 ===
242267-- | Boolean Matrix 'Split' constructor
243268(===) ::
244− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
269+ (TrivialE a b) =>
245270 Relation c a ->
246271 Relation c b ->
247272 Relation c (Either a b)
@@ -251,15 +276,14 @@ infixl 2 ===
251276
252277-- | Build a matrix out of a list of list of elements. Throws a runtime
253278-- error if the dimensions do not match.
254−fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
279+fromLists :: (FromListsN a b) => [[Boolean]] -> Relation a b
255280fromLists = R . I.fromLists
256281
257282-- | Matrix builder function. Constructs a matrix provided with
258283-- a construction function.
259284relationBuilder ::
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
285+ (FromListsN a b, CountableDimensionsN a b) =>
286+ ((Int, Int) -> Boolean) -> Relation a b
263287relationBuilder = R . I.matrixBuilder
264288
265289-- | Lifts functions to matrices with arbitrary dimensions.
@@ -267,14 +291,9 @@ relationBuilder = R . I.matrixBuilder
267291-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
268292-- types @a@ or @b@ allows.
269293fromF ::
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)
294+ ( Liftable a b,
295+ CountableDimensionsN c d,
296+ FromListsN d c
278297 )
279298 => (a -> b) -> Relation c d
280299fromF f = R (I.fromFRel f)
@@ -282,44 +301,29 @@ fromF f = R (I.fromFRel f)
282301-- | Lifts functions to matrices with dimensions matching @a@ and @b@
283302-- cardinality's.
284303fromF' ::
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)
304+ ( Liftable a b,
305+ CountableDimensionsN a b,
306+ FromListsN b a
293307 )
294308 => (a -> b) -> Relation a b
295309fromF' f = R (I.fromFRel' f)
296310
297311-- | Lifts relation functions to 'Relation'
298312toRel ::
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)
313+ ( Liftable a b,
314+ CountableDimensionsN a b,
315+ FromListsN b a
307316 )
308− => (a -> b -> Bool) -> Relation a b
317+ => (a -> b -> Bool) -> Relation a b
309318toRel = R . I.toRel
310319
311320-- | Lowers a 'Relation' to a function
312321fromRel ::
313− ( Bounded a,
314− Bounded b,
315− Enum a,
316− Enum b,
322+ ( Liftable a b,
317323 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
324+ CountableDimensionsN a b,
325+ FromListsN a One,
326+ FromListsN b One
323327 )
324328 => Relation a b -> (a -> b -> Bool)
325329fromRel r a b = pointApBool a b r
@@ -344,16 +348,11 @@ toBool r = case toList r of
344348--
345349-- Maps a relation to a set valued function.
346350pt ::
347− ( Bounded a,
348− Bounded b,
349− Enum a,
350− Enum b,
351+ ( Liftable a b,
351352 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
353+ CountableDimensionsN a b,
354+ FromListsN a One,
355+ FromListsN b One
357356 )
358357 => Relation a b -> (a -> Powerset b)
359358pt r a =
@@ -365,9 +364,8 @@ belongs ::
365364 ( Bounded a,
366365 Enum a,
367366 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))
367+ CountableDimensionsN (Powerset a) a,
368+ FromListsN a (Powerset a)
371369 )
372370 => Relation (Powerset a) a
373371belongs = toRel (flip elemR)
@@ -386,7 +384,7 @@ belongs = toRel (flip elemR)
386384-- ⊥ ``sse`` R && R ``sse`` T == True
387385-- @
388386zeros ::
389− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
387+ (FromListsN a b, CountableDimensionsN a b) =>
390388 Relation a b
391389zeros = relationBuilder (const (nat 0))
392390
@@ -401,7 +399,7 @@ zeros = relationBuilder (const (nat 0))
401399-- ⊥ ``sse`` R && R ``sse`` T == True
402400-- @
403401ones ::
404− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
402+ (FromListsN a b, CountableDimensionsN a b) =>
405403 Relation a b
406404ones = relationBuilder (const (nat 1))
407405
@@ -409,7 +407,7 @@ ones = relationBuilder (const (nat 1))
409407
410408-- | The T (Top) row vector relation.
411409bang ::
412− (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
410+ (FromListsN a One, CountableN a) =>
413411 Relation a One
414412bang = ones
415413
@@ -418,8 +416,8 @@ point ::
418416 ( Bounded a,
419417 Enum a,
420418 Eq a,
421− KnownNat (I.Count (I.Normalize a)),
422− I.FromLists Boolean (I.Normalize a) One
419+ CountableN a,
420+ FromListsN a One
423421 ) => a -> Relation One a
424422point = fromF' . const
425423
@@ -431,8 +429,7 @@ point = fromF' . const
431429-- 'identity' ``comp`` r == r == r ``comp`` 'identity'
432430-- @
433431identity ::
434− (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
435− Relation a a
432+ (FromListsN a a, CountableN a) => Relation a a
436433identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
437434
438435-- | Relational composition
@@ -486,8 +483,8 @@ shrunkBy r s = r `intersection` divR s (conv r)
486483-- r ``overriddenBy`` r == r
487484-- @
488485overriddenBy ::
489− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
490− KnownNat (I.Count (I.Normalize b))
486+ ( FromListsN b b,
487+ CountableN b
491488 ) => Relation a b -> Relation a b -> Relation a b
492489overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
493490
@@ -496,16 +493,11 @@ overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
496493-- If @a@ and @b@ are related by 'Relation' @r@
497494-- then @'pointAp' a b r == 'one' ('nat' 1)@
498495pointAp ::
499− ( Bounded a,
500− Bounded b,
501− Enum a,
502− Enum b,
496+ ( Liftable a b,
503497 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
498+ CountableDimensionsN a b,
499+ FromListsN a One,
500+ FromListsN b One
509501 ) => a -> b -> Relation a b -> Relation One One
510502pointAp a b r = conv (point b) `comp` r `comp` point a
511503
@@ -513,16 +505,11 @@ pointAp a b r = conv (point b) `comp` r `comp` point a
513505--
514506-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
515507pointApBool ::
516− ( Bounded a,
517− Bounded b,
518− Enum a,
519− Enum b,
508+ ( Liftable a b,
520509 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
510+ CountableDimensionsN a b,
511+ FromListsN a One,
512+ FromListsN b One
526513 ) => a -> b -> Relation a b -> Bool
527514pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
528515
@@ -602,19 +589,19 @@ divisionF f g = conv g `comp` f
602589-- Taxonomy of binary relations
603590
604591-- | 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
592+simple :: (CountableN b, FromListsN b b) => Relation a b -> Bool
606593simple = coreflexive . img
607594
608595-- | 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
596+injective :: (CountableN a, FromListsN a a) => Relation a b -> Bool
610597injective = coreflexive . ker
611598
612599-- | 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
600+entire :: (CountableN a, FromListsN a a) => Relation a b -> Bool
614601entire = reflexive . ker
615602
616603-- | 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
604+surjective :: (CountableN b, FromListsN b b) => Relation a b -> Bool
618605surjective = reflexive . img
619606
620607-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
@@ -627,68 +614,63 @@ surjective = reflexive . img
627614-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
628615-- @
629616function ::
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)
617+ ( CountableDimensionsN a b,
618+ FromListsN a a,
619+ FromListsN b b
634620 )
635621 => Relation a b -> Bool
636622function r = simple r && entire r
637623
638624-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
639625representation ::
640− ( KnownNat (I.Count (I.Normalize a)),
641− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
626+ ( CountableN a,
627+ FromListsN a a
642628 )
643629 => Relation a b -> Bool
644630representation r = injective r && entire r
645631
646632-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
647633abstraction ::
648− ( KnownNat (I.Count (I.Normalize b)),
649− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
634+ ( CountableN b,
635+ FromListsN b b
650636 )
651637 => Relation a b -> Bool
652638abstraction r = surjective r && simple r
653639
654640-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
655641surjection ::
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)
642+ ( CountableDimensionsN a b,
643+ FromListsN a a,
644+ FromListsN b b
660645 )
661646 => Relation a b -> Bool
662647surjection r = function r && abstraction r
663648
664649-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
665650injection ::
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)
651+ ( CountableDimensionsN a b,
652+ FromListsN a a,
653+ FromListsN b b
670654 )
671655 => Relation a b -> Bool
672656injection r = function r && representation r
673657
674658-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
675659bijection ::
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)
660+ ( CountableDimensionsN a b,
661+ FromListsN b b,
662+ FromListsN a a
680663 ) => Relation a b -> Bool
681664bijection r = injection r && surjection r
682665
683−
684666-- Properties of relations
685667
686668-- | 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
669+reflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
688670reflexive r = identity <= r
689671
690672-- | 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
673+coreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
692674coreflexive r = r <= identity
693675
694676-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
@@ -700,35 +682,35 @@ symmetric :: Relation a a -> Bool
700682symmetric r = r == conv r
701683
702684-- | 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
685+antiSymmetric :: (CountableN a, FromListsN a a) => Relation a a -> Bool
704686antiSymmetric r = (r `intersection` conv r) `sse` identity
705687
706688-- | 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
689+irreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
708690irreflexive r = (r `intersection` identity) == zeros
709691
710692-- | 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
693+connected :: (CountableN a, FromListsN a a) => Relation a a -> Bool
712694connected r = (r `union` conv r) == ones
713695
714696-- | 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
697+preorder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
716698preorder r = reflexive r && transitive r
717699
718700-- | 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
701+partialOrder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
720702partialOrder r = antiSymmetric r && preorder r
721703
722704-- | 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
705+linearOrder :: (CountableN a, FromListsN a a) => Relation a a -> Bool
724706linearOrder r = connected r && partialOrder r
725707
726708-- | 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
709+equivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool
728710equivalence r = symmetric r && preorder r
729711
730712-- | 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
713+partialEquivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool
732714partialEquivalence r = partialOrder r && equivalence r
733715
734716-- | A 'Relation' @r@ is 'difunctional' or regular wherever
@@ -760,12 +742,11 @@ difunctional r = r `comp` conv r `comp` r == r
760742-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
761743-- @
762744splitR ::
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)
745+ ( CountableDimensionsN a b,
746+ CountableN (a, b),
747+ FromListsN (a, b) a,
748+ FromListsN (a, b) b,
749+ TrivialP a b
769750 )
770751 => Relation c a -> Relation c b -> Relation c (a, b)
771752splitR (R f) (R g) = R (I.khatri f g)
@@ -777,11 +758,10 @@ splitR (R f) (R g) = R (I.khatri f g)
777758-- @
778759p1 ::
779760 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)
761+ ( CountableDimensionsN a b,
762+ CountableN (a, b),
763+ FromListsN (a, b) a,
764+ TrivialP a b
785765 )
786766 => Relation (a, b) a
787767p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
@@ -793,11 +773,10 @@ p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
793773-- @
794774p2 ::
795775 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)
776+ ( CountableDimensionsN a b,
777+ CountableN (a, b),
778+ FromListsN (a, b) b,
779+ TrivialP a b
801780 )
802781 => Relation (a, b) b
803782p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
@@ -812,18 +791,15 @@ infixl 4 ><
812791-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
813792-- @
814793(><) ::
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)
794+ ( CountableDimensionsN a b,
795+ CountableDimensionsN c d,
796+ CountableDimensionsN (a, c) (b, d),
797+ FromListsN (a, c) a,
798+ FromListsN (a, c) c,
799+ FromListsN (b, d) b,
800+ FromListsN (b, d) d,
801+ TrivialP a c,
802+ TrivialP b d
827803 )
828804 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
829805(><) (R a) (R b) = R ((I.><) a b)
@@ -845,7 +821,7 @@ infixl 4 ><
845821-- @
846822-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
847823-- @
848−eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
824+eitherR :: (TrivialE a b)
849825 => Relation a c -> Relation b c -> Relation (Either a b) c
850826eitherR = junc
851827
@@ -856,11 +832,10 @@ eitherR = junc
856832-- 'i1' ``comp`` 'i2' = 'zeros'
857833-- @
858834i1 ::
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)
835+ ( CountableDimensionsN a b,
836+ FromListsN b a,
837+ FromListsN a a,
838+ TrivialE a b
864839 )
865840 => Relation a (Either a b)
866841i1 = R I.i1
@@ -872,11 +847,10 @@ i1 = R I.i1
872847-- 'i1' ``comp`` 'i2' = 'zeros'
873848-- @
874849i2 ::
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)
850+ ( CountableDimensionsN a b,
851+ FromListsN a b,
852+ FromListsN b b,
853+ TrivialE a b
880854 )
881855 => Relation b (Either a b)
882856i2 = R I.i2
@@ -889,14 +863,13 @@ infixl 5 -|-
889863-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
890864-- @
891865(-|-) ::
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)
866+ ( CountableDimensionsN b d,
867+ FromListsN b b,
868+ FromListsN d b,
869+ FromListsN b d,
870+ FromListsN d d,
871+ TrivialE a c,
872+ TrivialE b d
900873 )
901874 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
902875(-|-) (R a) (R b) = R ((I.-|-) a b)
@@ -909,19 +882,17 @@ infixl 5 -|-
909882-- 'trans'/'untrans';
910883-- more-over, where each particular attribute is placed (input/output) is irrelevant.
911884trans ::
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)))
885+ ( CountableDimensionsN a b,
886+ CountableN c,
887+ CountableDimensionsN (a, b) (c, b),
888+ FromListsN (c, b) c,
889+ FromListsN (c, b) b,
890+ FromListsN (a, b) a,
891+ FromListsN (a, b) b,
892+ Trivial (a, b),
893+ Trivial (c, b),
894+ TrivialP2 a b,
895+ TrivialP2 c b
925896 )
926897 => Relation (a, b) c -> Relation a (c, b)
927898trans r = splitR r p2 `comp` conv p1
@@ -932,19 +903,17 @@ trans r = splitR r p2 `comp` conv p1
932903-- 'trans'/'untrans';
933904-- more-over, where each particular attribute is placed (input/output) is irrelevant.
934905untrans ::
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)))
906+ ( CountableDimensionsN a b,
907+ CountableN c,
908+ CountableDimensionsN (a, b) (c, b),
909+ FromListsN (c, b) c,
910+ FromListsN (c, b) b,
911+ FromListsN (a, b) b,
912+ FromListsN (a, b) a,
913+ Trivial (a, b),
914+ Trivial (c, b),
915+ TrivialP2 a b,
916+ TrivialP2 c b
948917 )
949918 => Relation a (c, b) -> Relation (a, b) c
950919untrans s = p1 `comp` conv (splitR (conv s) p2)
@@ -962,9 +931,9 @@ untrans s = p1 `comp` conv (splitR (conv s) p2)
962931predR ::
963932 ( Bounded a,
964933 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)
934+ CountableN a,
935+ FromListsN a a,
936+ FromListsN Bool a
968937 )
969938 => (a -> Bool) -> Relation a a
970939predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
@@ -978,8 +947,8 @@ predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
978947-- 'equalizer' ('point' True) ('point' False) == 'zeros'
979948-- @
980949equalizer ::
981− ( KnownNat (I.Count (I.Normalize a)),
982− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
950+ ( CountableN a,
951+ FromListsN a a
983952 )
984953 => Relation a b -> Relation a b -> Relation a a
985954equalizer f g = identity `intersection` divisionF f g
@@ -992,10 +961,10 @@ equalizer f g = identity `intersection` divisionF f g
992961guard ::
993962 ( Bounded b,
994963 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)
964+ CountableN b,
965+ FromListsN b b,
966+ FromListsN Bool b,
967+ TrivialE b b
999968 ) => (b -> Bool) -> Relation b (Either b b)
1000969guard p = conv (eitherR (predR p) (predR (not . p)))
1001970
@@ -1003,10 +972,10 @@ guard p = conv (eitherR (predR p) (predR (not . p)))
1003972cond ::
1004973 ( Bounded b,
1005974 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)
975+ CountableN b,
976+ FromListsN b b,
977+ FromListsN Bool b,
978+ TrivialE b b
1010979 )
1011980 => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
1012981cond p r s = eitherR r s `comp` guard p
@@ -1016,8 +985,8 @@ cond p r s = eitherR r s `comp` guard p
1016985-- For injective relations, 'domain' and 'ker'nel coincide,
1017986-- since @'ker' r ``sse`` 'identity'@ in such situations.
1018987domain ::
1019− ( KnownNat (I.Count (I.Normalize a)),
1020− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
988+ ( CountableN a,
989+ FromListsN a a
1021990 ) => Relation a b -> Relation a a
1022991domain r = ker r `intersection` identity
1023992
@@ -1026,17 +995,17 @@ domain r = ker r `intersection` identity
1026995-- For functions, 'range' and 'img' (image) coincide,
1027996-- since @'img' f ``sse`` 'identity'@ for any @f@.
1028997range ::
1029− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
1030− KnownNat (I.Count (I.Normalize b))
998+ ( CountableN b,
999+ FromListsN b b
10311000 ) => Relation a b -> Relation b b
10321001range r = img r `intersection` identity
10331002
10341003-- Relation pretty print
10351004
10361005-- | Relation pretty printing
1037−pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1006+pretty :: (CountableN a) => Relation a b -> String
10381007pretty (R a) = I.pretty a
10391008
10401009-- | Relation pretty printing
1041−prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1010+prettyPrint :: (CountableN a) => Relation a b -> IO ()
10421011prettyPrint (R a) = I.prettyPrint a