9e8b43c · laop · git.iko.soy

git.iko.soy/laop

Merge pull request #3 from bolt12/constraints

Constraints

commit9e8b43c796262b11e519514b0ee26e46269d9c46 authorArmando Santos <armandoifsantos@gmail.com> dateFri 31 Jan 2020, 20:15 (7 years ago) parent9592019 43fe3c2

5 files changed+488−565

compare with master

unifiedsplit

src/LAoP/Matrix/Internal.hs+59−86 src/LAoP/Matrix/Nat.hs+117−125 src/LAoP/Matrix/Type.hs+123−146 src/LAoP/Relation.hs+12 src/LAoP/Relation/Internal.hs+177−208

src/LAoP/Matrix/Internal.hs+59−86

@@ -1,4 +1,5 @@

11{-# LANGUAGE TypeFamilyDependencies #-}

2+{-# LANGUAGE ConstraintKinds #-}

23{-# LANGUAGE AllowAmbiguousTypes #-}

34{-# LANGUAGE DataKinds #-}

45{-# LANGUAGE FlexibleContexts #-}

@@ -205,6 +206,14 @@ type family FromNat' (b :: Bool) (m :: Type) :: Type where

205206type family Normalize (d :: Type) :: Type where

206207 Normalize d = FromNat (Count d)

207208

209+-- | Constraint type synonyms to keep the type signatures less convoluted

210+type Countable a = KnownNat (Count a)

211+type CountableN a = KnownNat (Count (Normalize a))

212+type CountableDimensions a b = (Countable a, Countable b)

213+type CountableDimensionsN a b = (CountableN a, CountableN b)

214+type FromListsN e a b = FromLists e (Normalize a) (Normalize b)

215+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

216+

208217-- | It isn't possible to implement the 'id' function so it's

209218-- implementation is 'undefined'. However 'comp' can be and this partial

210219-- class implementation exists just to make the code more readable.

@@ -322,7 +331,7 @@ instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () col

322331 fromLists [h : t] = Junc (One h) (fromLists [t])

323332 fromLists _ = error "Wrong dimensions"

324333

325−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where

334+instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where

326335 fromLists [l] =

327336 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))

328337 in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])

@@ -332,13 +341,13 @@ instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either ()

332341 fromLists ([h] : t) = Split (One h) (fromLists t)

333342 fromLists _ = error "Wrong dimensions"

334343

335−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where

344+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where

336345 fromLists l@([_] : _) =

337346 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))

338347 in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))

339348 fromLists _ = error "Wrong dimensions"

340349

341−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count c)) => FromLists e (Either a b) (Either c d) where

350+instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (Either a b) (Either c d) where

342351 fromLists l@(h : t) =

343352 let lh = length h

344353 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))

@@ -352,8 +361,7 @@ instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a

352361matrixBuilder ::

353362 forall e cols rows.

354363 ( FromLists e cols rows,

355− KnownNat (Count cols),

356− KnownNat (Count rows)

364+ CountableDimensions cols rows

357365 ) =>

358366 ((Int, Int) -> e) ->

359367 Matrix e cols rows

@@ -377,15 +385,8 @@ row = fromLists . (: [])

377385-- types @a@ or @b@ allows.

378386fromF ::

379387 forall a b cols rows e.

380− ( Bounded a,

381− Bounded b,

382− Enum a,

383− Enum b,

384− Eq b,

385− Num e,

386− Ord e,

387− KnownNat (Count cols),

388− KnownNat (Count rows),

388+ ( Liftable e a b,

389+ CountableDimensions cols rows,

389390 FromLists e rows cols

390391 ) =>

391392 (a -> b) ->

@@ -413,16 +414,9 @@ fromF f =

413414-- cardinality's.

414415fromF' ::

415416 forall a b e.

416− ( Bounded a,

417− Bounded b,

418− Enum a,

419− Enum b,

420− Eq b,

421− Num e,

422− Ord e,

423− KnownNat (Count (Normalize a)),

424− KnownNat (Count (Normalize b)),

425− FromLists e (Normalize b) (Normalize a)

417+ ( Liftable e a b,

418+ CountableDimensionsN a b,

419+ FromListsN e b a

426420 ) =>

427421 (a -> b) ->

428422 Matrix e (Normalize a) (Normalize b)

@@ -461,7 +455,7 @@ toList = concat . toLists

461455-- Zeros Matrix

462456

463457-- | The zero matrix. A matrix wholly filled with zeros.

464−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows

458+zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows

465459zeros = matrixBuilder (const 0)

466460

467461-- Ones Matrix

@@ -469,20 +463,20 @@ zeros = matrixBuilder (const 0)

469463-- | The ones matrix. A matrix wholly filled with ones.

470464--

471465-- Also known as T (Top) matrix.

472−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows

466+ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows

473467ones = matrixBuilder (const 1)

474468

475469-- Const Matrix

476470

477471-- | The constant matrix constructor. A matrix wholly filled with a given

478472-- value.

479−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows

473+constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows

480474constant e = matrixBuilder (const e)

481475

482476-- Bang Matrix

483477

484478-- | The T (Top) row vector matrix.

485−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()

479+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), Countable cols) => Matrix e cols ()

486480bang =

487481 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))

488482 in fromLists [take c [1, 1 ..]]

@@ -490,7 +484,7 @@ bang =

490484-- Identity Matrix

491485

492486-- | Identity matrix.

493−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols

487+identity :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols

494488identity = matrixBuilder (bool 0 1 . uncurry (==))

495489

496490-- Matrix composition (MMM)

@@ -509,14 +503,14 @@ comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law

509503-- Projections

510504

511505-- | Biproduct first component projection

512−p1 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e (Either m n) m

506+p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m

513507p1 =

514508 let iden = identity :: Matrix e m m

515509 zero = zeros :: Matrix e n m

516510 in junc iden zero

517511

518512-- | Biproduct second component projection

519−p2 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e (Either m n) n

513+p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n

520514p2 =

521515 let iden = identity :: Matrix e n n

522516 zero = zeros :: Matrix e m n

@@ -525,11 +519,11 @@ p2 =

525519-- Injections

526520

527521-- | Biproduct first component injection

528−i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)

522+i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e m (Either m n)

529523i1 = tr p1

530524

531525-- | Biproduct second component injection

532−i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)

526+i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e n (Either m n)

533527i2 = tr p2

534528

535529-- Dimensions

@@ -541,7 +535,7 @@ i2 = tr p2

541535--

542536-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in

543537-- exchange for performance.

544−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int

538+rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int

545539rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))

546540

547541-- | Obtain the number of columns.

@@ -551,7 +545,7 @@ rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))

551545--

552546-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in

553547-- exchange for performance.

554−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int

548+columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int

555549columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))

556550

557551-- Coproduct Bifunctor

@@ -562,8 +556,7 @@ infixl 5 -|-

562556(-|-) ::

563557 forall e n k m j.

564558 ( Num e,

565− KnownNat (Count j),

566− KnownNat (Count k),

559+ CountableDimensions j k,

567560 FromLists e k k,

568561 FromLists e j k,

569562 FromLists e k j,

@@ -580,10 +573,9 @@ infixl 5 -|-

580573kp1 ::

581574 forall e m k .

582575 ( Num e,

583− KnownNat (Count k),

584− FromLists e (FromNat (Count m * Count k)) m,

585− KnownNat (Count m),

586− KnownNat (Count (Normalize (m, k)))

576+ CountableDimensions k m,

577+ FromLists e (Normalize (m, k)) m,

578+ CountableN (m, k)

587579 ) => Matrix e (Normalize (m, k)) m

588580kp1 = matrixBuilder f

589581 where

@@ -596,10 +588,9 @@ kp1 = matrixBuilder f

596588kp2 ::

597589 forall e m k .

598590 ( Num e,

599− KnownNat (Count k),

600− FromLists e (FromNat (Count m * Count k)) k,

601− KnownNat (Count m),

602− KnownNat (Count (Normalize (m, k)))

591+ CountableDimensions k m,

592+ FromLists e (Normalize (m, k)) k,

593+ CountableN (m, k)

603594 ) => Matrix e (Normalize (m, k)) k

604595kp2 = matrixBuilder f

605596 where

@@ -622,9 +613,8 @@ kp2 = matrixBuilder f

622613khatri ::

623614 forall e cols a b.

624615 ( Num e,

625− KnownNat (Count a),

626− KnownNat (Count b),

627− KnownNat (Count (Normalize (a, b))),

616+ CountableDimensions a b,

617+ CountableN (a, b),

628618 FromLists e (Normalize (a, b)) a,

629619 FromLists e (Normalize (a, b)) b

630620 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))

@@ -641,14 +631,11 @@ infixl 4 ><

641631(><) ::

642632 forall e m p n q.

643633 ( Num e,

644− KnownNat (Count m),

645− KnownNat (Count n),

646− KnownNat (Count p),

647− KnownNat (Count q),

648− KnownNat (Count (Normalize (m, n))),

634+ CountableDimensions m n,

635+ CountableDimensions p q,

636+ CountableDimensionsN (m, n) (p, q),

649637 FromLists e (Normalize (m, n)) m,

650638 FromLists e (Normalize (m, n)) n,

651− KnownNat (Count (Normalize (p, q))),

652639 FromLists e (Normalize (p, q)) p,

653640 FromLists e (Normalize (p, q)) q

654641 )

@@ -701,15 +688,15 @@ tr (Split a b) = Junc (tr a) (tr b)

701688

702689-- | Selective functors 'select' operator equivalent inspired by the

703690-- ArrowMonad solution presented in the paper.

704−select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

691+select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

705692select m y = junc y identity . m

706693

707694-- McCarthy's Conditional

708695

709696-- | McCarthy's Conditional expresses probabilistic choice.

710697cond ::

711− ( cols ~ FromNat (Count cols),

712− KnownNat (Count cols),

698+ ( cols ~ Normalize cols,

699+ Countable cols,

713700 FromLists e () cols,

714701 FromLists e cols (),

715702 FromLists e cols cols,

@@ -723,8 +710,8 @@ cond ::

723710cond p f g = junc f g . grd p

724711

725712grd ::

726− ( q ~ FromNat (Count q),

727− KnownNat (Count q),

713+ ( q ~ Normalize q,

714+ Countable q,

728715 FromLists e () q,

729716 FromLists e q (),

730717 FromLists e q q,

@@ -739,15 +726,12 @@ grd f = split (corr f) (corr (not . f))

739726

740727corr ::

741728 forall e a q .

742− ( q ~ FromNat (Count q),

743− KnownNat (Count q),

729+ ( q ~ Normalize q,

730+ Countable q,

744731 FromLists e () q,

745732 FromLists e q (),

746733 FromLists e q q,

747− Bounded a,

748− Enum a,

749− Num e,

750− Ord e

734+ Liftable e a Bool

751735 )

752736 => (a -> Bool) -> Matrix e q q

753737corr p = let f = fromF p :: Matrix e q ()

@@ -775,7 +759,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++

775759 fill str = replicate (widest - length str - 2) ' ' ++ str

776760

777761-- | Matrix pretty printer

778−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String

762+pretty :: (Countable cols, Show e) => Matrix e cols rows -> String

779763pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++

780764 prettyAux (toLists m) (toLists m) ++

781765 "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"

@@ -786,7 +770,7 @@ pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++

786770 blank = fill ""

787771

788772-- | Matrix pretty printer

789−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()

773+prettyPrint :: (Countable cols, Show e) => Matrix e cols rows -> IO ()

790774prettyPrint = putStrLn . pretty

791775

792776-- Relational operators functions

@@ -872,14 +856,9 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)

872856-- types @a@ or @b@ allows.

873857fromFRel ::

874858 forall a b cols rows.

875− ( Bounded a,

876− Bounded b,

877− Enum a,

878− Enum b,

879− Eq b,

880− KnownNat (Count cols),

881− KnownNat (Count rows),

882− FromLists (Natural 0 1) rows cols

859+ ( Liftable Boolean a b,

860+ CountableDimensions cols rows,

861+ FromLists Boolean rows cols

883862 ) =>

884863 (a -> b) ->

885864 Relation cols rows

@@ -906,14 +885,9 @@ fromFRel f =

906885-- cardinality's.

907886fromFRel' ::

908887 forall a b.

909− ( Bounded a,

910− Bounded b,

911− Enum a,

912− Enum b,

913− Eq b,

914− KnownNat (Count (Normalize a)),

915− KnownNat (Count (Normalize b)),

916− FromLists (Natural 0 1) (Normalize b) (Normalize a)

888+ ( Liftable Boolean a b,

889+ CountableDimensionsN a b,

890+ FromLists Boolean (Normalize b) (Normalize a)

917891 ) =>

918892 (a -> b) ->

919893 Relation (Normalize a) (Normalize b)

@@ -944,9 +918,8 @@ toRel ::

944918 Enum a,

945919 Enum b,

946920 Eq b,

947− KnownNat (Count (Normalize a)),

948− KnownNat (Count (Normalize b)),

949− FromLists (Natural 0 1) (Normalize b) (Normalize a)

921+ CountableDimensionsN a b,

922+ FromListsN Boolean b a

950923 )

951924 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)

952925toRel f =

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+123−146

@@ -1,3 +1,4 @@

1+{-# LANGUAGE ConstraintKinds #-}

12{-# LANGUAGE AllowAmbiguousTypes #-}

23{-# LANGUAGE DataKinds #-}

34{-# LANGUAGE DerivingVia #-}

@@ -55,6 +56,17 @@ module LAoP.Matrix.Type

5556 -- * Type safe matrix representation

5657 Matrix (..),

5758

59+ -- * Constraint type aliases

60+ Countable,

61+ CountableDimensions,

62+ CountableN,

63+ CountableDimensionsN,

64+ FromListsN,

65+ Liftable,

66+ Trivial,

67+ TrivialE,

68+ TrivialP,

69+

5870 -- * Type aliases

5971 Zero,

6072 One,

@@ -170,6 +182,17 @@ import qualified LAoP.Matrix.Internal as I

170182newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))

171183 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))

172184

185+-- | Constraint type synonyms to keep the type signatures less convoluted

186+type Countable a = KnownNat (I.Count a)

187+type CountableDimensions a b = (Countable a, Countable b)

188+type CountableN a = KnownNat (I.Count (I.Normalize a))

189+type CountableDimensionsN a b = (CountableN a, CountableN b)

190+type FromListsN e a b = I.FromLists e (I.Normalize a) (I.Normalize b)

191+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

192+type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)

193+type TrivialE a b = I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)

194+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

195+

173196-- | It isn't possible to implement the 'id' function so it's

174197-- implementation is 'undefined'. However 'comp' can be and this partial

175198-- class implementation exists just to make the code more readable.

@@ -197,7 +220,7 @@ one = M . I.One

197220

198221-- | Matrix 'Junc' constructor

199222junc ::

200− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

223+ (TrivialE a b) =>

201224 Matrix e a rows ->

202225 Matrix e b rows ->

203226 Matrix e (Either a b) rows

@@ -206,7 +229,7 @@ junc (M a) (M b) = M (I.Junc a b)

206229infixl 3 |||

207230-- | Matrix 'Junc' constructor

208231(|||) ::

209− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

232+ (TrivialE a b) =>

210233 Matrix e a rows ->

211234 Matrix e b rows ->

212235 Matrix e (Either a b) rows

@@ -214,7 +237,7 @@ infixl 3 |||

214237

215238-- | Matrix 'Split' constructor

216239split ::

217− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

240+ (TrivialE a b) =>

218241 Matrix e cols a ->

219242 Matrix e cols b ->

220243 Matrix e cols (Either a b)

@@ -223,7 +246,7 @@ split (M a) (M b) = M (I.Split a b)

223246infixl 2 ===

224247-- | Matrix 'Split' constructor

225248(===) ::

226− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

249+ (TrivialE a b) =>

227250 Matrix e cols a ->

228251 Matrix e cols b ->

229252 Matrix e cols (Either a b)

@@ -233,16 +256,9 @@ infixl 2 ===

233256

234257-- | Functor instance equivalent function

235258fmapM ::

236− ( Bounded a,

237− Bounded b,

238− Enum a,

239− Enum b,

240− Eq b,

241− Num e,

242− Ord e,

243− KnownNat (I.Count (I.Normalize a)),

244− KnownNat (I.Count (I.Normalize b)),

245− I.FromLists e (I.Normalize b) (I.Normalize a)

259+ ( Liftable e a b,

260+ CountableDimensionsN a b,

261+ FromListsN e b a

246262 )

247263 =>

248264 (a -> b) -> Matrix e c a -> Matrix e c b

@@ -254,25 +270,23 @@ unitM = one 1

254270

255271-- | Applicative instance equivalent 'unit' function,

256272multM ::

257− ( KnownNat (I.Count (I.Normalize a)),

258− KnownNat (I.Count (I.Normalize b)),

259− KnownNat (I.Count (I.Normalize (a, b))),

273+ ( CountableDimensionsN a b,

274+ CountableN (a, b),

260275 Num e,

261− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),

262− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),

263− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

276+ FromListsN e (a, b) a,

277+ FromListsN e (a, b) b,

278+ TrivialP a b

264279 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)

265−multM a b = khatri a b

266−

280+multM = khatri

267281

268282-- | Monad instance equivalent 'return' function,

269283returnM ::

270284 forall e a .

271− ( Num e,

272− Enum e,

273− Enum a,

274− I.FromLists e () (I.Normalize a),

275− KnownNat (I.Count a)

285+ ( Num e,

286+ Enum e,

287+ Enum a,

288+ FromListsN e () a,

289+ Countable a

276290 ) => a -> Matrix e One a

277291returnM a = col l

278292 where

@@ -288,23 +302,22 @@ bindM = flip comp

288302

289303-- | Build a matrix out of a list of list of elements. Throws a runtime

290304-- error if the dimensions do not match.

291−fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows

305+fromLists :: (FromListsN e cols rows) => [[e]] -> Matrix e cols rows

292306fromLists = M . I.fromLists

293307

294308-- | Matrix builder function. Constructs a matrix provided with

295309-- a construction function.

296310matrixBuilder ::

297− (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

298− ((Int, Int) -> e) ->

299− Matrix e cols rows

311+ (FromListsN e cols rows, CountableDimensionsN cols rows )

312+ => ((Int, Int) -> e) -> Matrix e cols rows

300313matrixBuilder = M . I.matrixBuilder

301314

302315-- | Constructs a column vector matrix

303−col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows

316+col :: (FromListsN e () rows) => [e] -> Matrix e One rows

304317col = M . I.col

305318

306319-- | Constructs a row vector matrix

307−row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One

320+row :: (FromListsN e cols ()) => [e] -> Matrix e cols One

308321row = M . I.row

309322

310323-- | Lifts functions to matrices with arbitrary dimensions.

@@ -312,49 +325,28 @@ row = M . I.row

312325-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of

313326-- types @a@ or @b@ allows.

314327fromF ::

315− ( Bounded a,

316− Bounded b,

317− Enum a,

318− Enum b,

319− Eq b,

320− Num e,

321− Ord e,

322− KnownNat (I.Count (I.Normalize cols)),

323− KnownNat (I.Count (I.Normalize rows)),

324− I.FromLists e (I.Normalize rows) (I.Normalize cols)

328+ ( Liftable e a b,

329+ CountableDimensionsN cols rows,

330+ FromListsN e rows cols

325331 ) =>

326− (a -> b) ->

327− Matrix e cols rows

332+ (a -> b) -> Matrix e cols rows

328333fromF = M . I.fromF

329334

330335-- | Lifts functions to matrices with dimensions matching @a@ and @b@

331336-- cardinality's.

332337fromF' ::

333− ( Bounded a,

334− Bounded b,

335− Enum a,

336− Enum b,

337− Eq b,

338− Num e,

339− Ord e,

340− KnownNat (I.Count (I.Normalize a)),

341− KnownNat (I.Count (I.Normalize b)),

342− I.FromLists e (I.Normalize b) (I.Normalize a)

338+ ( Liftable e a b,

339+ CountableDimensionsN a b,

340+ FromListsN e b a

343341 ) =>

344− (a -> b) ->

345− Matrix e a b

342+ (a -> b) -> Matrix e a b

346343fromF' = M . I.fromF'

347344

348345-- | Lifts relation functions to Boolean Matrix

349346toRel ::

350− ( Bounded a,

351− Bounded b,

352− Enum a,

353− Enum b,

354− Eq b,

355− KnownNat (I.Count (I.Normalize a)),

356− KnownNat (I.Count (I.Normalize b)),

357− I.FromLists (Natural 0 1) (I.Normalize b) (I.Normalize a)

347+ ( Liftable (Natural 0 1) a b,

348+ CountableDimensionsN a b,

349+ FromListsN (Natural 0 1) b a

358350 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b

359351toRel = M . I.toRel

360352

@@ -372,8 +364,8 @@ toList (M m) = I.toList m

372364

373365-- | The zero matrix. A matrix wholly filled with zeros.

374366zeros ::

375− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

376− Matrix e cols rows

367+ (Num e, FromListsN e cols rows, CountableDimensionsN cols rows)

368+ => Matrix e cols rows

377369zeros = M I.zeros

378370

379371-- Ones Matrix

@@ -382,8 +374,8 @@ zeros = M I.zeros

382374--

383375-- Also known as T (Top) matrix.

384376ones ::

385− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

386− Matrix e cols rows

377+ (Num e, FromListsN e cols rows, CountableDimensionsN cols rows)

378+ => Matrix e cols rows

387379ones = M I.ones

388380

389381-- Const Matrix

@@ -391,9 +383,8 @@ ones = M I.ones

391383-- | The constant matrix constructor. A matrix wholly filled with a given

392384-- value.

393385constant ::

394− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

395− e ->

396− Matrix e cols rows

386+ (Num e, FromListsN e cols rows, CountableDimensionsN cols rows)

387+ => e -> Matrix e cols rows

397388constant = M . I.constant

398389

399390-- Bang Matrix

@@ -401,7 +392,7 @@ constant = M . I.constant

401392-- | The T (Top) row vector matrix.

402393bang ::

403394 forall e cols.

404− (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>

395+ (Num e, Enum e, FromListsN e cols (), CountableN cols) =>

405396 Matrix e cols One

406397bang = M I.bang

407398

@@ -409,7 +400,7 @@ bang = M I.bang

409400

410401-- | Identity matrix

411402identity ::

412− (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>

403+ (Num e, FromListsN e a a, CountableN a) =>

413404 Matrix e a a

414405identity = M I.identity

415406

@@ -425,11 +416,10 @@ comp (M a) (M b) = M (I.comp a b)

425416-- | Biproduct first component projection

426417p1 ::

427418 ( Num e,

428− KnownNat (I.Count (I.Normalize n)),

429− KnownNat (I.Count (I.Normalize m)),

430− I.FromLists e (I.Normalize n) (I.Normalize m),

431− I.FromLists e (I.Normalize m) (I.Normalize m),

432− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

419+ CountableDimensionsN n m,

420+ FromListsN e n m,

421+ FromListsN e m m,

422+ TrivialE m n

433423 ) =>

434424 Matrix e (Either m n) m

435425p1 = M I.p1

@@ -437,11 +427,10 @@ p1 = M I.p1

437427-- | Biproduct second component projection

438428p2 ::

439429 ( Num e,

440− KnownNat (I.Count (I.Normalize n)),

441− KnownNat (I.Count (I.Normalize m)),

442− I.FromLists e (I.Normalize m) (I.Normalize n),

443− I.FromLists e (I.Normalize n) (I.Normalize n),

444− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

430+ CountableDimensionsN n m,

431+ FromListsN e m n,

432+ FromListsN e n n,

433+ TrivialE m n

445434 ) =>

446435 Matrix e (Either m n) n

447436p2 = M I.p2

@@ -451,11 +440,10 @@ p2 = M I.p2

451440-- | Biproduct first component injection

452441i1 ::

453442 ( Num e,

454− KnownNat (I.Count (I.Normalize n)),

455− KnownNat (I.Count (I.Normalize m)),

456− I.FromLists e (I.Normalize n) (I.Normalize m),

457− I.FromLists e (I.Normalize m) (I.Normalize m),

458− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

443+ CountableDimensionsN n m,

444+ FromListsN e n m,

445+ FromListsN e m m,

446+ TrivialE m n

459447 ) =>

460448 Matrix e m (Either m n)

461449i1 = tr p1

@@ -463,11 +451,10 @@ i1 = tr p1

463451-- | Biproduct second component injection

464452i2 ::

465453 ( Num e,

466− KnownNat (I.Count (I.Normalize n)),

467− KnownNat (I.Count (I.Normalize m)),

468− I.FromLists e (I.Normalize m) (I.Normalize n),

469− I.FromLists e (I.Normalize n) (I.Normalize n),

470− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

454+ CountableDimensionsN n m,

455+ FromListsN e m n,

456+ FromListsN e n n,

457+ TrivialE m n

471458 ) =>

472459 Matrix e n (Either m n)

473460i2 = tr p2

@@ -481,7 +468,7 @@ i2 = tr p2

481468--

482469-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in

483470-- exchange for performance.

484−rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int

471+rows :: (CountableN rows) => Matrix e cols rows -> Int

485472rows (M m) = I.rows m

486473

487474-- | Obtain the number of columns.

@@ -491,7 +478,7 @@ rows (M m) = I.rows m

491478--

492479-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in

493480-- exchange for performance.

494−columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int

481+columns :: (CountableN cols) => Matrix e cols rows -> Int

495482columns (M m) = I.columns m

496483

497484-- Coproduct Bifunctor

@@ -501,14 +488,13 @@ infixl 5 -|-

501488-- | Matrix coproduct functor also known as matrix direct sum.

502489(-|-) ::

503490 ( Num e,

504− KnownNat (I.Count (I.Normalize j)),

505− KnownNat (I.Count (I.Normalize k)),

506− I.FromLists e (I.Normalize k) (I.Normalize k),

507− I.FromLists e (I.Normalize j) (I.Normalize k),

508− I.FromLists e (I.Normalize k) (I.Normalize j),

509− I.FromLists e (I.Normalize j) (I.Normalize j),

510− I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),

511− I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)

491+ CountableDimensionsN j k,

492+ FromListsN e k k,

493+ FromListsN e j k,

494+ FromListsN e k j,

495+ FromListsN e j j,

496+ TrivialE n m,

497+ TrivialE k j

512498 ) =>

513499 Matrix e n k ->

514500 Matrix e m j ->

@@ -521,11 +507,10 @@ infixl 5 -|-

521507kp1 ::

522508 forall e m k .

523509 ( Num e,

524− KnownNat (I.Count (I.Normalize m)),

525− KnownNat (I.Count (I.Normalize k)),

526− KnownNat (I.Count (I.Normalize (m, k))),

527− I.FromLists e (I.Normalize (m, k)) (I.Normalize m),

528− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)

510+ CountableDimensionsN m k,

511+ CountableN (m, k),

512+ FromListsN e (m, k) m,

513+ TrivialP m k

529514 ) => Matrix e (m, k) m

530515kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))

531516

@@ -533,11 +518,10 @@ kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))

533518kp2 ::

534519 forall e m k.

535520 ( Num e,

536− KnownNat (I.Count (I.Normalize k)),

537− KnownNat (I.Count (I.Normalize m)),

538− KnownNat (I.Count (I.Normalize (m, k))),

539− I.FromLists e (I.Normalize (m, k)) (I.Normalize k),

540− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)

521+ CountableDimensionsN k m,

522+ CountableN (m, k),

523+ FromListsN e (m, k) k,

524+ TrivialP m k

541525 ) => Matrix e (m, k) k

542526kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))

543527

@@ -555,12 +539,11 @@ kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))

555539khatri ::

556540 forall e cols a b.

557541 ( Num e,

558− KnownNat (I.Count (I.Normalize a)),

559− KnownNat (I.Count (I.Normalize b)),

560− KnownNat (I.Count (I.Normalize (a, b))),

561− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),

562− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),

563− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

542+ CountableDimensionsN a b,

543+ CountableN (a, b),

544+ FromListsN e (a, b) a,

545+ FromListsN e (a, b) b,

546+ TrivialP a b

564547 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)

565548khatri a b =

566549 let kp1' = kp1 @e @a @b

@@ -575,18 +558,15 @@ infixl 4 ><

575558(><) ::

576559 forall e m p n q.

577560 ( Num e,

578− KnownNat (I.Count (I.Normalize m)),

579− KnownNat (I.Count (I.Normalize n)),

580− KnownNat (I.Count (I.Normalize p)),

581− KnownNat (I.Count (I.Normalize q)),

582− KnownNat (I.Count (I.Normalize (m, n))),

583− KnownNat (I.Count (I.Normalize (p, q))),

584− I.FromLists e (I.Normalize (m, n)) (I.Normalize m),

585− I.FromLists e (I.Normalize (m, n)) (I.Normalize n),

586− I.FromLists e (I.Normalize (p, q)) (I.Normalize p),

587− I.FromLists e (I.Normalize (p, q)) (I.Normalize q),

588− I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),

589− I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)

561+ CountableDimensionsN m n,

562+ CountableDimensionsN p q,

563+ CountableDimensionsN (m, n) (p, q),

564+ FromListsN e (m, n) m,

565+ FromListsN e (m, n) n,

566+ FromListsN e (p, q) p,

567+ FromListsN e (p, q) q,

568+ TrivialP m n,

569+ TrivialP p q

590570 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)

591571(><) a b =

592572 let kp1' = kp1 @e @m @n

@@ -629,9 +609,9 @@ tr (M m) = M (I.tr m)

629609-- ArrowMonad solution presented in the paper.

630610selectM ::

631611 ( Num e,

632− I.FromLists e (I.Normalize b) (I.Normalize b),

633− KnownNat (I.Count (I.Normalize b)),

634− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)

612+ FromListsN e b b,

613+ CountableN b,

614+ TrivialE a b

635615 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

636616selectM (M m) (M y) = M (I.select m y)

637617

@@ -639,15 +619,12 @@ selectM (M m) (M y) = M (I.select m y)

639619

640620-- | McCarthy's Conditional expresses probabilistic choice.

641621cond ::

642− ( I.Normalize (I.Normalize a) ~ I.Normalize a,

643− KnownNat (I.Count (I.Normalize a)),

644− I.FromLists e () (I.Normalize a),

645− I.FromLists e (I.Normalize a) (),

646− I.FromLists e (I.Normalize a) (I.Normalize a),

647− Bounded a,

648− Enum a,

649− Num e,

650− Ord e

622+ ( Trivial a,

623+ CountableN a,

624+ FromListsN e () a,

625+ FromListsN e a (),

626+ FromListsN e a a,

627+ Liftable e a Bool

651628 )

652629 =>

653630 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b

@@ -656,9 +633,9 @@ cond p (M a) (M b) = M (I.cond p a b)

656633-- Pretty print

657634

658635-- | Matrix pretty printer

659−pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String

636+pretty :: (CountableN cols, Show e) => Matrix e cols rows -> String

660637pretty (M m) = I.pretty m

661638

662639-- | Matrix pretty printer

663−prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()

640+prettyPrint :: (CountableN cols, Show e) => Matrix e cols rows -> IO ()

664641prettyPrint (M m) = I.prettyPrint m

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