1da55a0 · laop · git.iko.soy

git.iko.soy/laop

Added constrained Category class!

commit1da55a0fe8d6f13602db7fc6c505f058d452f956 authorArmando Santos <armandoifsantos@gmail.com> dateWed 26 Feb 2020, 11:38 (7 years ago) parent1a819dd

10 files changed+137−117

compare with master

unifiedsplit

app/Examples.hs+6−7 app/Quantum.hs+4−2 app/Spreadsheets.hs+4−2 src/LAoP/Dist/Internal.hs+1 src/LAoP/Matrix/Internal.hs+13−14 src/LAoP/Matrix/Nat.hs−10 src/LAoP/Matrix/Type.hs+12−13 src/LAoP/Relation/Internal.hs+65−66 src/LAoP/Utils.hs+4−1 src/LAoP/Utils/Internal.hs+28−2

app/Examples.hs+6−7

@@ -17,8 +17,7 @@ import LAoP.Dist

1717import GHC.TypeLits

1818import Data.Coerce

1919import qualified GHC.Generics as G

20−import Control.Category hiding (id)

21−import Prelude hiding ((.))

20+import Prelude hiding (id, (.))

2221

2322-- Monty Hall Problem

2423data Outcome = Win | Lose

@@ -76,8 +75,8 @@ sprinkler :: Matrix Double R S

7675sprinkler = matrixBuilder gen

7776 where

7877 gen (No, Off) = 0.6

79− gen (No, On) = 0.99

80− gen (Yes, Off) = 0.4

78+ gen (No, On) = 0.4

79+ gen (Yes, Off) = 0.99

8180 gen (Yes, On) = 0.01

8281

8382grass :: Matrix Double (S, R) G

@@ -92,9 +91,9 @@ grass = matrixBuilder gen

9291 gen ((On, No), Wet) = 0.9

9392 gen ((On, Yes), Wet) = 0.99

9493

95−tag f = kr f iden

94+tag f = kr f id

9695

97−state g s r = tag g `comp` tag s `comp` r

96+state g s r = tag g . tag s . r

9897

9998grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One

10099grass_wet state = row [0,1] . fstM . state

@@ -173,7 +172,7 @@ exec = do

173172 putStrLn "Monty Hall Problem solution:"

174173 prettyPrint (secondChoice . firstChoice)

175174 putStrLn "\n Sum of dices probability:"

176− prettyPrint (sumSSM `comp` kr die die)

175+ prettyPrint (sumSSM . kr die die)

177176 putStrLn "\n Conditional dice throw:"

178177 prettyPrint conditionalThrows

179178 putStrLn "\n Checking that the last result is indeed a distribution: "

app/Quantum.hs+4−2

@@ -1,8 +1,10 @@

11{-# LANGUAGE StandaloneDeriving #-}

22module Quantum where

4+import LAoP.Utils

45import LAoP.Matrix.Type

56import Data.Complex

7+import Prelude hiding (id, (.))

79deriving instance Ord a => Ord (Complex a)

810

@@ -11,7 +13,7 @@ xor (False, b) = b

1113xor (True, b) = not b

1214

1315ker :: Num e => Matrix e a b -> Matrix e a a

14−ker m = tr m `comp` m

16+ker m = tr m . m

1517

1618cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)

1719cnot = kr fstM (fromF xor)

@@ -26,4 +28,4 @@ had :: Matrix (Complex Double) Bool Bool

2628had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]

2729

2830bell :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)

29−bell = cnot `comp` (had >< iden)

31+bell = cnot . (had >< iden)

app/Spreadsheets.hs+4−2

@@ -3,8 +3,10 @@

33module Spreadsheets

44 where

6+import LAoP.Utils

67import LAoP.Matrix.Type

78import GHC.Generics

9+import Prelude hiding (id, (.))

810

911data Student = Student1 | Student2 | Student3 | Student4

1012 deriving (Eq, Show, Enum, Bounded, Generic)

@@ -36,10 +38,10 @@ xls :: Matrix Float Question One

3638 -> Matrix Float (Either Question Results) (Either One Student)

3739xls w m t = join (fork w m) (fork zeros r)

3840 where

39− rExam = m `comp` tr w

41+ rExam = m . tr w

4042 rTest = tr t

4143 rFinal = rTest `maxPW` rExam

42− r = (rExam `comp` tr exam) + (rTest `comp` tr test) + (rFinal `comp` tr final)

44+ r = (rExam . tr exam) + (rTest . tr test) + (rFinal . tr final)

4345

4446-- | Overloaded, point-wise 'max' function

4547maxPW :: Ord e => Matrix e a b -> Matrix e a b -> Matrix e a b

src/LAoP/Dist/Internal.hs+1

@@ -44,6 +44,7 @@ module LAoP.Dist.Internal

4444 where

4545

4646import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDimensions, CountableN, CountableDimensionsN, Liftable, FromListsN)

47+import Prelude hiding (id, (.))

4748import qualified LAoP.Matrix.Internal as I

4849import LAoP.Utils

4950import GHC.TypeLits

src/LAoP/Matrix/Internal.hs+13−14

@@ -119,6 +119,7 @@ module LAoP.Matrix.Internal

119119

120120 -- | Note that given the restrictions imposed it is not possible to

121121 -- implement the standard type classes present in standard Haskell.

122+

122123 -- *** Matrix pairing projections

123124 fstM,

124125 sndM,

@@ -169,8 +170,8 @@ import GHC.TypeLits

169170import Data.Type.Equality

170171import GHC.Generics

171172import Control.DeepSeq

172−import Control.Category

173−import Prelude hiding ((.))

173+import Prelude hiding (id, (.))

174+import qualified Prelude (id, (.))

174175

175176-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.

176177data Matrix e cols rows where

@@ -227,14 +228,12 @@ type FromListsN e a b = FromLists e (Normalize a) (Normalize b)

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

228229type Trivial a = FromNat (Count a) ~ a

229230

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

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

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

233−--

234−-- Please use 'iden' instead.

231+-- | It is possible to implement a constrained version of the category type

232+-- class.

235233instance (Num e) => Category (Matrix e) where

236− id = undefined

237− (.) = comp

234+ type Object (Matrix e) a = (FromLists e a a, Countable a)

235+ id = iden

236+ (.) = comp

238237

239238instance NFData e => NFData (Matrix e cols rows) where

240239 rnf Empty = ()

@@ -501,7 +500,7 @@ bang =

501500-- iden Matrix

502501

503502-- | iden matrix.

504−iden :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols

503+iden :: forall e cols . (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols

505504iden = matrixBuilder' (bool 0 1 . uncurry (==))

506505{-# NOINLINE iden #-}

507506

@@ -547,11 +546,11 @@ infixl 7 ./

547546

548547-- | Biproduct first component projection

549548p1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m

550−p1 = join iden zeros

549+p1 = join id zeros

551550

552551-- | Biproduct second component projection

553552p2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n

554−p2 = join zeros iden

553+p2 = join zeros id

555554

556555-- Injections

557556

@@ -728,7 +727,7 @@ tr (Fork a b) = Join (tr a) (tr b)

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

729728select (Fork a b) y = y . a + b -- Divide-and-conquer law

730729select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law

731−select m y = join y iden . m

730+select m y = join y id . m

732731

733732branch ::

734733 ( Num e,

@@ -797,7 +796,7 @@ corr ::

797796 )

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

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

800− in kr f (iden :: Matrix e q q)

799+ in kr f (id :: Matrix e q q)

801800

802801-- Pretty print

803802

src/LAoP/Matrix/Nat.hs−10

@@ -161,7 +161,6 @@ where

161161import Data.Proxy

162162import GHC.TypeLits

163163import Control.DeepSeq

164−import qualified Control.Category as C

165164import qualified LAoP.Matrix.Internal as I

166165

167166newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))

@@ -179,15 +178,6 @@ type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num

179178type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)

180179type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))

181180

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

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

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

185−--

186−-- Please use 'iden' instead.

187−instance (Num e) => C.Category (Matrix e) where

188− id = undefined

189− (.) = comp

190−

191181-- Primitives

192182

193183empty :: Matrix e 0 0

src/LAoP/Matrix/Type.hs+12−13

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

11{-# LANGUAGE ConstraintKinds #-}

2+{-# LANGUAGE TypeFamilies #-}

23{-# LANGUAGE AllowAmbiguousTypes #-}

34{-# LANGUAGE DataKinds #-}

45{-# LANGUAGE DerivingVia #-}

@@ -185,8 +186,8 @@ import Data.Kind

185186import GHC.TypeLits

186187import Control.DeepSeq

187188import LAoP.Utils

188−import qualified Control.Category as C

189189import qualified LAoP.Matrix.Internal as I

190+import Prelude hiding (id, (.))

190191

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

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

@@ -203,14 +204,12 @@ type Trivial2 a = I.Normalize a ~ I.Normalize (I.Normalize a)

203204type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)

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

205206

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

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

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

209−--

210−-- Please use 'iden' instead.

211−instance (Num e) => C.Category (Matrix e) where

212− id = undefined

213− (.) = comp

207+-- | It is possible to implement a constrained version of the category type

208+-- class.

209+instance (Num e) => Category (Matrix e) where

210+ type Object (Matrix e) a = (FromListsN e a a, CountableN a)

211+ id = iden

212+ (.) = comp

214213

215214-- | Bifunctor equivalent function

216215bimapM ::

@@ -221,7 +220,7 @@ bimapM ::

221220 FromListsN e d c,

222221 FromListsN e b a

223222 ) => (a -> b) -> (c -> d) -> Matrix e a c -> Matrix e b d

224−bimapM f g m = fromF g `comp` m `comp` tr (fromF f)

223+bimapM f g m = fromF g . m . tr (fromF f)

225224

226225-- | Zero type alias

227226type Zero = Void

@@ -279,7 +278,7 @@ fmapM ::

279278 )

280279 =>

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

282−fmapM f m = fromF f `comp` m

281+fmapM f m = fromF f . m

283282

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

285284unitM :: (Num e) => Matrix e () ()

@@ -586,9 +585,9 @@ sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))

586585-- NOTE: That this is not a true categorical product, see for instance:

587586--

588587-- @

589−-- | fstM `comp` kr a b == a

588+-- | fstM . kr a b == a

590589-- kr a b ==> |

591−-- | sndM `comp` kr a b == b

590+-- | sndM . kr a b == b

592591-- @

593592--

594593-- __Emphasis__ on the implication symbol.

src/LAoP/Relation/Internal.hs+65−66

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

1+{-# LANGUAGE TypeFamilies #-}

12{-# LANGUAGE ConstraintKinds #-}

23{-# LANGUAGE GADTs #-}

34{-# LANGUAGE UndecidableInstances #-}

@@ -178,9 +179,9 @@ import Data.Void

178179import qualified LAoP.Matrix.Internal as I

179180import LAoP.Utils.Internal

180181import Control.DeepSeq

181−import qualified Control.Category as C

182182import Data.Bool

183183import GHC.TypeLits

184+import Prelude hiding (id, (.))

184185

185186-- | Boolean type synonym for working with boolean matrices

186187type Boolean = Natural 0 1

@@ -202,14 +203,12 @@ type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num

202203type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)

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

204205

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

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

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

208−--

209−-- Please use 'iden' instead.

210−instance C.Category Relation where

211− id = undefined

212− (.) = comp

206+-- | It is possible to implement a constrained version of the category type

207+-- class.

208+instance Category Relation where

209+ type Object Relation a = (FromListsN a a, CountableN a)

210+ id = iden

211+ (.) = comp

213212

214213instance Num (Relation a b) where

215214 -- | Matrix addition becomes Boolean matrix disjointion

@@ -387,7 +386,7 @@ belongs = toRel elemR

387386-- Also known as ⊥ (Bottom) Relation or empty Relation.

388387--

389388-- @

390−-- r ``comp`` ⊥ == ⊥ ``comp`` r == ⊥

389+-- r `.` ⊥ == ⊥ `.` r == ⊥

391390-- ⊥ ``sse`` R && R ``sse`` T == True

392391-- @

393392zeros ::

@@ -433,7 +432,7 @@ point = fromF . const

433432-- | iden matrix

434433--

435434-- @

436−-- 'iden' ``comp`` r == r == r ``comp`` 'iden'

435+-- 'iden' `.` r == r == r `.` 'iden'

437436-- @

438437iden ::

439438 (FromListsN a a, CountableN a) => Relation a a

@@ -442,7 +441,7 @@ iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))

442441-- | Relational composition

443442--

444443-- @

445−-- r ``comp`` (s ``comp`` p) = (r ``comp`` s) ``comp`` p

444+-- r `.` (s `.` p) = (r `.` s) `.` p

446445-- @

447446comp :: Relation b c -> Relation a b -> Relation a c

448447comp (R a) (R b) = R (I.compRel a b)

@@ -506,7 +505,7 @@ pointAp ::

506505 FromListsN a One,

507506 FromListsN b One

508507 ) => a -> b -> Relation a b -> Relation One One

509−pointAp a b r = conv (point b) `comp` r `comp` point a

508+pointAp a b r = conv (point b) . r . point a

510509

511510-- | Relational application

512511--

@@ -518,7 +517,7 @@ pointApBool ::

518517 FromListsN a One,

519518 FromListsN b One

520519 ) => a -> b -> Relation a b -> Bool

521−pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a

520+pointApBool a b r = toBool $ conv (point b) . r . point a

522521

523522-- | Relational converse

524523--

@@ -560,8 +559,8 @@ intersection a b = a * b

560559-- @

561560-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)

562561-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x

563−-- r ``comp`` (s ``union`` t) == (r ``comp`` s) ``union`` (r ``comp`` t)

564−-- (s ``union`` t) ``comp`` r == (s ``comp`` r) ``union`` (t ``comp`` r)

562+-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)

563+-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)

565564-- @

566565union :: Relation a b -> Relation a b -> Relation a b

567566union a b = a + b

@@ -569,29 +568,29 @@ union a b = a + b

569568-- | Relation Kernel

570569--

571570-- @

572−-- 'ker' r == 'conv' r ``comp`` r

571+-- 'ker' r == 'conv' r `.` r

573572-- 'ker' r == 'img' ('conv' r)

574573-- @

575574ker :: Relation a b -> Relation a a

576−ker r = conv r `comp` r

575+ker r = conv r . r

577576

578577-- | Relation Image

579578--

580579-- @

581−-- 'img' r == r ``comp`` conv r

580+-- 'img' r == r `.` conv r

582581-- 'img' r == 'ker' ('conv' r)

583582-- @

584583img :: Relation a b -> Relation b b

585−img r = r `comp` conv r

584+img r = r . conv r

586585

587586-- | Function division. Special case of 'divS'.

588587--

589588-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and

590589-- 'entire'.

591590--

592−-- @'divisionF' f g == 'conv' g ``comp`` f@

591+-- @'divisionF' f g == 'conv' g `.` f@

593592divisionF :: Relation a c -> Relation b c -> Relation a b

594−divisionF f g = conv g `comp` f

593+divisionF f g = conv g . f

595594

596595-- Taxonomy of binary relations

597596

@@ -617,8 +616,8 @@ surjective = reflexive . img

617616-- relations:

618617--

619618-- @

620−-- f ``comp`` r ``sse`` s == r ``sse`` f ``comp`` s

621−-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f

619+-- f `.` r ``sse`` s == r ``sse`` f `.` s

620+-- r `.` f ``sse`` s == r ``sse`` s `.` f

622621-- @

623622function ::

624623 ( CountableDimensionsN a b,

@@ -672,29 +671,29 @@ bijection r = injection r && surjection r

672671

673672-- Properties of relations

674673

675−-- | A 'Relation' @r@ is 'reflexive' 'iff' @'iden' ``sse`` r@

674+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@

676675reflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool

677−reflexive r = iden <= r

676+reflexive r = id <= r

678677

679−-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'iden'@

678+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@

680679coreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool

681−coreflexive r = r <= iden

680+coreflexive r = r <= id

682681

683−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@

682+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@

684683transitive :: Relation a a -> Bool

685−transitive r = (r `comp` r) `sse` r

684+transitive r = (r . r) `sse` r

686685

687686-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@

688687symmetric :: Relation a a -> Bool

689688symmetric r = r == conv r

690689

691−-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'iden'@

690+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@

692691antiSymmetric :: (CountableN a, FromListsN a a) => Relation a a -> Bool

693−antiSymmetric r = (r `intersection` conv r) `sse` iden

692+antiSymmetric r = (r `intersection` conv r) `sse` id

694693

695−-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'iden') == 'zeros'@

694+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@

696695irreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool

697−irreflexive r = (r `intersection` iden) == zeros

696+irreflexive r = (r `intersection` id) == zeros

698697

699698-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@

700699connected :: (CountableN a, FromListsN a a) => Relation a a -> Bool

@@ -721,9 +720,9 @@ partialEquivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool

721720partialEquivalence r = partialOrder r && equivalence r

722721

723722-- | A 'Relation' @r@ is 'difunctional' or regular wherever

724−-- @r ``comp`` 'conv' r ``comp`` r == r@

723+-- @r `.` 'conv' r `.` r == r@

725724difunctional :: Relation a b -> Bool

726−difunctional r = r `comp` conv r `comp` r == r

725+difunctional r = r . conv r . r == r

727726

728727-- Relational pairing

729728

@@ -732,17 +731,17 @@ difunctional r = r `comp` conv r `comp` r == r

732731-- NOTE: That this is not a true categorical product, see for instance:

733732--

734733-- @

735−-- | 'fstR' ``comp`` 'splitR' a b ``sse`` a

734+-- | 'fstR' `.` 'splitR' a b ``sse`` a

736735-- 'splitR' a b <=> |

737−-- | 'sndR' ``comp`` 'splitR' a b ``sse`` b

736+-- | 'sndR' `.` 'splitR' a b ``sse`` b

738737-- @

739738--

740739-- __Emphasis__ on the 'sse'.

741740--

742741-- @

743−-- 'splitR' r s ``comp`` f == 'splitR' (r ``comp`` f) (s ``comp`` f)

744−-- (R '><' S) ``comp`` 'splitR' p q == 'splitR' (r ``comp`` p) (s ``comp`` q)

745−-- 'conv' ('splitR' r s) ``comp`` 'splitR' x y == ('conv' r ``comp`` x) ``intersection`` ('conv' s ``comp`` y)

742+-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)

743+-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)

744+-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)

746745-- @

747746--

748747-- @

@@ -761,7 +760,7 @@ splitR (R f) (R g) = R (I.kr f g)

761760-- | Relational pairing first component projection

762761--

763762-- @

764−-- 'fstR' ``comp`` 'splitR' r s ``sse`` r

763+-- 'fstR' `.` 'splitR' r s ``sse`` r

765764-- @

766765fstR ::

767766 forall a b .

@@ -776,7 +775,7 @@ fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))

776775-- | Relational pairing second component projection

777776--

778777-- @

779−-- 'sndR' ``comp`` 'splitR' r s ``sse`` s

778+-- 'sndR' `.` 'splitR' r s ``sse`` s

780779-- @

781780sndR ::

782781 forall a b .

@@ -794,8 +793,8 @@ infixl 4 ><

794793-- | Relational pairing functor

795794--

796795-- @

797−-- r '><' s == 'splitR' (r ``comp`` fstR) (s ``comp`` sndR)

798−-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)

796+-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)

797+-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)

799798-- @

800799(><) ::

801800 ( CountableDimensionsN a b,

@@ -816,13 +815,13 @@ infixl 4 ><

816815-- | Relational coproduct.

817816--

818817-- @

819−-- | 'eitherR' a b ``comp`` 'i1' == a

818+-- | 'eitherR' a b `.` 'i1' == a

820819-- 'eitherR' a b <=> |

821−-- | 'eitherR' a b ``comp`` 'i2' == b

820+-- | 'eitherR' a b `.` 'i2' == b

822821-- @

823822--

824823-- @

825−-- 'eitherR' r s ``comp`` 'conv' ('eitherR' t u) == (r ``comp`` 'conv' t) ``union`` (s ``comp`` 'conv' u)

824+-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)

826825-- @

827826--

828827-- @

@@ -834,8 +833,8 @@ eitherR = join

834833-- | Relational coproduct first component injection

835834--

836835-- @

837−-- 'img' 'i1' ``union`` 'img' 'i2' == 'iden'

838−-- 'i1' ``comp`` 'i2' = 'zeros'

836+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'

837+-- 'i1' `.` 'i2' = 'zeros'

839838-- @

840839i1 ::

841840 ( CountableDimensionsN a b,

@@ -848,8 +847,8 @@ i1 = R I.i1

848847-- | Relational coproduct second component injection

849848--

850849-- @

851−-- 'img' 'i1' ``union`` 'img' 'i2' == 'iden'

852−-- 'i1' ``comp`` 'i2' = 'zeros'

850+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'

851+-- 'i1' `.` 'i2' = 'zeros'

853852-- @

854853i2 ::

855854 ( CountableDimensionsN a b,

@@ -864,7 +863,7 @@ infixl 5 -|-

864863-- | Relational coproduct functor.

865864--

866865-- @

867−-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)

866+-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)

868867-- @

869868(-|-) ::

870869 ( CountableDimensionsN b d,

@@ -897,7 +896,7 @@ trans ::

897896 TrivialP c b

898897 )

899898 => Relation (a, b) c -> Relation a (c, b)

900−trans r = splitR r sndR `comp` conv fstR

899+trans r = splitR r sndR . conv fstR

901900

902901-- | Relational 'untrans'

903902--

@@ -918,17 +917,17 @@ untrans ::

918917 TrivialP c b

919918 )

920919 => Relation a (c, b) -> Relation (a, b) c

921−untrans s = fstR `comp` conv (splitR (conv s) sndR)

920+untrans s = fstR . conv (splitR (conv s) sndR)

922921

923922-- | Transforms predicate @p@ into a correflexive relation.

924923--

925924-- @

926−-- 'predR' ('const' True) == 'iden'

925+-- 'predR' ('const' True) == 'id'

927926-- 'predR' ('const' False) == 'zeros'

928927-- @

929928--

930929-- @

931−-- 'predR' q ``comp`` 'predR' p == 'predR' q ``union`` 'predR' p

930+-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p

932931-- @

933932predR ::

934933 ( Bounded a,

@@ -938,14 +937,14 @@ predR ::

938937 FromListsN Bool a

939938 )

940939 => Relation a Bool -> Relation a a

941−predR p = iden `intersection` divisionF (fromF (const True)) p

940+predR p = id `intersection` divisionF (fromF (const True)) p

942941

943942-- | Equalizes functions @f@ and @g@.

944943-- That is, @'equalizer' f g@ is the largest coreflexive

945944-- that restricts @g@ so that @f@ and @g@ yield the same outputs.

946945--

947946-- @

948−-- 'equalizer' r r == 'iden'

947+-- 'equalizer' r r == 'id'

949948-- 'equalizer' ('point' True) ('point' False) == 'zeros'

950949-- @

951950equalizer ::

@@ -953,12 +952,12 @@ equalizer ::

953952 FromListsN a a

954953 )

955954 => Relation a b -> Relation a b -> Relation a a

956−equalizer f g = iden `intersection` divisionF f g

955+equalizer f g = id `intersection` divisionF f g

957956

958957-- | Relational conditional guard.

959958--

960959-- @

961−-- 'guard' p = 'i2' ``overriddenBy`` 'i1' ``comp`` 'predR' p

960+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p

962961-- @

963962guard ::

964963 ( Bounded b,

@@ -978,27 +977,27 @@ cond ::

978977 FromListsN Bool b

979978 )

980979 => Relation b Bool -> Relation b c -> Relation b c -> Relation b c

981−cond p r s = eitherR r s `comp` guard p

980+cond p r s = eitherR r s . guard p

982981

983982-- | Relational domain.

984983--

985984-- For injective relations, 'domain' and 'ker'nel coincide,

986−-- since @'ker' r ``sse`` 'iden'@ in such situations.

985+-- since @'ker' r ``sse`` 'id'@ in such situations.

987986domain ::

988987 ( CountableN a,

989988 FromListsN a a

990989 ) => Relation a b -> Relation a a

991−domain r = ker r `intersection` iden

990+domain r = ker r `intersection` id

992991

993992-- | Relational range.

994993--

995994-- For functions, 'range' and 'img' (image) coincide,

996−-- since @'img' f ``sse`` 'iden'@ for any @f@.

995+-- since @'img' f ``sse`` id@ for any @f@.

997996range ::

998997 ( CountableN b,

999998 FromListsN b b

1000999 ) => Relation a b -> Relation b b

1001−range r = img r `intersection` iden

1000+range r = img r `intersection` id

10021001

10031002-- Relation pretty print

10041003

src/LAoP/Utils.hs+4−1

@@ -96,7 +96,10 @@ module LAoP.Utils

9696 coerceNat3,

9797

9898 -- * List data type

99− List (..)

99+ List (..),

100+

101+ -- * Category type-class

102+ Category(..)

100103 )

101104where

102105

src/LAoP/Utils/Internal.hs+28−2

@@ -1,9 +1,9 @@

1+{-# LANGUAGE TypeFamilies #-}

12{-# LANGUAGE DeriveGeneric #-}

23{-# LANGUAGE TypeApplications #-}

34{-# LANGUAGE DataKinds #-}

45{-# LANGUAGE FlexibleInstances #-}

56{-# LANGUAGE GeneralizedNewtypeDeriving #-}

6−{-# LANGUAGE KindSignatures #-}

77{-# LANGUAGE ScopedTypeVariables #-}

99module LAoP.Utils.Internal

@@ -19,7 +19,10 @@ module LAoP.Utils.Internal

1919 coerceNat3,

2020

2121 -- * 'List' data type

22− List (..)

22+ List (..),

23+

24+ -- * Category type class

25+ Category(..)

2326 )

2427where

2528

@@ -30,6 +33,9 @@ import Data.Maybe

3033import GHC.TypeLits

3134import Control.DeepSeq

3235import GHC.Generics

36+import Data.Kind

37+import Prelude hiding (id, (.))

38+import qualified Prelude

3339

3440-- | Wrapper around 'Int's that have a restrictive semantic associated.

3541-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'

@@ -168,3 +174,23 @@ instance

168174 fromEnum (L x) =

169175 let as = [minBound .. maxBound]

170176 in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)

177+

178+-- | Constrained category instance

179+class Category k where

180+ type Object k o :: Constraint

181+ type Object k o = ()

182+ id :: Object k a => k a a

183+ (.) :: k b c -> k a b -> k a c

184+

185+{-# RULES

186+"identity/left" forall p .

187+ id . p = p

188+"identity/right" forall p .

189+ p . id = p

190+"association" forall p q r .

191+ (p . q) . r = p . (q . r)

192+ #-}

193+

194+instance Category (->) where

195+ id = Prelude.id

196+ (.) = (Prelude..)