git.iko.soy/laop
on master help sign in
Added constrained Category class!
1da55a0Armando Santos
app/Examples.hs+6−7
compare with master
unifiedsplit
@@ -17,8 +17,7 @@ import LAoP.Dist
17import GHC.TypeLits
17import GHC.TypeLits
18import Data.Coerce
18import Data.Coerce
19import qualified GHC.Generics as G
19import qualified GHC.Generics as G
20−import Control.Category hiding (id)
21−import Prelude hiding ((.))
20+import Prelude hiding (id, (.))
22
21
23-- Monty Hall Problem
22-- Monty Hall Problem
24data Outcome = Win | Lose
23data Outcome = Win | Lose
@@ -76,8 +75,8 @@ sprinkler :: Matrix Double R S
76sprinkler = matrixBuilder gen
75sprinkler = matrixBuilder gen
77 where
76 where
78 gen (No, Off) = 0.6
77 gen (No, Off) = 0.6
79− gen (No, On) = 0.99
78+ gen (No, On) = 0.4
80− gen (Yes, Off) = 0.4
79+ gen (Yes, Off) = 0.99
81 gen (Yes, On) = 0.01
80 gen (Yes, On) = 0.01
82
81
83grass :: Matrix Double (S, R) G
82grass :: Matrix Double (S, R) G
@@ -92,9 +91,9 @@ grass = matrixBuilder gen
92 gen ((On, No), Wet) = 0.9
91 gen ((On, No), Wet) = 0.9
93 gen ((On, Yes), Wet) = 0.99
92 gen ((On, Yes), Wet) = 0.99
94
93
95−tag f = kr f iden
94+tag f = kr f id
96
95
97−state g s r = tag g `comp` tag s `comp` r
96+state g s r = tag g . tag s . r
98
97
99grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
98grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
100grass_wet state = row [0,1] . fstM . state
99grass_wet state = row [0,1] . fstM . state
@@ -173,7 +172,7 @@ exec = do
173 putStrLn "Monty Hall Problem solution:"
172 putStrLn "Monty Hall Problem solution:"
174 prettyPrint (secondChoice . firstChoice)
173 prettyPrint (secondChoice . firstChoice)
175 putStrLn "\n Sum of dices probability:"
174 putStrLn "\n Sum of dices probability:"
176− prettyPrint (sumSSM `comp` kr die die)
175+ prettyPrint (sumSSM . kr die die)
177 putStrLn "\n Conditional dice throw:"
176 putStrLn "\n Conditional dice throw:"
178 prettyPrint conditionalThrows
177 prettyPrint conditionalThrows
179 putStrLn "\n Checking that the last result is indeed a distribution: "
178 putStrLn "\n Checking that the last result is indeed a distribution: "
app/Quantum.hs+4−2
@@ -1,8 +1,10 @@
1{-# LANGUAGE StandaloneDeriving #-}
1{-# LANGUAGE StandaloneDeriving #-}
2module Quantum where
2module Quantum where
3
3
4+import LAoP.Utils
4import LAoP.Matrix.Type
5import LAoP.Matrix.Type
5import Data.Complex
6import Data.Complex
7+import Prelude hiding (id, (.))
6
8
7deriving instance Ord a => Ord (Complex a)
9deriving instance Ord a => Ord (Complex a)
8
10
@@ -11,7 +13,7 @@ xor (False, b) = b
11xor (True, b) = not b
13xor (True, b) = not b
12
14
13ker :: Num e => Matrix e a b -> Matrix e a a
15ker :: Num e => Matrix e a b -> Matrix e a a
14−ker m = tr m `comp` m
16+ker m = tr m . m
15
17
16cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
18cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
17cnot = kr fstM (fromF xor)
19cnot = kr fstM (fromF xor)
@@ -26,4 +28,4 @@ had :: Matrix (Complex Double) Bool Bool
26had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]
28had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]
27
29
28bell :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
30bell :: 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 @@
3module Spreadsheets
3module Spreadsheets
4 where
4 where
5
5
6+import LAoP.Utils
6import LAoP.Matrix.Type
7import LAoP.Matrix.Type
7import GHC.Generics
8import GHC.Generics
9+import Prelude hiding (id, (.))
8
10
9data Student = Student1 | Student2 | Student3 | Student4
11data Student = Student1 | Student2 | Student3 | Student4
10 deriving (Eq, Show, Enum, Bounded, Generic)
12 deriving (Eq, Show, Enum, Bounded, Generic)
@@ -36,10 +38,10 @@ xls :: Matrix Float Question One
36 -> Matrix Float (Either Question Results) (Either One Student)
38 -> Matrix Float (Either Question Results) (Either One Student)
37xls w m t = join (fork w m) (fork zeros r)
39xls w m t = join (fork w m) (fork zeros r)
38 where
40 where
39− rExam = m `comp` tr w
41+ rExam = m . tr w
40 rTest = tr t
42 rTest = tr t
41 rFinal = rTest `maxPW` rExam
43 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)
43
45
44-- | Overloaded, point-wise 'max' function
46-- | Overloaded, point-wise 'max' function
45maxPW :: Ord e => Matrix e a b -> Matrix e a b -> Matrix e a b
47maxPW :: 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
44 where
44 where
45
45
46import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDimensions, CountableN, CountableDimensionsN, Liftable, FromListsN)
46import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDimensions, CountableN, CountableDimensionsN, Liftable, FromListsN)
47+import Prelude hiding (id, (.))
47import qualified LAoP.Matrix.Internal as I
48import qualified LAoP.Matrix.Internal as I
48import LAoP.Utils
49import LAoP.Utils
49import GHC.TypeLits
50import GHC.TypeLits
src/LAoP/Matrix/Internal.hs+13−14
@@ -119,6 +119,7 @@ module LAoP.Matrix.Internal
119
119
120 -- | Note that given the restrictions imposed it is not possible to
120 -- | Note that given the restrictions imposed it is not possible to
121 -- implement the standard type classes present in standard Haskell.
121 -- implement the standard type classes present in standard Haskell.
122+
122 -- *** Matrix pairing projections
123 -- *** Matrix pairing projections
123 fstM,
124 fstM,
124 sndM,
125 sndM,
@@ -169,8 +170,8 @@ import GHC.TypeLits
169import Data.Type.Equality
170import Data.Type.Equality
170import GHC.Generics
171import GHC.Generics
171import Control.DeepSeq
172import Control.DeepSeq
172−import Control.Category
173+import Prelude hiding (id, (.))
173−import Prelude hiding ((.))
174+import qualified Prelude (id, (.))
174
175
175-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
176-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
176data Matrix e cols rows where
177data Matrix e cols rows where
@@ -227,14 +228,12 @@ type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
227type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
228type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
228type Trivial a = FromNat (Count a) ~ a
229type Trivial a = FromNat (Count a) ~ a
229
230
230−-- | It isn't possible to implement the 'id' function so it's
231+-- | It is possible to implement a constrained version of the category type
231−-- implementation is 'undefined'. However 'comp' can be and this partial
232+-- class.
232−-- class implementation exists just to make the code more readable.
233−--
234−-- Please use 'iden' instead.
235instance (Num e) => Category (Matrix e) where
233instance (Num e) => Category (Matrix e) where
236− id = undefined
234+ type Object (Matrix e) a = (FromLists e a a, Countable a)
235+ id = iden
237− (.) = comp
236+ (.) = comp
238
237
239instance NFData e => NFData (Matrix e cols rows) where
238instance NFData e => NFData (Matrix e cols rows) where
240 rnf Empty = ()
239 rnf Empty = ()
@@ -501,7 +500,7 @@ bang =
501-- iden Matrix
500-- iden Matrix
502
501
503-- | iden matrix.
502-- | 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
505iden = matrixBuilder' (bool 0 1 . uncurry (==))
504iden = matrixBuilder' (bool 0 1 . uncurry (==))
506{-# NOINLINE iden #-}
505{-# NOINLINE iden #-}
507
506
@@ -547,11 +546,11 @@ infixl 7 ./
547
546
548-- | Biproduct first component projection
547-- | Biproduct first component projection
549p1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
548p1 :: (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
551
550
552-- | Biproduct second component projection
551-- | Biproduct second component projection
553p2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
552p2 :: (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
555
554
556-- Injections
555-- Injections
557
556
@@ -728,7 +727,7 @@ tr (Fork a b) = Join (tr a) (tr b)
728select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
727select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
729select (Fork a b) y = y . a + b -- Divide-and-conquer law
728select (Fork a b) y = y . a + b -- Divide-and-conquer law
730select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
729select (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
732
731
733branch ::
732branch ::
734 ( Num e,
733 ( Num e,
@@ -797,7 +796,7 @@ corr ::
797 )
796 )
798 => (a -> Bool) -> Matrix e q q
797 => (a -> Bool) -> Matrix e q q
799corr p = let f = fromF' p :: Matrix e q ()
798corr 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)
801
800
802-- Pretty print
801-- Pretty print
803
802
src/LAoP/Matrix/Nat.hs−10
@@ -161,7 +161,6 @@ where
161import Data.Proxy
161import Data.Proxy
162import GHC.TypeLits
162import GHC.TypeLits
163import Control.DeepSeq
163import Control.DeepSeq
164−import qualified Control.Category as C
165import qualified LAoP.Matrix.Internal as I
164import qualified LAoP.Matrix.Internal as I
166
165
167newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
166newtype 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
179type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)
178type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)
180type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
179type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
181
180
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−
191-- Primitives
181-- Primitives
192
182
193empty :: Matrix e 0 0
183empty :: Matrix e 0 0
src/LAoP/Matrix/Type.hs+12−13
@@ -1,4 +1,5 @@
1{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE ConstraintKinds #-}
2+{-# LANGUAGE TypeFamilies #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DerivingVia #-}
5{-# LANGUAGE DerivingVia #-}
@@ -185,8 +186,8 @@ import Data.Kind
185import GHC.TypeLits
186import GHC.TypeLits
186import Control.DeepSeq
187import Control.DeepSeq
187import LAoP.Utils
188import LAoP.Utils
188−import qualified Control.Category as C
189import qualified LAoP.Matrix.Internal as I
189import qualified LAoP.Matrix.Internal as I
190+import Prelude hiding (id, (.))
190
191
191newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
192 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
193 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)
203type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)
204type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)
204type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
205type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
205
206
206−-- | It isn't possible to implement the 'id' function so it's
207+-- | It is possible to implement a constrained version of the category type
207−-- implementation is 'undefined'. However 'comp' can be and this partial
208+-- class.
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
209+instance (Num e) => Category (Matrix e) where
212− id = undefined
210+ type Object (Matrix e) a = (FromListsN e a a, CountableN a)
211+ id = iden
213− (.) = comp
212+ (.) = comp
214
213
215-- | Bifunctor equivalent function
214-- | Bifunctor equivalent function
216bimapM ::
215bimapM ::
@@ -221,7 +220,7 @@ bimapM ::
221 FromListsN e d c,
220 FromListsN e d c,
222 FromListsN e b a
221 FromListsN e b a
223 ) => (a -> b) -> (c -> d) -> Matrix e a c -> Matrix e b d
222 ) => (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)
225
224
226-- | Zero type alias
225-- | Zero type alias
227type Zero = Void
226type Zero = Void
@@ -279,7 +278,7 @@ fmapM ::
279 )
278 )
280 =>
279 =>
281 (a -> b) -> Matrix e c a -> Matrix e c b
280 (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
283
282
284-- | Applicative instance equivalent 'unit' function,
283-- | Applicative instance equivalent 'unit' function,
285unitM :: (Num e) => Matrix e () ()
284unitM :: (Num e) => Matrix e () ()
@@ -586,9 +585,9 @@ sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
586-- NOTE: That this is not a true categorical product, see for instance:
585-- NOTE: That this is not a true categorical product, see for instance:
587--
586--
588-- @
587-- @
589−-- | fstM `comp` kr a b == a
588+-- | fstM . kr a b == a
590-- kr a b ==> |
589-- kr a b ==> |
591−-- | sndM `comp` kr a b == b
590+-- | sndM . kr a b == b
592-- @
591-- @
593--
592--
594-- __Emphasis__ on the implication symbol.
593-- __Emphasis__ on the implication symbol.
src/LAoP/Relation/Internal.hs+65−66
@@ -1,3 +1,4 @@
1+{-# LANGUAGE TypeFamilies #-}
1{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE GADTs #-}
3{-# LANGUAGE GADTs #-}
3{-# LANGUAGE UndecidableInstances #-}
4{-# LANGUAGE UndecidableInstances #-}
@@ -178,9 +179,9 @@ import Data.Void
178import qualified LAoP.Matrix.Internal as I
179import qualified LAoP.Matrix.Internal as I
179import LAoP.Utils.Internal
180import LAoP.Utils.Internal
180import Control.DeepSeq
181import Control.DeepSeq
181−import qualified Control.Category as C
182import Data.Bool
182import Data.Bool
183import GHC.TypeLits
183import GHC.TypeLits
184+import Prelude hiding (id, (.))
184
185
185-- | Boolean type synonym for working with boolean matrices
186-- | Boolean type synonym for working with boolean matrices
186type Boolean = Natural 0 1
187type Boolean = Natural 0 1
@@ -202,14 +203,12 @@ type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num
202type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
203type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
203type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
204type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
204
205
205−-- | It isn't possible to implement the 'id' function so it's
206+-- | It is possible to implement a constrained version of the category type
206−-- implementation is 'undefined'. However 'comp' can be and this partial
207+-- class.
207−-- class implementation exists just to make the code more readable.
208−--
209−-- Please use 'iden' instead.
210−instance C.Category Relation where
208+instance Category Relation where
211− id = undefined
209+ type Object Relation a = (FromListsN a a, CountableN a)
210+ id = iden
212− (.) = comp
211+ (.) = comp
213
212
214instance Num (Relation a b) where
213instance Num (Relation a b) where
215 -- | Matrix addition becomes Boolean matrix disjointion
214 -- | Matrix addition becomes Boolean matrix disjointion
@@ -387,7 +386,7 @@ belongs = toRel elemR
387-- Also known as ⊥ (Bottom) Relation or empty Relation.
386-- Also known as ⊥ (Bottom) Relation or empty Relation.
388--
387--
389-- @
388-- @
390−-- r ``comp`` ⊥ == ⊥ ``comp`` r == ⊥
389+-- r `.` ⊥ == ⊥ `.` r == ⊥
391-- ⊥ ``sse`` R && R ``sse`` T == True
390-- ⊥ ``sse`` R && R ``sse`` T == True
392-- @
391-- @
393zeros ::
392zeros ::
@@ -433,7 +432,7 @@ point = fromF . const
433-- | iden matrix
432-- | iden matrix
434--
433--
435-- @
434-- @
436−-- 'iden' ``comp`` r == r == r ``comp`` 'iden'
435+-- 'iden' `.` r == r == r `.` 'iden'
437-- @
436-- @
438iden ::
437iden ::
439 (FromListsN a a, CountableN a) => Relation a a
438 (FromListsN a a, CountableN a) => Relation a a
@@ -442,7 +441,7 @@ iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))
442-- | Relational composition
441-- | Relational composition
443--
442--
444-- @
443-- @
445−-- r ``comp`` (s ``comp`` p) = (r ``comp`` s) ``comp`` p
444+-- r `.` (s `.` p) = (r `.` s) `.` p
446-- @
445-- @
447comp :: Relation b c -> Relation a b -> Relation a c
446comp :: Relation b c -> Relation a b -> Relation a c
448comp (R a) (R b) = R (I.compRel a b)
447comp (R a) (R b) = R (I.compRel a b)
@@ -506,7 +505,7 @@ pointAp ::
506 FromListsN a One,
505 FromListsN a One,
507 FromListsN b One
506 FromListsN b One
508 ) => a -> b -> Relation a b -> Relation One One
507 ) => 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
510
509
511-- | Relational application
510-- | Relational application
512--
511--
@@ -518,7 +517,7 @@ pointApBool ::
518 FromListsN a One,
517 FromListsN a One,
519 FromListsN b One
518 FromListsN b One
520 ) => a -> b -> Relation a b -> Bool
519 ) => 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
522
521
523-- | Relational converse
522-- | Relational converse
524--
523--
@@ -560,8 +559,8 @@ intersection a b = a * b
560-- @
559-- @
561-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
560-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
562-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
561-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
563−-- r ``comp`` (s ``union`` t) == (r ``comp`` s) ``union`` (r ``comp`` t)
562+-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)
564−-- (s ``union`` t) ``comp`` r == (s ``comp`` r) ``union`` (t ``comp`` r)
563+-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)
565-- @
564-- @
566union :: Relation a b -> Relation a b -> Relation a b
565union :: Relation a b -> Relation a b -> Relation a b
567union a b = a + b
566union a b = a + b
@@ -569,29 +568,29 @@ union a b = a + b
569-- | Relation Kernel
568-- | Relation Kernel
570--
569--
571-- @
570-- @
572−-- 'ker' r == 'conv' r ``comp`` r
571+-- 'ker' r == 'conv' r `.` r
573-- 'ker' r == 'img' ('conv' r)
572-- 'ker' r == 'img' ('conv' r)
574-- @
573-- @
575ker :: Relation a b -> Relation a a
574ker :: Relation a b -> Relation a a
576−ker r = conv r `comp` r
575+ker r = conv r . r
577
576
578-- | Relation Image
577-- | Relation Image
579--
578--
580-- @
579-- @
581−-- 'img' r == r ``comp`` conv r
580+-- 'img' r == r `.` conv r
582-- 'img' r == 'ker' ('conv' r)
581-- 'img' r == 'ker' ('conv' r)
583-- @
582-- @
584img :: Relation a b -> Relation b b
583img :: Relation a b -> Relation b b
585−img r = r `comp` conv r
584+img r = r . conv r
586
585
587-- | Function division. Special case of 'divS'.
586-- | Function division. Special case of 'divS'.
588--
587--
589-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
588-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
590-- 'entire'.
589-- 'entire'.
591--
590--
592−-- @'divisionF' f g == 'conv' g ``comp`` f@
591+-- @'divisionF' f g == 'conv' g `.` f@
593divisionF :: Relation a c -> Relation b c -> Relation a b
592divisionF :: Relation a c -> Relation b c -> Relation a b
594−divisionF f g = conv g `comp` f
593+divisionF f g = conv g . f
595
594
596-- Taxonomy of binary relations
595-- Taxonomy of binary relations
597
596
@@ -617,8 +616,8 @@ surjective = reflexive . img
617-- relations:
616-- relations:
618--
617--
619-- @
618-- @
620−-- f ``comp`` r ``sse`` s == r ``sse`` f ``comp`` s
619+-- f `.` r ``sse`` s == r ``sse`` f `.` s
621−-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
620+-- r `.` f ``sse`` s == r ``sse`` s `.` f
622-- @
621-- @
623function ::
622function ::
624 ( CountableDimensionsN a b,
623 ( CountableDimensionsN a b,
@@ -672,29 +671,29 @@ bijection r = injection r && surjection r
672
671
673-- Properties of relations
672-- Properties of relations
674
673
675−-- | A 'Relation' @r@ is 'reflexive' 'iff' @'iden' ``sse`` r@
674+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@
676reflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
675reflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
677−reflexive r = iden <= r
676+reflexive r = id <= r
678
677
679−-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'iden'@
678+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
680coreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
679coreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
681−coreflexive r = r <= iden
680+coreflexive r = r <= id
682
681
683−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
682+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
684transitive :: Relation a a -> Bool
683transitive :: Relation a a -> Bool
685−transitive r = (r `comp` r) `sse` r
684+transitive r = (r . r) `sse` r
686
685
687-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
686-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
688symmetric :: Relation a a -> Bool
687symmetric :: Relation a a -> Bool
689symmetric r = r == conv r
688symmetric r = r == conv r
690
689
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'@
692antiSymmetric :: (CountableN a, FromListsN a a) => Relation a a -> Bool
691antiSymmetric :: (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
694
693
695−-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'iden') == 'zeros'@
694+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@
696irreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
695irreflexive :: (CountableN a, FromListsN a a) => Relation a a -> Bool
697−irreflexive r = (r `intersection` iden) == zeros
696+irreflexive r = (r `intersection` id) == zeros
698
697
699-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
698-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
700connected :: (CountableN a, FromListsN a a) => Relation a a -> Bool
699connected :: (CountableN a, FromListsN a a) => Relation a a -> Bool
@@ -721,9 +720,9 @@ partialEquivalence :: (CountableN a, FromListsN a a) => Relation a a -> Bool
721partialEquivalence r = partialOrder r && equivalence r
720partialEquivalence r = partialOrder r && equivalence r
722
721
723-- | A 'Relation' @r@ is 'difunctional' or regular wherever
722-- | A 'Relation' @r@ is 'difunctional' or regular wherever
724−-- @r ``comp`` 'conv' r ``comp`` r == r@
723+-- @r `.` 'conv' r `.` r == r@
725difunctional :: Relation a b -> Bool
724difunctional :: Relation a b -> Bool
726−difunctional r = r `comp` conv r `comp` r == r
725+difunctional r = r . conv r . r == r
727
726
728-- Relational pairing
727-- Relational pairing
729
728
@@ -732,17 +731,17 @@ difunctional r = r `comp` conv r `comp` r == r
732-- NOTE: That this is not a true categorical product, see for instance:
731-- NOTE: That this is not a true categorical product, see for instance:
733--
732--
734-- @
733-- @
735−-- | 'fstR' ``comp`` 'splitR' a b ``sse`` a
734+-- | 'fstR' `.` 'splitR' a b ``sse`` a
736-- 'splitR' a b <=> |
735-- 'splitR' a b <=> |
737−-- | 'sndR' ``comp`` 'splitR' a b ``sse`` b
736+-- | 'sndR' `.` 'splitR' a b ``sse`` b
738-- @
737-- @
739--
738--
740-- __Emphasis__ on the 'sse'.
739-- __Emphasis__ on the 'sse'.
741--
740--
742-- @
741-- @
743−-- 'splitR' r s ``comp`` f == 'splitR' (r ``comp`` f) (s ``comp`` f)
742+-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)
744−-- (R '><' S) ``comp`` 'splitR' p q == 'splitR' (r ``comp`` p) (s ``comp`` q)
743+-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)
745−-- 'conv' ('splitR' r s) ``comp`` 'splitR' x y == ('conv' r ``comp`` x) ``intersection`` ('conv' s ``comp`` y)
744+-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)
746-- @
745-- @
747--
746--
748-- @
747-- @
@@ -761,7 +760,7 @@ splitR (R f) (R g) = R (I.kr f g)
761-- | Relational pairing first component projection
760-- | Relational pairing first component projection
762--
761--
763-- @
762-- @
764−-- 'fstR' ``comp`` 'splitR' r s ``sse`` r
763+-- 'fstR' `.` 'splitR' r s ``sse`` r
765-- @
764-- @
766fstR ::
765fstR ::
767 forall a b .
766 forall a b .
@@ -776,7 +775,7 @@ fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
776-- | Relational pairing second component projection
775-- | Relational pairing second component projection
777--
776--
778-- @
777-- @
779−-- 'sndR' ``comp`` 'splitR' r s ``sse`` s
778+-- 'sndR' `.` 'splitR' r s ``sse`` s
780-- @
779-- @
781sndR ::
780sndR ::
782 forall a b .
781 forall a b .
@@ -794,8 +793,8 @@ infixl 4 ><
794-- | Relational pairing functor
793-- | Relational pairing functor
795--
794--
796-- @
795-- @
797−-- r '><' s == 'splitR' (r ``comp`` fstR) (s ``comp`` sndR)
796+-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
798−-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
797+-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
799-- @
798-- @
800(><) ::
799(><) ::
801 ( CountableDimensionsN a b,
800 ( CountableDimensionsN a b,
@@ -816,13 +815,13 @@ infixl 4 ><
816-- | Relational coproduct.
815-- | Relational coproduct.
817--
816--
818-- @
817-- @
819−-- | 'eitherR' a b ``comp`` 'i1' == a
818+-- | 'eitherR' a b `.` 'i1' == a
820-- 'eitherR' a b <=> |
819-- 'eitherR' a b <=> |
821−-- | 'eitherR' a b ``comp`` 'i2' == b
820+-- | 'eitherR' a b `.` 'i2' == b
822-- @
821-- @
823--
822--
824-- @
823-- @
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)
826-- @
825-- @
827--
826--
828-- @
827-- @
@@ -834,8 +833,8 @@ eitherR = join
834-- | Relational coproduct first component injection
833-- | Relational coproduct first component injection
835--
834--
836-- @
835-- @
837−-- 'img' 'i1' ``union`` 'img' 'i2' == 'iden'
836+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
838−-- 'i1' ``comp`` 'i2' = 'zeros'
837+-- 'i1' `.` 'i2' = 'zeros'
839-- @
838-- @
840i1 ::
839i1 ::
841 ( CountableDimensionsN a b,
840 ( CountableDimensionsN a b,
@@ -848,8 +847,8 @@ i1 = R I.i1
848-- | Relational coproduct second component injection
847-- | Relational coproduct second component injection
849--
848--
850-- @
849-- @
851−-- 'img' 'i1' ``union`` 'img' 'i2' == 'iden'
850+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
852−-- 'i1' ``comp`` 'i2' = 'zeros'
851+-- 'i1' `.` 'i2' = 'zeros'
853-- @
852-- @
854i2 ::
853i2 ::
855 ( CountableDimensionsN a b,
854 ( CountableDimensionsN a b,
@@ -864,7 +863,7 @@ infixl 5 -|-
864-- | Relational coproduct functor.
863-- | Relational coproduct functor.
865--
864--
866-- @
865-- @
867−-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
866+-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
868-- @
867-- @
869(-|-) ::
868(-|-) ::
870 ( CountableDimensionsN b d,
869 ( CountableDimensionsN b d,
@@ -897,7 +896,7 @@ trans ::
897 TrivialP c b
896 TrivialP c b
898 )
897 )
899 => Relation (a, b) c -> Relation a (c, b)
898 => 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
901
900
902-- | Relational 'untrans'
901-- | Relational 'untrans'
903--
902--
@@ -918,17 +917,17 @@ untrans ::
918 TrivialP c b
917 TrivialP c b
919 )
918 )
920 => Relation a (c, b) -> Relation (a, b) c
919 => 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)
922
921
923-- | Transforms predicate @p@ into a correflexive relation.
922-- | Transforms predicate @p@ into a correflexive relation.
924--
923--
925-- @
924-- @
926−-- 'predR' ('const' True) == 'iden'
925+-- 'predR' ('const' True) == 'id'
927-- 'predR' ('const' False) == 'zeros'
926-- 'predR' ('const' False) == 'zeros'
928-- @
927-- @
929--
928--
930-- @
929-- @
931−-- 'predR' q ``comp`` 'predR' p == 'predR' q ``union`` 'predR' p
930+-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p
932-- @
931-- @
933predR ::
932predR ::
934 ( Bounded a,
933 ( Bounded a,
@@ -938,14 +937,14 @@ predR ::
938 FromListsN Bool a
937 FromListsN Bool a
939 )
938 )
940 => Relation a Bool -> Relation a a
939 => 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
942
941
943-- | Equalizes functions @f@ and @g@.
942-- | Equalizes functions @f@ and @g@.
944-- That is, @'equalizer' f g@ is the largest coreflexive
943-- That is, @'equalizer' f g@ is the largest coreflexive
945-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
944-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
946--
945--
947-- @
946-- @
948−-- 'equalizer' r r == 'iden'
947+-- 'equalizer' r r == 'id'
949-- 'equalizer' ('point' True) ('point' False) == 'zeros'
948-- 'equalizer' ('point' True) ('point' False) == 'zeros'
950-- @
949-- @
951equalizer ::
950equalizer ::
@@ -953,12 +952,12 @@ equalizer ::
953 FromListsN a a
952 FromListsN a a
954 )
953 )
955 => Relation a b -> Relation a b -> Relation a a
954 => 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
957
956
958-- | Relational conditional guard.
957-- | Relational conditional guard.
959--
958--
960-- @
959-- @
961−-- 'guard' p = 'i2' ``overriddenBy`` 'i1' ``comp`` 'predR' p
960+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p
962-- @
961-- @
963guard ::
962guard ::
964 ( Bounded b,
963 ( Bounded b,
@@ -978,27 +977,27 @@ cond ::
978 FromListsN Bool b
977 FromListsN Bool b
979 )
978 )
980 => Relation b Bool -> Relation b c -> Relation b c -> Relation b c
979 => 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
982
981
983-- | Relational domain.
982-- | Relational domain.
984--
983--
985-- For injective relations, 'domain' and 'ker'nel coincide,
984-- 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.
987domain ::
986domain ::
988 ( CountableN a,
987 ( CountableN a,
989 FromListsN a a
988 FromListsN a a
990 ) => Relation a b -> Relation a a
989 ) => Relation a b -> Relation a a
991−domain r = ker r `intersection` iden
990+domain r = ker r `intersection` id
992
991
993-- | Relational range.
992-- | Relational range.
994--
993--
995-- For functions, 'range' and 'img' (image) coincide,
994-- 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@.
997range ::
996range ::
998 ( CountableN b,
997 ( CountableN b,
999 FromListsN b b
998 FromListsN b b
1000 ) => Relation a b -> Relation b b
999 ) => Relation a b -> Relation b b
1001−range r = img r `intersection` iden
1000+range r = img r `intersection` id
1002
1001
1003-- Relation pretty print
1002-- Relation pretty print
1004
1003
src/LAoP/Utils.hs+4−1
@@ -96,7 +96,10 @@ module LAoP.Utils
96 coerceNat3,
96 coerceNat3,
97
97
98 -- * List data type
98 -- * List data type
99− List (..)
99+ List (..),
100+
101+ -- * Category type-class
102+ Category(..)
100 )
103 )
101where
104where
102
105
src/LAoP/Utils/Internal.hs+28−2
@@ -1,9 +1,9 @@
1+{-# LANGUAGE TypeFamilies #-}
1{-# LANGUAGE DeriveGeneric #-}
2{-# LANGUAGE DeriveGeneric #-}
2{-# LANGUAGE TypeApplications #-}
3{-# LANGUAGE TypeApplications #-}
3{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE GeneralizedNewtypeDeriving #-}
6{-# LANGUAGE GeneralizedNewtypeDeriving #-}
6−{-# LANGUAGE KindSignatures #-}
7{-# LANGUAGE ScopedTypeVariables #-}
7{-# LANGUAGE ScopedTypeVariables #-}
8
8
9module LAoP.Utils.Internal
9module LAoP.Utils.Internal
@@ -19,7 +19,10 @@ module LAoP.Utils.Internal
19 coerceNat3,
19 coerceNat3,
20
20
21 -- * 'List' data type
21 -- * 'List' data type
22− List (..)
22+ List (..),
23+
24+ -- * Category type class
25+ Category(..)
23 )
26 )
24where
27where
25
28
@@ -30,6 +33,9 @@ import Data.Maybe
30import GHC.TypeLits
33import GHC.TypeLits
31import Control.DeepSeq
34import Control.DeepSeq
32import GHC.Generics
35import GHC.Generics
36+import Data.Kind
37+import Prelude hiding (id, (.))
38+import qualified Prelude
33
39
34-- | Wrapper around 'Int's that have a restrictive semantic associated.
40-- | Wrapper around 'Int's that have a restrictive semantic associated.
35-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
41-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
@@ -168,3 +174,23 @@ instance
168 fromEnum (L x) =
174 fromEnum (L x) =
169 let as = [minBound .. maxBound]
175 let as = [minBound .. maxBound]
170 in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)
176 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..)