7c95b00 · laop · git.iko.soy

git.iko.soy/laop

Small tweaks on the Utils/Matrix.Internal/Matrix.Nat/Matrix.Type modules. Added Relation module

commit7c95b008748fd99686fa1d38c3ca83f00998f596 authorArmando Santos <armandoifsantos@gmail.com> dateTue 31 Dec 2019, 18:26 (7 years ago) parentbf2cb96

6 files changed+300−4

compare with master

unifiedsplit

src/Matrix/Internal.hs+137−1 src/Matrix/Nat.hs+1−1 src/Matrix/Type.hs+1−1 src/Relation/Internal.hs+141 src/Utils.hs+1 src/Utils/Internal.hs+19−1

src/Matrix/Internal.hs+137−1

@@ -128,7 +128,17 @@ module Matrix.Internal

128128

129129 -- * Matrix printing

130130 pretty,

131− prettyPrint

131+ prettyPrint,

132+

133+ -- * Other

134+ toBool,

135+ fromBool,

136+ compRel,

137+ fromFRel,

138+ fromFRel',

139+ orM,

140+ andM,

141+ subM

132142 )

133143 where

134144

@@ -245,6 +255,14 @@ instance Num e => Num (Matrix e cols rows) where

245255 signum (Junc a b) = Junc (signum a) (signum b)

246256 signum (Split a b) = Split (signum a) (signum b)

247257

258+instance Ord e => Ord (Matrix e cols rows) where

259+ Empty <= Empty = True

260+ (One a) <= (One b) = a <= b

261+ (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)

262+ (Split a b) <= (Split c d) = (a <= c) && (b <= d)

263+ x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y

264+ x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y

265+

248266-- Primitives

249267

250268-- | Empty matrix constructor

@@ -779,3 +797,121 @@ pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++

779797-- | Matrix pretty printer

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

781799prettyPrint = putStrLn . pretty

800+

801+-- Relational operators functions

802+

803+-- | Helper conversion function

804+toBool :: (Num e, Eq e) => e -> Bool

805+toBool n

806+ | n == 0 = False

807+ | n == 1 = True

808+

809+-- | Helper conversion function

810+fromBool :: Bool -> Natural 0 1

811+fromBool True = nat 1

812+fromBool False = nat 0

813+

814+-- | Relational addition

815+orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

816+orM Empty Empty = Empty

817+orM (One a) (One b) = One (fromBool (toBool a || toBool b))

818+orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)

819+orM (Split a b) (Split c d) = Split (orM a c) (orM b d)

820+orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)

821+orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y

822+

823+-- | Relational multiplication

824+andM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

825+andM Empty Empty = Empty

826+andM (One a) (One b) = One (fromBool (toBool a && toBool b))

827+andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)

828+andM (Split a b) (Split c d) = Split (andM a c) (andM b d)

829+andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)

830+andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y

831+

832+-- | Relational subtraction

833+subM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

834+subM Empty Empty = Empty

835+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)

836+subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)

837+subM (Split a b) (Split c d) = Split (subM a c) (subM b d)

838+subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)

839+subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y

840+

841+-- | Matrix relational composition.

842+compRel :: Matrix (Natural 0 1) cr rows -> Matrix (Natural 0 1) cols cr -> Matrix (Natural 0 1) cols rows

843+compRel Empty Empty = Empty

844+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))

845+compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law

846+compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law

847+compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law

848+

849+-- | Lifts functions to relations with arbitrary dimensions.

850+--

851+-- NOTE: Be careful to not ask for a relation bigger than the cardinality of

852+-- types @a@ or @b@ allows.

853+fromFRel ::

854+ forall a b cols rows.

855+ ( Bounded a,

856+ Bounded b,

857+ Enum a,

858+ Enum b,

859+ Eq b,

860+ KnownNat (Count cols),

861+ KnownNat (Count rows),

862+ FromLists (Natural 0 1) rows cols

863+ ) =>

864+ (a -> b) ->

865+ Matrix (Natural 0 1) cols rows

866+fromFRel f =

867+ let minA = minBound @a

868+ maxA = maxBound @a

869+ minB = minBound @b

870+ maxB = maxBound @b

871+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))

872+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))

873+ elementsA = take ccols [minA .. maxA]

874+ elementsB = take rrows [minB .. maxB]

875+ combinations = (,) <$> elementsA <*> elementsB

876+ combAp = map snd . sort . map (\(a, b) -> if f a == b

877+ then ((fromEnum a, fromEnum b), nat 1)

878+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations

879+ mList = buildList combAp rrows

880+ in tr $ fromLists mList

881+ where

882+ buildList [] _ = []

883+ buildList l r = take r l : buildList (drop r l) r

884+

885+-- | Lifts functions to relations with dimensions matching @a@ and @b@

886+-- cardinality's.

887+fromFRel' ::

888+ forall a b.

889+ ( Bounded a,

890+ Bounded b,

891+ Enum a,

892+ Enum b,

893+ Eq b,

894+ KnownNat (Count (Normalize a)),

895+ KnownNat (Count (Normalize b)),

896+ FromLists (Natural 0 1) (Normalize b) (Normalize a)

897+ ) =>

898+ (a -> b) ->

899+ Matrix (Natural 0 1) (Normalize a) (Normalize b)

900+fromFRel' f =

901+ let minA = minBound @a

902+ maxA = maxBound @a

903+ minB = minBound @b

904+ maxB = maxBound @b

905+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))

906+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))

907+ elementsA = take ccols [minA .. maxA]

908+ elementsB = take rrows [minB .. maxB]

909+ combinations = (,) <$> elementsA <*> elementsB

910+ combAp = map snd . sort . map (\(a, b) -> if f a == b

911+ then ((fromEnum a, fromEnum b), nat 1)

912+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations

913+ mList = buildList combAp rrows

914+ in tr $ fromLists mList

915+ where

916+ buildList [] _ = []

917+ buildList l r = take r l : buildList (drop r l) r

src/Matrix/Nat.hs+1−1

@@ -145,7 +145,7 @@ import qualified Control.Category as C

145145import qualified Matrix.Internal as I

146146

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

148− deriving (Show, Num, Eq, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))

148+ deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))

149149

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

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

src/Matrix/Type.hs+1−1

@@ -153,7 +153,7 @@ import qualified Control.Category as C

153153import qualified Matrix.Internal as I

154154

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

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

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

157157

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

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

src/Relation/Internal.hsnew file+141

@@ -0,0 +1,141 @@

1+{-# LANGUAGE GADTs #-}

2+{-# LANGUAGE UndecidableInstances #-}

3+{-# LANGUAGE FlexibleContexts #-}

4+{-# LANGUAGE ScopedTypeVariables #-}

5+{-# LANGUAGE StandaloneDeriving #-}

6+{-# LANGUAGE DerivingVia #-}

7+{-# LANGUAGE DataKinds #-}

9+module Relation.Internal

10+ (

11+ )

12+ where

13+

14+import Data.Void

15+import qualified Matrix.Internal as I

16+import Utils

17+import Control.DeepSeq

18+import qualified Control.Category as C

19+import Data.Coerce

20+import GHC.TypeLits

21+

22+type Boolean = Natural 0 1

23+newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))

24+ deriving (Show, Eq, Ord, NFData) via (I.Matrix (Natural 1 1) (I.Normalize a) (I.Normalize b))

25+

26+deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)

27+

28+instance C.Category Relation where

29+ id = undefined

30+ (.) = comp

31+

32+instance Num (Relation a b) where

33+ (R a) + (R b) = R (I.orM a b)

34+

35+ (R a) - (R b) = R (I.subM a b)

36+

37+ (R a) * (R b) = R (I.andM a b)

38+

39+-- Type alias

40+type Zero = Void

41+type One = ()

42+

43+-- Primitives

44+

45+empty :: Relation Zero Zero

46+empty = R I.Empty

47+

48+one :: Boolean -> Relation One One

49+one = R . I.One

50+

51+junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))

52+ => Relation a c -> Relation b c -> Relation (Either a b) c

53+junc (R a) (R b) = R (I.Junc a b)

54+

55+split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))

56+ => Relation c a -> Relation c b -> Relation c (Either a b)

57+split (R a) (R b) = R (I.Split a b)

58+

59+-- Construction

60+

61+fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b

62+fromLists = R . I.fromLists

63+

64+identity :: (KnownNat (I.Count (I.Normalize a)),I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a

65+identity = R I.identity

66+

67+fromF ::

68+ ( Bounded a,

69+ Bounded b,

70+ Enum a,

71+ Enum b,

72+ Eq b,

73+ KnownNat (I.Count (I.Normalize c)),

74+ KnownNat (I.Count (I.Normalize d)),

75+ I.FromLists Boolean (I.Normalize d) (I.Normalize c)

76+ )

77+ => (a -> b) -> Relation c d

78+fromF f = R (I.fromFRel f)

79+

80+fromF' ::

81+ ( Bounded b,

82+ Bounded a,

83+ Enum a,

84+ Enum b,

85+ Eq b,

86+ KnownNat (I.Count (I.Normalize a)),

87+ KnownNat (I.Count (I.Normalize b)),

88+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)

89+ )

90+ => (a -> b) -> Relation a b

91+fromF' f = R (I.fromFRel' f)

92+

93+-- | Relational composition

94+comp :: forall a b c . Relation b c -> Relation a b -> Relation a c

95+comp (R a) (R b) = R (I.compRel a b)

96+

97+-- | Relational converse

98+conv :: Relation a b -> Relation b a

99+conv (R a) = R (I.tr a)

100+

101+-- | Relational inclusion (subset or equal)

102+sse :: Relation a b -> Relation a b -> Bool

103+sse a b = a <= b

104+

105+-- | Relational intersection

106+--

107+-- @M `inter` N = M * N@

108+intersection :: Relation a b -> Relation a b -> Relation a b

109+intersection a b = a * b

110+

111+-- | Relational union

112+--

113+-- @M `union` N = M + N - M * N

114+union :: Relation a b -> Relation a b -> Relation a b

115+union a b = a + b - a * b

116+

117+-- | Relation Kernel

118+ker :: Relation a b -> Relation a a

119+ker r = conv r `comp` r

120+

121+-- | Relation Image

122+img :: Relation a b -> Relation b b

123+img r = r `comp` conv r

124+

125+-- | Properties of relations

126+coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

127+coreflexive r = r <= identity

128+

129+simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool

130+simple = coreflexive . img

131+

132+injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool

133+injective = simple . conv

134+

135+-- | Relation pretty printing

136+pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String

137+pretty (R a) = I.pretty a

138+

139+-- | Relation pretty printing

140+prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()

141+prettyPrint (R a) = I.prettyPrint a

src/Utils.hs+1

@@ -93,6 +93,7 @@ module Utils

9393 -- 'Natural' typed functions.

9494 coerceNat,

9595 coerceNat2,

96+ coerceNat3,

9697 )

9798where

9899

src/Utils/Internal.hs+19−1

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

1+{-# LANGUAGE TypeApplications #-}

12{-# LANGUAGE DataKinds #-}

23{-# LANGUAGE FlexibleInstances #-}

34{-# LANGUAGE GeneralizedNewtypeDeriving #-}

@@ -84,18 +85,30 @@ module Utils.Internal

8485 -- 'Natural' typed functions.

8586 coerceNat,

8687 coerceNat2,

88+ coerceNat3,

8789 )

8890where

8991

9092import Data.Coerce

9193import Data.Proxy

9294import GHC.TypeLits

95+import Control.DeepSeq

9396

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

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

9699-- @i@ that's @n <= i <= m@.

97100newtype Natural (start :: Nat) (end :: Nat) = Nat Int

98− deriving (Show, Read, Eq, Num)

101+ deriving (Show, Read, Eq, Ord, NFData)

102+

103+-- | Throws a runtime error if any of the operations overflows or

104+-- underflows.

105+instance (KnownNat n, KnownNat m) => Num (Natural n m) where

106+ (Nat a) + (Nat b) = nat @n @m (a + b)

107+ (Nat a) - (Nat b) = nat @n @m (a - b)

108+ (Nat a) * (Nat b) = nat @n @m (a * b)

109+ abs (Nat a) = nat @n @m (abs a)

110+ signum (Nat a) = nat @n @m (signum a)

111+ fromInteger i = nat @n @m (fromInteger i)

99112

100113-- | Natural constructor function. Throws a runtime error if the 'Int'

101114-- value is greater than the corresponding @m@ or lower than @n@ in the @'Natural' n m@ type.

@@ -117,6 +130,11 @@ coerceNat = coerce

117130coerceNat2 :: ((Int, Int) -> Int -> Int) -> ((Natural a a', Natural b b') -> Natural c c' -> Natural d d')

118131coerceNat2 = coerce

119132

133+-- | Auxiliary function that promotes ternary (binary) 'Int' functions to 'Natural'

134+-- functions.

135+coerceNat3 :: (Int -> Int -> a) -> (Natural b b' -> Natural c c' -> a)

136+coerceNat3 = coerce

137+

120138instance (KnownNat n, KnownNat m) => Bounded (Natural n m) where

121139 minBound = Nat $ fromInteger (natVal (Proxy :: Proxy n))

122140 maxBound = Nat $ fromInteger (natVal (Proxy :: Proxy m))