git.iko.soy/laop
on master help sign in
Added constraint type synonyms to the rest
43fe3c2Armando Santos
src/LAoP/Matrix/Nat.hs+117−125
compare with master
unifiedsplit
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DerivingVia #-}
4{-# LANGUAGE DerivingVia #-}
@@ -53,6 +54,18 @@ module LAoP.Matrix.Nat
53 -- * Type safe matrix representation
54 -- * Type safe matrix representation
54 Matrix (..),
55 Matrix (..),
55
56
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+
56 -- * Primitives
69 -- * Primitives
57 empty,
70 empty,
58 one,
71 one,
@@ -147,6 +160,18 @@ import qualified LAoP.Matrix.Internal as I
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
160newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
161 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
149
162
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+
150-- | It isn't possible to implement the 'id' function so it's
175-- | It isn't possible to implement the 'id' function so it's
151-- implementation is 'undefined'. However 'comp' can be and this partial
176-- implementation is 'undefined'. However 'comp' can be and this partial
152-- class implementation exists just to make the code more readable.
177-- class implementation exists just to make the code more readable.
@@ -165,44 +190,43 @@ one :: e -> Matrix e 1 1
165one = M . I.One
190one = M . I.One
166
191
167junc ::
192junc ::
168− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
193+ (TrivialE a b) =>
169− Matrix e cols1 rows ->
194+ Matrix e a rows ->
170− Matrix e cols2 rows ->
195+ Matrix e b rows ->
171− Matrix e cols3 rows
196+ Matrix e (a + b) rows
172junc (M a) (M b) = M (I.Junc a b)
197junc (M a) (M b) = M (I.Junc a b)
173
198
174infixl 3 |||
199infixl 3 |||
175(|||) ::
200(|||) ::
176− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
201+ (TrivialE a b) =>
177− Matrix e cols1 rows ->
202+ Matrix e a rows ->
178− Matrix e cols2 rows ->
203+ Matrix e b rows ->
179− Matrix e cols3 rows
204+ Matrix e (a + b) rows
180(|||) = junc
205(|||) = junc
181
206
182split ::
207split ::
183− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
208+ (TrivialE a b) =>
184− Matrix e cols rows1 ->
209+ Matrix e cols a ->
185− Matrix e cols rows2 ->
210+ Matrix e cols b ->
186− Matrix e cols rows3
211+ Matrix e cols (a + b)
187split (M a) (M b) = M (I.Split a b)
212split (M a) (M b) = M (I.Split a b)
188
213
189infixl 2 ===
214infixl 2 ===
190(===) ::
215(===) ::
191− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
216+ (TrivialE a b) =>
192− Matrix e cols rows1 ->
217+ Matrix e cols a ->
193− Matrix e cols rows2 ->
218+ Matrix e cols b ->
194− Matrix e cols rows3
219+ Matrix e cols (a + b)
195(===) = split
220(===) = split
196
221
197-- Construction
222-- Construction
198
223
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
200fromLists = M . I.fromLists
225fromLists = M . I.fromLists
201
226
202matrixBuilder ::
227matrixBuilder ::
203− (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
228+ (FromListsN e cols rows, CountableN cols, CountableN rows)
204− ((Int, Int) -> e) ->
205− Matrix e cols rows
229+ => ((Int, Int) -> e) -> Matrix e cols rows
206matrixBuilder = M . I.matrixBuilder
230matrixBuilder = M . I.matrixBuilder
207
231
208col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
232col :: (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
212row = M . I.row
236row = M . I.row
213
237
214fromF ::
238fromF ::
215− ( Bounded a,
239+ ( Liftable e a b,
216− Bounded b,
240+ CountableN cols,
217− Enum a,
241+ CountableN rows,
218− Enum b,
242+ FromListsN e rows cols
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)
225 ) =>
243 ) =>
226 (a -> b) ->
244 (a -> b) ->
227 Matrix e cols rows
245 Matrix e cols rows
228fromF = M . I.fromF
246fromF = M . I.fromF
229
247
230fromF' ::
248fromF' ::
231− ( Bounded a,
249+ ( Liftable e a b,
232− Bounded b,
250+ CountableNz a,
233− Enum a,
251+ CountableNz b,
234− Enum b,
252+ FromListsNz e b a
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)
241 ) =>
253 ) =>
242 (a -> b) ->
254 (a -> b) ->
243 Matrix e (I.Count a) (I.Count b)
255 Matrix e (I.Count a) (I.Count b)
@@ -254,21 +266,21 @@ toList (M m) = I.toList m
254-- Zeros Matrix
266-- Zeros Matrix
255
267
256zeros ::
268zeros ::
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) =>
258 Matrix e cols rows
270 Matrix e cols rows
259zeros = M I.zeros
271zeros = M I.zeros
260
272
261-- Ones Matrix
273-- Ones Matrix
262
274
263ones ::
275ones ::
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) =>
265 Matrix e cols rows
277 Matrix e cols rows
266ones = M I.ones
278ones = M I.ones
267
279
268-- Const Matrix
280-- Const Matrix
269
281
270constant ::
282constant ::
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) =>
272 e ->
284 e ->
273 Matrix e cols rows
285 Matrix e cols rows
274constant = M . I.constant
286constant = M . I.constant
@@ -277,14 +289,14 @@ constant = M . I.constant
277
289
278bang ::
290bang ::
279 forall e cols.
291 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) =>
281 Matrix e cols 1
293 Matrix e cols 1
282bang = M I.bang
294bang = M I.bang
283
295
284-- Identity Matrix
296-- Identity Matrix
285
297
286identity ::
298identity ::
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) =>
288 Matrix e cols cols
300 Matrix e cols cols
289identity = M I.identity
301identity = M I.identity
290
302
@@ -295,22 +307,20 @@ comp (M a) (M b) = M (I.comp a b)
295
307
296p1 ::
308p1 ::
297 ( Num e,
309 ( Num e,
298− KnownNat (I.Count (I.FromNat n)),
310+ CountableDimensionsN n m,
299− KnownNat (I.Count (I.FromNat m)),
311+ FromListsN e n m,
300− I.FromLists e (I.FromNat n) (I.FromNat m),
312+ FromListsN e m m,
301− I.FromLists e (I.FromNat m) (I.FromNat m),
313+ TrivialE m n
302− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
303 ) =>
314 ) =>
304 Matrix e (m + n) m
315 Matrix e (m + n) m
305p1 = M I.p1
316p1 = M I.p1
306
317
307p2 ::
318p2 ::
308 ( Num e,
319 ( Num e,
309− KnownNat (I.Count (I.FromNat n)),
320+ CountableDimensionsN n m,
310− KnownNat (I.Count (I.FromNat m)),
321+ FromListsN e m n,
311− I.FromLists e (I.FromNat m) (I.FromNat n),
322+ FromListsN e n n,
312− I.FromLists e (I.FromNat n) (I.FromNat n),
323+ TrivialE m n
313− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
314 ) =>
324 ) =>
315 Matrix e (m + n) n
325 Matrix e (m + n) n
316p2 = M I.p2
326p2 = M I.p2
@@ -319,138 +329,123 @@ p2 = M I.p2
319
329
320i1 ::
330i1 ::
321 ( Num e,
331 ( Num e,
322− KnownNat (I.Count (I.FromNat n)),
332+ CountableDimensionsN n rows,
323− KnownNat (I.Count (I.FromNat rows)),
333+ FromListsN e n rows,
324− I.FromLists e (I.FromNat n) (I.FromNat rows),
334+ FromListsN e rows rows,
325− I.FromLists e (I.FromNat rows) (I.FromNat rows),
335+ TrivialE rows n
326− I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)
327 ) =>
336 ) =>
328 Matrix e rows (rows + n)
337 Matrix e rows (rows + n)
329i1 = tr p1
338i1 = tr p1
330
339
331i2 ::
340i2 ::
332 ( Num e,
341 ( Num e,
333− KnownNat (I.Count (I.FromNat rows)),
342+ CountableDimensionsN rows m,
334− KnownNat (I.Count (I.FromNat m)),
343+ FromListsN e m rows,
335− I.FromLists e (I.FromNat m) (I.FromNat rows),
344+ FromListsN e rows rows,
336− I.FromLists e (I.FromNat rows) (I.FromNat rows),
345+ TrivialE m rows
337− I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)
338 ) =>
346 ) =>
339 Matrix e rows (m + rows)
347 Matrix e rows (m + rows)
340i2 = tr p2
348i2 = tr p2
341
349
342-- Dimensions
350-- Dimensions
343
351
344−rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
352+rows :: (CountableN rows) => Matrix e cols rows -> Int
345rows (M m) = I.rows m
353rows (M m) = I.rows m
346
354
347−columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
355+columns :: (CountableN cols) => Matrix e cols rows -> Int
348columns (M m) = I.columns m
356columns (M m) = I.columns m
349
357
350−-- Coproduct Bifunctor
358+-- | Coproduct Bifunctor
351−
352infixl 5 -|-
359infixl 5 -|-
353
360
354(-|-) ::
361(-|-) ::
355 ( Num e,
362 ( Num e,
356− KnownNat (I.Count (I.FromNat j)),
363+ CountableDimensionsN j k,
357− KnownNat (I.Count (I.FromNat k)),
364+ FromListsN e k k,
358− I.FromLists e (I.FromNat k) (I.FromNat k),
365+ FromListsN e j k,
359− I.FromLists e (I.FromNat j) (I.FromNat k),
366+ FromListsN e k j,
360− I.FromLists e (I.FromNat k) (I.FromNat j),
367+ FromListsN e j j,
361− I.FromLists e (I.FromNat j) (I.FromNat j),
368+ TrivialE n m,
362− I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),
369+ TrivialE k j
363− I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)
364 ) =>
370 ) =>
365 Matrix e n k ->
371 Matrix e n k ->
366 Matrix e m j ->
372 Matrix e m j ->
367 Matrix e (n + m) (k + j)
373 Matrix e (n + m) (k + j)
368(-|-) (M a) (M b) = M ((I.-|-) a b)
374(-|-) (M a) (M b) = M ((I.-|-) a b)
369
375
370−-- Khatri Rao Product and projections
376+-- | Khatri Rao Product and projections
371−
372kp1 ::
377kp1 ::
373 forall e m k .
378 forall e m k .
374 ( Num e,
379 ( Num e,
375− KnownNat (I.Count (I.FromNat m)),
380+ CountableDimensionsN m k,
376− KnownNat (I.Count (I.FromNat k)),
381+ CountableN (m * k),
377− KnownNat (I.Count (I.FromNat (m * k))),
382+ FromListsN e (m * k) m,
378− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
383+ TrivialP m k
379− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
380 ) => Matrix e (m * k) m
384 ) => Matrix e (m * k) m
381kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
385kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
382
386
383kp2 ::
387kp2 ::
384 forall e m k.
388 forall e m k.
385 ( Num e,
389 ( Num e,
386− KnownNat (I.Count (I.FromNat k)),
390+ CountableDimensionsN k m,
387− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
391+ FromListsN e (m * k) k,
388− KnownNat (I.Count (I.FromNat m)),
392+ CountableN (m * k),
389− KnownNat (I.Count (I.FromNat (m * k))),
393+ TrivialP m k
390− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
391 ) => Matrix e (m * k) k
394 ) => Matrix e (m * k) k
392kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
395kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
393
396
394khatri ::
397khatri ::
395 forall e cols a b.
398 forall e cols a b.
396 ( Num e,
399 ( Num e,
397− KnownNat (I.Count (I.FromNat a)),
400+ CountableDimensionsN a b,
398− KnownNat (I.Count (I.FromNat b)),
401+ CountableN (a * b),
399− KnownNat (I.Count (I.FromNat (a * b))),
402+ FromListsN e (a * b) a,
400− I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
403+ FromListsN e (a * b) b,
401− I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
404+ TrivialP a b
402− I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
403 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
405 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
404khatri a b =
406khatri a b =
405 let kp1' = kp1 @e @a @b
407 let kp1' = kp1 @e @a @b
406 kp2' = kp2 @e @a @b
408 kp2' = kp2 @e @a @b
407 in comp (tr kp1') a * comp (tr kp2') b
409 in comp (tr kp1') a * comp (tr kp2') b
408
410
409−-- Product Bifunctor (Kronecker)
411+-- | Product Bifunctor (Kronecker)
410−
411infixl 4 ><
412infixl 4 ><
412
413
413(><) ::
414(><) ::
414 forall e m p n q.
415 forall e m p n q.
415 ( Num e,
416 ( Num e,
416− KnownNat (I.Count (I.FromNat m)),
417+ CountableDimensionsN m n,
417− KnownNat (I.Count (I.FromNat n)),
418+ CountableDimensionsN p q,
418− KnownNat (I.Count (I.FromNat p)),
419+ CountableDimensionsN (m * n) (p * q),
419− KnownNat (I.Count (I.FromNat q)),
420+ FromListsN e (m * n) m,
420− KnownNat (I.Count (I.FromNat (m * n))),
421+ FromListsN e (m * n) n,
421− KnownNat (I.Count (I.FromNat (p * q))),
422+ FromListsN e (p * q) p,
422− I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
423+ FromListsN e (p * q) q,
423− I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
424+ TrivialP m n,
424− I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
425+ TrivialP p q
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))
428 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
426 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
429(><) a b =
427(><) a b =
430 let kp1' = kp1 @e @m @n
428 let kp1' = kp1 @e @m @n
431 kp2' = kp2 @e @m @n
429 kp2' = kp2 @e @m @n
432 in khatri (comp a kp1') (comp b kp2')
430 in khatri (comp a kp1') (comp b kp2')
433
431
434−-- Matrix abide Junc Split
432+-- | Matrix abide Junc Split
435−
436abideJS :: Matrix e cols rows -> Matrix e cols rows
433abideJS :: Matrix e cols rows -> Matrix e cols rows
437abideJS (M m) = M (I.abideJS m)
434abideJS (M m) = M (I.abideJS m)
438
435
439−-- Matrix abide Split Junc
436+-- | Matrix abide Split Junc
440−
441abideSJ :: Matrix e cols rows -> Matrix e cols rows
437abideSJ :: Matrix e cols rows -> Matrix e cols rows
442abideSJ (M m) = M (I.abideSJ m)
438abideSJ (M m) = M (I.abideSJ m)
443
439
444−-- Matrix transposition
440+-- | Matrix transposition
445−
446tr :: Matrix e cols rows -> Matrix e rows cols
441tr :: Matrix e cols rows -> Matrix e rows cols
447tr (M m) = M (I.tr m)
442tr (M m) = M (I.tr m)
448
443
449-- Selective 'select' operator
444-- Selective 'select' operator
450select ::
445select ::
451 ( Num e,
446 ( Num e,
452− I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
447+ FromListsN e rows1 rows1,
453− KnownNat (I.Count (I.FromNat rows1)),
448+ CountableN rows1,
454 I.FromNat rows2 ~ I.FromNat rows1,
449 I.FromNat rows2 ~ I.FromNat rows1,
455 I.FromNat cols1 ~ I.FromNat cols2,
450 I.FromNat cols1 ~ I.FromNat cols2,
456 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
451 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -461,14 +456,11 @@ select (M m) (M y) = M (I.select m y)
461
456
462cond ::
457cond ::
463 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
458 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
464− KnownNat (I.Count (I.FromNat cols)),
459+ CountableN cols,
465 I.FromLists e () (I.FromNat cols),
460 I.FromLists e () (I.FromNat cols),
466 I.FromLists e (I.FromNat cols) (),
461 I.FromLists e (I.FromNat cols) (),
467− I.FromLists e (I.FromNat cols) (I.FromNat cols),
462+ FromListsN e cols cols,
468− Bounded a,
463+ Liftable e a Bool
469− Enum a,
470− Num e,
471− Ord e
472 )
464 )
473 =>
465 =>
474 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
466 (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)
476
468
477-- Pretty print
469-- Pretty print
478
470
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
480pretty (M m) = I.pretty m
472pretty (M m) = I.pretty m
481
473
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 ()
483prettyPrint (M m) = I.prettyPrint m
475prettyPrint (M m) = I.prettyPrint m
src/LAoP/Matrix/Type.hs+11
@@ -56,6 +56,17 @@ module LAoP.Matrix.Type
56 -- * Type safe matrix representation
56 -- * Type safe matrix representation
57 Matrix (..),
57 Matrix (..),
58
58
59+ -- * Constraint type aliases
60+ Countable,
61+ CountableDimensions,
62+ CountableN,
63+ CountableDimensionsN,
64+ FromListsN,
65+ Liftable,
66+ Trivial,
67+ TrivialE,
68+ TrivialP,
69+
59 -- * Type aliases
70 -- * Type aliases
60 Zero,
71 Zero,
61 One,
72 One,
src/LAoP/Relation.hs+12
@@ -30,6 +30,18 @@ module LAoP.Relation
30 Relation (..),
30 Relation (..),
31 Boolean,
31 Boolean,
32
32
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+
33 -- * Primitives
45 -- * Primitives
34 empty,
46 empty,
35 one,
47 one,
src/LAoP/Relation/Internal.hs+177−208
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE GADTs #-}
2{-# LANGUAGE GADTs #-}
2{-# LANGUAGE UndecidableInstances #-}
3{-# LANGUAGE UndecidableInstances #-}
3{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleContexts #-}
@@ -39,6 +40,18 @@ module LAoP.Relation.Internal
39 Relation (..),
40 Relation (..),
40 Boolean,
41 Boolean,
41
42
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+
42 -- * Primitives
55 -- * Primitives
43 empty,
56 empty,
44 one,
57 one,
@@ -179,6 +192,18 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
179
192
180deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
181
194
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+
182-- | It isn't possible to implement the 'id' function so it's
207-- | It isn't possible to implement the 'id' function so it's
183-- implementation is 'undefined'. However 'comp' can be and this partial
208-- implementation is 'undefined'. However 'comp' can be and this partial
184-- class implementation exists just to make the code more readable.
209-- class implementation exists just to make the code more readable.
@@ -218,7 +243,7 @@ one = R . I.One
218-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
243-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
219--
244--
220-- See 'eitherR'.
245-- See 'eitherR'.
221−junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
246+junc :: (TrivialE a b)
222 => Relation a c -> Relation b c -> Relation (Either a b) c
247 => Relation a c -> Relation b c -> Relation (Either a b) c
223junc (R a) (R b) = R (I.Junc a b)
248junc (R a) (R b) = R (I.Junc a b)
224
249
@@ -227,21 +252,21 @@ infixl 3 |||
227--
252--
228-- See 'eitherR'.
253-- See 'eitherR'.
229(|||) ::
254(|||) ::
230− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
255+ (TrivialE a b) =>
231 Relation a c ->
256 Relation a c ->
232 Relation b c ->
257 Relation b c ->
233 Relation (Either a b) c
258 Relation (Either a b) c
234(|||) = junc
259(|||) = junc
235
260
236-- | Boolean Matrix 'Split' constructor, also known as relational product.
261-- | 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)
238 => Relation c a -> Relation c b -> Relation c (Either a b)
263 => Relation c a -> Relation c b -> Relation c (Either a b)
239split (R a) (R b) = R (I.Split a b)
264split (R a) (R b) = R (I.Split a b)
240
265
241infixl 2 ===
266infixl 2 ===
242-- | Boolean Matrix 'Split' constructor
267-- | Boolean Matrix 'Split' constructor
243(===) ::
268(===) ::
244− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
269+ (TrivialE a b) =>
245 Relation c a ->
270 Relation c a ->
246 Relation c b ->
271 Relation c b ->
247 Relation c (Either a b)
272 Relation c (Either a b)
@@ -251,15 +276,14 @@ infixl 2 ===
251
276
252-- | Build a matrix out of a list of list of elements. Throws a runtime
277-- | Build a matrix out of a list of list of elements. Throws a runtime
253-- error if the dimensions do not match.
278-- 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
255fromLists = R . I.fromLists
280fromLists = R . I.fromLists
256
281
257-- | Matrix builder function. Constructs a matrix provided with
282-- | Matrix builder function. Constructs a matrix provided with
258-- a construction function.
283-- a construction function.
259relationBuilder ::
284relationBuilder ::
260− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
285+ (FromListsN a b, CountableDimensionsN a b) =>
261− ((Int, Int) -> Boolean) ->
286+ ((Int, Int) -> Boolean) -> Relation a b
262− Relation a b
263relationBuilder = R . I.matrixBuilder
287relationBuilder = R . I.matrixBuilder
264
288
265-- | Lifts functions to matrices with arbitrary dimensions.
289-- | Lifts functions to matrices with arbitrary dimensions.
@@ -267,14 +291,9 @@ relationBuilder = R . I.matrixBuilder
267-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
291-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
268-- types @a@ or @b@ allows.
292-- types @a@ or @b@ allows.
269fromF ::
293fromF ::
270− ( Bounded a,
294+ ( Liftable a b,
271− Bounded b,
295+ CountableDimensionsN c d,
272− Enum a,
296+ FromListsN d c
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 )
297 )
279 => (a -> b) -> Relation c d
298 => (a -> b) -> Relation c d
280fromF f = R (I.fromFRel f)
299fromF f = R (I.fromFRel f)
@@ -282,44 +301,29 @@ fromF f = R (I.fromFRel f)
282-- | Lifts functions to matrices with dimensions matching @a@ and @b@
301-- | Lifts functions to matrices with dimensions matching @a@ and @b@
283-- cardinality's.
302-- cardinality's.
284fromF' ::
303fromF' ::
285− ( Bounded b,
304+ ( Liftable a b,
286− Bounded a,
305+ CountableDimensionsN a b,
287− Enum a,
306+ FromListsN b 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 )
307 )
294 => (a -> b) -> Relation a b
308 => (a -> b) -> Relation a b
295fromF' f = R (I.fromFRel' f)
309fromF' f = R (I.fromFRel' f)
296
310
297-- | Lifts relation functions to 'Relation'
311-- | Lifts relation functions to 'Relation'
298toRel ::
312toRel ::
299− ( Bounded b,
313+ ( Liftable a b,
300− Bounded a,
314+ CountableDimensionsN a b,
301− Enum a,
315+ FromListsN b 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 )
316 )
308− => (a -> b -> Bool) -> Relation a b
317+ => (a -> b -> Bool) -> Relation a b
309toRel = R . I.toRel
318toRel = R . I.toRel
310
319
311-- | Lowers a 'Relation' to a function
320-- | Lowers a 'Relation' to a function
312fromRel ::
321fromRel ::
313− ( Bounded a,
322+ ( Liftable a b,
314− Bounded b,
315− Enum a,
316− Enum b,
317 Eq a,
323 Eq a,
318− Eq b,
324+ CountableDimensionsN a b,
319− KnownNat (I.Count (I.Normalize a)),
325+ FromListsN a One,
320− KnownNat (I.Count (I.Normalize b)),
326+ FromListsN b One
321− I.FromLists Boolean (I.Normalize a) One,
322− I.FromLists Boolean (I.Normalize b) One
323 )
327 )
324 => Relation a b -> (a -> b -> Bool)
328 => Relation a b -> (a -> b -> Bool)
325fromRel r a b = pointApBool a b r
329fromRel r a b = pointApBool a b r
@@ -344,16 +348,11 @@ toBool r = case toList r of
344--
348--
345-- Maps a relation to a set valued function.
349-- Maps a relation to a set valued function.
346pt ::
350pt ::
347− ( Bounded a,
351+ ( Liftable a b,
348− Bounded b,
349− Enum a,
350− Enum b,
351 Eq a,
352 Eq a,
352− Eq b,
353+ CountableDimensionsN a b,
353− KnownNat (I.Count (I.Normalize a)),
354+ FromListsN a One,
354− KnownNat (I.Count (I.Normalize b)),
355+ FromListsN b One
355− I.FromLists Boolean (I.Normalize a) One,
356− I.FromLists Boolean (I.Normalize b) One
357 )
356 )
358 => Relation a b -> (a -> Powerset b)
357 => Relation a b -> (a -> Powerset b)
359pt r a =
358pt r a =
@@ -365,9 +364,8 @@ belongs ::
365 ( Bounded a,
364 ( Bounded a,
366 Enum a,
365 Enum a,
367 Eq a,
366 Eq a,
368− KnownNat (I.Count (I.Normalize (Powerset a))),
367+ CountableDimensionsN (Powerset a) a,
369− KnownNat (I.Count (I.Normalize a)),
368+ FromListsN a (Powerset a)
370− I.FromLists Boolean (I.Normalize a) (I.Normalize (Powerset a))
371 )
369 )
372 => Relation (Powerset a) a
370 => Relation (Powerset a) a
373belongs = toRel (flip elemR)
371belongs = toRel (flip elemR)
@@ -386,7 +384,7 @@ belongs = toRel (flip elemR)
386-- ⊥ ``sse`` R && R ``sse`` T == True
384-- ⊥ ``sse`` R && R ``sse`` T == True
387-- @
385-- @
388zeros ::
386zeros ::
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) =>
390 Relation a b
388 Relation a b
391zeros = relationBuilder (const (nat 0))
389zeros = relationBuilder (const (nat 0))
392
390
@@ -401,7 +399,7 @@ zeros = relationBuilder (const (nat 0))
401-- ⊥ ``sse`` R && R ``sse`` T == True
399-- ⊥ ``sse`` R && R ``sse`` T == True
402-- @
400-- @
403ones ::
401ones ::
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) =>
405 Relation a b
403 Relation a b
406ones = relationBuilder (const (nat 1))
404ones = relationBuilder (const (nat 1))
407
405
@@ -409,7 +407,7 @@ ones = relationBuilder (const (nat 1))
409
407
410-- | The T (Top) row vector relation.
408-- | The T (Top) row vector relation.
411bang ::
409bang ::
412− (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
410+ (FromListsN a One, CountableN a) =>
413 Relation a One
411 Relation a One
414bang = ones
412bang = ones
415
413
@@ -418,8 +416,8 @@ point ::
418 ( Bounded a,
416 ( Bounded a,
419 Enum a,
417 Enum a,
420 Eq a,
418 Eq a,
421− KnownNat (I.Count (I.Normalize a)),
419+ CountableN a,
422− I.FromLists Boolean (I.Normalize a) One
420+ FromListsN a One
423 ) => a -> Relation One a
421 ) => a -> Relation One a
424point = fromF' . const
422point = fromF' . const
425
423
@@ -431,8 +429,7 @@ point = fromF' . const
431-- 'identity' ``comp`` r == r == r ``comp`` 'identity'
429-- 'identity' ``comp`` r == r == r ``comp`` 'identity'
432-- @
430-- @
433identity ::
431identity ::
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
436identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
433identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
437
434
438-- | Relational composition
435-- | Relational composition
@@ -486,8 +483,8 @@ shrunkBy r s = r `intersection` divR s (conv r)
486-- r ``overriddenBy`` r == r
483-- r ``overriddenBy`` r == r
487-- @
484-- @
488overriddenBy ::
485overriddenBy ::
489− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
486+ ( FromListsN b b,
490− KnownNat (I.Count (I.Normalize b))
487+ CountableN b
491 ) => Relation a b -> Relation a b -> Relation a b
488 ) => Relation a b -> Relation a b -> Relation a b
492overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
489overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
493
490
@@ -496,16 +493,11 @@ overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
496-- If @a@ and @b@ are related by 'Relation' @r@
493-- If @a@ and @b@ are related by 'Relation' @r@
497-- then @'pointAp' a b r == 'one' ('nat' 1)@
494-- then @'pointAp' a b r == 'one' ('nat' 1)@
498pointAp ::
495pointAp ::
499− ( Bounded a,
496+ ( Liftable a b,
500− Bounded b,
501− Enum a,
502− Enum b,
503 Eq a,
497 Eq a,
504− Eq b,
498+ CountableDimensionsN a b,
505− KnownNat (I.Count (I.Normalize a)),
499+ FromListsN a One,
506− KnownNat (I.Count (I.Normalize b)),
500+ FromListsN b One
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
501 ) => a -> b -> Relation a b -> Relation One One
510pointAp a b r = conv (point b) `comp` r `comp` point a
502pointAp a b r = conv (point b) `comp` r `comp` point a
511
503
@@ -513,16 +505,11 @@ pointAp a b r = conv (point b) `comp` r `comp` point a
513--
505--
514-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
506-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
515pointApBool ::
507pointApBool ::
516− ( Bounded a,
508+ ( Liftable a b,
517− Bounded b,
518− Enum a,
519− Enum b,
520 Eq a,
509 Eq a,
521− Eq b,
510+ CountableDimensionsN a b,
522− KnownNat (I.Count (I.Normalize a)),
511+ FromListsN a One,
523− KnownNat (I.Count (I.Normalize b)),
512+ FromListsN b One
524− I.FromLists Boolean (I.Normalize a) One,
525− I.FromLists Boolean (I.Normalize b) One
526 ) => a -> b -> Relation a b -> Bool
513 ) => a -> b -> Relation a b -> Bool
527pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
514pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
528
515
@@ -602,19 +589,19 @@ divisionF f g = conv g `comp` f
602-- Taxonomy of binary relations
589-- Taxonomy of binary relations
603
590
604-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
591-- | 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
606simple = coreflexive . img
593simple = coreflexive . img
607
594
608-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
595-- | 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
610injective = coreflexive . ker
597injective = coreflexive . ker
611
598
612-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
599-- | 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
614entire = reflexive . ker
601entire = reflexive . ker
615
602
616-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
603-- | 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
618surjective = reflexive . img
605surjective = reflexive . img
619
606
620-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
607-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
@@ -627,68 +614,63 @@ surjective = reflexive . img
627-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
614-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
628-- @
615-- @
629function ::
616function ::
630− ( KnownNat (I.Count (I.Normalize b)),
617+ ( CountableDimensionsN a b,
631− KnownNat (I.Count (I.Normalize a)),
618+ FromListsN a a,
632− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
619+ FromListsN b b
633− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
634 )
620 )
635 => Relation a b -> Bool
621 => Relation a b -> Bool
636function r = simple r && entire r
622function r = simple r && entire r
637
623
638-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
624-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
639representation ::
625representation ::
640− ( KnownNat (I.Count (I.Normalize a)),
626+ ( CountableN a,
641− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
627+ FromListsN a a
642 )
628 )
643 => Relation a b -> Bool
629 => Relation a b -> Bool
644representation r = injective r && entire r
630representation r = injective r && entire r
645
631
646-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
632-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
647abstraction ::
633abstraction ::
648− ( KnownNat (I.Count (I.Normalize b)),
634+ ( CountableN b,
649− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
635+ FromListsN b b
650 )
636 )
651 => Relation a b -> Bool
637 => Relation a b -> Bool
652abstraction r = surjective r && simple r
638abstraction r = surjective r && simple r
653
639
654-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
640-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
655surjection ::
641surjection ::
656− ( KnownNat (I.Count (I.Normalize b)),
642+ ( CountableDimensionsN a b,
657− KnownNat (I.Count (I.Normalize a)),
643+ FromListsN a a,
658− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
644+ FromListsN b b
659− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
660 )
645 )
661 => Relation a b -> Bool
646 => Relation a b -> Bool
662surjection r = function r && abstraction r
647surjection r = function r && abstraction r
663
648
664-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
649-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
665injection ::
650injection ::
666− ( KnownNat (I.Count (I.Normalize b)),
651+ ( CountableDimensionsN a b,
667− KnownNat (I.Count (I.Normalize a)),
652+ FromListsN a a,
668− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
653+ FromListsN b b
669− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
670 )
654 )
671 => Relation a b -> Bool
655 => Relation a b -> Bool
672injection r = function r && representation r
656injection r = function r && representation r
673
657
674-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
658-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
675bijection ::
659bijection ::
676− ( KnownNat (I.Count (I.Normalize b)),
660+ ( CountableDimensionsN a b,
677− KnownNat (I.Count (I.Normalize a)),
661+ FromListsN b b,
678− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
662+ FromListsN a a
679− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
680 ) => Relation a b -> Bool
663 ) => Relation a b -> Bool
681bijection r = injection r && surjection r
664bijection r = injection r && surjection r
682
665
683−
684-- Properties of relations
666-- Properties of relations
685
667
686-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' ``sse`` r@
668-- | 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
688reflexive r = identity <= r
670reflexive r = identity <= r
689
671
690-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'identity'@
672-- | 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
692coreflexive r = r <= identity
674coreflexive r = r <= identity
693
675
694-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
676-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
@@ -700,35 +682,35 @@ symmetric :: Relation a a -> Bool
700symmetric r = r == conv r
682symmetric r = r == conv r
701
683
702-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'identity'@
684-- | 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
704antiSymmetric r = (r `intersection` conv r) `sse` identity
686antiSymmetric r = (r `intersection` conv r) `sse` identity
705
687
706-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'identity') == 'zeros'@
688-- | 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
708irreflexive r = (r `intersection` identity) == zeros
690irreflexive r = (r `intersection` identity) == zeros
709
691
710-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
692-- | 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
712connected r = (r `union` conv r) == ones
694connected r = (r `union` conv r) == ones
713
695
714-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
696-- | 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
716preorder r = reflexive r && transitive r
698preorder r = reflexive r && transitive r
717
699
718-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
700-- | 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
720partialOrder r = antiSymmetric r && preorder r
702partialOrder r = antiSymmetric r && preorder r
721
703
722-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
704-- | 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
724linearOrder r = connected r && partialOrder r
706linearOrder r = connected r && partialOrder r
725
707
726-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
708-- | 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
728equivalence r = symmetric r && preorder r
710equivalence r = symmetric r && preorder r
729
711
730-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
712-- | 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
732partialEquivalence r = partialOrder r && equivalence r
714partialEquivalence r = partialOrder r && equivalence r
733
715
734-- | A 'Relation' @r@ is 'difunctional' or regular wherever
716-- | A 'Relation' @r@ is 'difunctional' or regular wherever
@@ -760,12 +742,11 @@ difunctional r = r `comp` conv r `comp` r == r
760-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
742-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
761-- @
743-- @
762splitR ::
744splitR ::
763− ( KnownNat (I.Count (I.Normalize a)),
745+ ( CountableDimensionsN a b,
764− KnownNat (I.Count (I.Normalize b)),
746+ CountableN (a, b),
765− KnownNat (I.Count (I.Normalize (a, b))),
747+ FromListsN (a, b) a,
766− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
748+ FromListsN (a, b) b,
767− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
749+ TrivialP a b
768− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
769 )
750 )
770 => Relation c a -> Relation c b -> Relation c (a, b)
751 => Relation c a -> Relation c b -> Relation c (a, b)
771splitR (R f) (R g) = R (I.khatri f g)
752splitR (R f) (R g) = R (I.khatri f g)
@@ -777,11 +758,10 @@ splitR (R f) (R g) = R (I.khatri f g)
777-- @
758-- @
778p1 ::
759p1 ::
779 forall a b .
760 forall a b .
780− ( KnownNat (I.Count (I.Normalize a)),
761+ ( CountableDimensionsN a b,
781− KnownNat (I.Count (I.Normalize b)),
762+ CountableN (a, b),
782− KnownNat (I.Count (I.Normalize (a, b))),
763+ FromListsN (a, b) a,
783− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
764+ TrivialP a b
784− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
785 )
765 )
786 => Relation (a, b) a
766 => Relation (a, b) a
787p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
767p1 = 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))
793-- @
773-- @
794p2 ::
774p2 ::
795 forall a b .
775 forall a b .
796− ( KnownNat (I.Count (I.Normalize b)),
776+ ( CountableDimensionsN a b,
797− KnownNat (I.Count (I.Normalize a)),
777+ CountableN (a, b),
798− KnownNat (I.Count (I.Normalize (a, b))),
778+ FromListsN (a, b) b,
799− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
779+ TrivialP a b
800− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
801 )
780 )
802 => Relation (a, b) b
781 => Relation (a, b) b
803p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
782p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
@@ -812,18 +791,15 @@ infixl 4 ><
812-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
791-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
813-- @
792-- @
814(><) ::
793(><) ::
815− ( KnownNat (I.Count (I.Normalize a)),
794+ ( CountableDimensionsN a b,
816− KnownNat (I.Count (I.Normalize b)),
795+ CountableDimensionsN c d,
817− KnownNat (I.Count (I.Normalize c)),
796+ CountableDimensionsN (a, c) (b, d),
818− KnownNat (I.Count (I.Normalize d)),
797+ FromListsN (a, c) a,
819− KnownNat (I.Count (I.Normalize (a, c))),
798+ FromListsN (a, c) c,
820− KnownNat (I.Count (I.Normalize (b, d))),
799+ FromListsN (b, d) b,
821− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),
800+ FromListsN (b, d) d,
822− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),
801+ TrivialP a c,
823− I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),
802+ TrivialP b d
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 )
803 )
828 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
804 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
829(><) (R a) (R b) = R ((I.><) a b)
805(><) (R a) (R b) = R ((I.><) a b)
@@ -845,7 +821,7 @@ infixl 4 ><
845-- @
821-- @
846-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
822-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
847-- @
823-- @
848−eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
824+eitherR :: (TrivialE a b)
849 => Relation a c -> Relation b c -> Relation (Either a b) c
825 => Relation a c -> Relation b c -> Relation (Either a b) c
850eitherR = junc
826eitherR = junc
851
827
@@ -856,11 +832,10 @@ eitherR = junc
856-- 'i1' ``comp`` 'i2' = 'zeros'
832-- 'i1' ``comp`` 'i2' = 'zeros'
857-- @
833-- @
858i1 ::
834i1 ::
859− ( KnownNat (I.Count (I.Normalize b)),
835+ ( CountableDimensionsN a b,
860− KnownNat (I.Count (I.Normalize a)),
836+ FromListsN b a,
861− I.FromLists Boolean (I.Normalize b) (I.Normalize a),
837+ FromListsN a a,
862− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
838+ TrivialE a b
863− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
864 )
839 )
865 => Relation a (Either a b)
840 => Relation a (Either a b)
866i1 = R I.i1
841i1 = R I.i1
@@ -872,11 +847,10 @@ i1 = R I.i1
872-- 'i1' ``comp`` 'i2' = 'zeros'
847-- 'i1' ``comp`` 'i2' = 'zeros'
873-- @
848-- @
874i2 ::
849i2 ::
875− ( KnownNat (I.Count (I.Normalize b)),
850+ ( CountableDimensionsN a b,
876− KnownNat (I.Count (I.Normalize a)),
851+ FromListsN a b,
877− I.FromLists Boolean (I.Normalize a) (I.Normalize b),
852+ FromListsN b b,
878− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
853+ TrivialE a b
879− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
880 )
854 )
881 => Relation b (Either a b)
855 => Relation b (Either a b)
882i2 = R I.i2
856i2 = R I.i2
@@ -889,14 +863,13 @@ infixl 5 -|-
889-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
863-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
890-- @
864-- @
891(-|-) ::
865(-|-) ::
892− ( KnownNat (I.Count (I.Normalize d)),
866+ ( CountableDimensionsN b d,
893− KnownNat (I.Count (I.Normalize b)),
867+ FromListsN b b,
894− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
868+ FromListsN d b,
895− I.FromLists Boolean (I.Normalize d) (I.Normalize b),
869+ FromListsN b d,
896− I.FromLists Boolean (I.Normalize b) (I.Normalize d),
870+ FromListsN d d,
897− I.FromLists Boolean (I.Normalize d) (I.Normalize d),
871+ TrivialE a c,
898− I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),
872+ TrivialE b d
899− I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)
900 )
873 )
901 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
874 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
902(-|-) (R a) (R b) = R ((I.-|-) a b)
875(-|-) (R a) (R b) = R ((I.-|-) a b)
@@ -909,19 +882,17 @@ infixl 5 -|-
909-- 'trans'/'untrans';
882-- 'trans'/'untrans';
910-- more-over, where each particular attribute is placed (input/output) is irrelevant.
883-- more-over, where each particular attribute is placed (input/output) is irrelevant.
911trans ::
884trans ::
912− ( KnownNat (I.Count (I.Normalize (a, b))),
885+ ( CountableDimensionsN a b,
913− KnownNat (I.Count (I.Normalize a)),
886+ CountableN c,
914− KnownNat (I.Count (I.Normalize (c, b))),
887+ CountableDimensionsN (a, b) (c, b),
915− KnownNat (I.Count (I.Normalize b)),
888+ FromListsN (c, b) c,
916− KnownNat (I.Count (I.Normalize c)),
889+ FromListsN (c, b) b,
917− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
890+ FromListsN (a, b) a,
918− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
891+ FromListsN (a, b) b,
919− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
892+ Trivial (a, b),
920− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
893+ Trivial (c, b),
921− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
894+ TrivialP2 a b,
922− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
895+ TrivialP2 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 )
896 )
926 => Relation (a, b) c -> Relation a (c, b)
897 => Relation (a, b) c -> Relation a (c, b)
927trans r = splitR r p2 `comp` conv p1
898trans r = splitR r p2 `comp` conv p1
@@ -932,19 +903,17 @@ trans r = splitR r p2 `comp` conv p1
932-- 'trans'/'untrans';
903-- 'trans'/'untrans';
933-- more-over, where each particular attribute is placed (input/output) is irrelevant.
904-- more-over, where each particular attribute is placed (input/output) is irrelevant.
934untrans ::
905untrans ::
935− ( KnownNat (I.Count (I.Normalize (a, b))),
906+ ( CountableDimensionsN a b,
936− KnownNat (I.Count (I.Normalize a)),
907+ CountableN c,
937− KnownNat (I.Count (I.Normalize (c, b))),
908+ CountableDimensionsN (a, b) (c, b),
938− KnownNat (I.Count (I.Normalize b)),
909+ FromListsN (c, b) c,
939− KnownNat (I.Count (I.Normalize c)),
910+ FromListsN (c, b) b,
940− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
911+ FromListsN (a, b) b,
941− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
912+ FromListsN (a, b) a,
942− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
913+ Trivial (a, b),
943− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
914+ Trivial (c, b),
944− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
915+ TrivialP2 a b,
945− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
916+ TrivialP2 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 )
917 )
949 => Relation a (c, b) -> Relation (a, b) c
918 => Relation a (c, b) -> Relation (a, b) c
950untrans s = p1 `comp` conv (splitR (conv s) p2)
919untrans s = p1 `comp` conv (splitR (conv s) p2)
@@ -962,9 +931,9 @@ untrans s = p1 `comp` conv (splitR (conv s) p2)
962predR ::
931predR ::
963 ( Bounded a,
932 ( Bounded a,
964 Enum a,
933 Enum a,
965− KnownNat (I.Count (I.Normalize a)),
934+ CountableN a,
966− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
935+ FromListsN a a,
967− I.FromLists Boolean (I.Normalize Bool) (I.Normalize a)
936+ FromListsN Bool a
968 )
937 )
969 => (a -> Bool) -> Relation a a
938 => (a -> Bool) -> Relation a a
970predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
939predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
@@ -978,8 +947,8 @@ predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
978-- 'equalizer' ('point' True) ('point' False) == 'zeros'
947-- 'equalizer' ('point' True) ('point' False) == 'zeros'
979-- @
948-- @
980equalizer ::
949equalizer ::
981− ( KnownNat (I.Count (I.Normalize a)),
950+ ( CountableN a,
982− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
951+ FromListsN a a
983 )
952 )
984 => Relation a b -> Relation a b -> Relation a a
953 => Relation a b -> Relation a b -> Relation a a
985equalizer f g = identity `intersection` divisionF f g
954equalizer f g = identity `intersection` divisionF f g
@@ -992,10 +961,10 @@ equalizer f g = identity `intersection` divisionF f g
992guard ::
961guard ::
993 ( Bounded b,
962 ( Bounded b,
994 Enum b,
963 Enum b,
995− KnownNat (I.Count (I.Normalize b)),
964+ CountableN b,
996− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
965+ FromListsN b b,
997− I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
966+ FromListsN Bool b,
998− I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
967+ TrivialE b b
999 ) => (b -> Bool) -> Relation b (Either b b)
968 ) => (b -> Bool) -> Relation b (Either b b)
1000guard p = conv (eitherR (predR p) (predR (not . p)))
969guard p = conv (eitherR (predR p) (predR (not . p)))
1001
970
@@ -1003,10 +972,10 @@ guard p = conv (eitherR (predR p) (predR (not . p)))
1003cond ::
972cond ::
1004 ( Bounded b,
973 ( Bounded b,
1005 Enum b,
974 Enum b,
1006− KnownNat (I.Count (I.Normalize b)),
975+ CountableN b,
1007− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
976+ FromListsN b b,
1008− I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
977+ FromListsN Bool b,
1009− I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
978+ TrivialE b b
1010 )
979 )
1011 => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
980 => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
1012cond p r s = eitherR r s `comp` guard p
981cond p r s = eitherR r s `comp` guard p
@@ -1016,8 +985,8 @@ cond p r s = eitherR r s `comp` guard p
1016-- For injective relations, 'domain' and 'ker'nel coincide,
985-- For injective relations, 'domain' and 'ker'nel coincide,
1017-- since @'ker' r ``sse`` 'identity'@ in such situations.
986-- since @'ker' r ``sse`` 'identity'@ in such situations.
1018domain ::
987domain ::
1019− ( KnownNat (I.Count (I.Normalize a)),
988+ ( CountableN a,
1020− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
989+ FromListsN a a
1021 ) => Relation a b -> Relation a a
990 ) => Relation a b -> Relation a a
1022domain r = ker r `intersection` identity
991domain r = ker r `intersection` identity
1023
992
@@ -1026,17 +995,17 @@ domain r = ker r `intersection` identity
1026-- For functions, 'range' and 'img' (image) coincide,
995-- For functions, 'range' and 'img' (image) coincide,
1027-- since @'img' f ``sse`` 'identity'@ for any @f@.
996-- since @'img' f ``sse`` 'identity'@ for any @f@.
1028range ::
997range ::
1029− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
998+ ( CountableN b,
1030− KnownNat (I.Count (I.Normalize b))
999+ FromListsN b b
1031 ) => Relation a b -> Relation b b
1000 ) => Relation a b -> Relation b b
1032range r = img r `intersection` identity
1001range r = img r `intersection` identity
1033
1002
1034-- Relation pretty print
1003-- Relation pretty print
1035
1004
1036-- | Relation pretty printing
1005-- | Relation pretty printing
1037−pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1006+pretty :: (CountableN a) => Relation a b -> String
1038pretty (R a) = I.pretty a
1007pretty (R a) = I.pretty a
1039
1008
1040-- | Relation pretty printing
1009-- | Relation pretty printing
1041−prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1010+prettyPrint :: (CountableN a) => Relation a b -> IO ()
1042prettyPrint (R a) = I.prettyPrint a
1011prettyPrint (R a) = I.prettyPrint a