git.iko.soy/laop
on master help sign in
Small tweaks and fixes
dfbd1d5Armando Santos
app/Main.hs+3−3
compare with master
unifiedsplit
@@ -6,9 +6,9 @@
6
6
7module Main where
7module Main where
8
8
9−import Matrix.Type
9+import LAoP.Matrix.Type
10−import Utils
10+import LAoP.Utils
11−import Dist
11+import LAoP.Dist
12import GHC.TypeLits
12import GHC.TypeLits
13import Data.Coerce
13import Data.Coerce
14import GHC.Generics
14import GHC.Generics
src/LAoP/Dist.hs+3−3
@@ -1,6 +1,6 @@
1-----------------------------------------------------------------------------
1-----------------------------------------------------------------------------
2-- |
2-- |
3−-- Module : Dist
3+-- Module : LAoP.Dist
4-- Copyright : (c) Armando Santos 2019-2020
4-- Copyright : (c) Armando Santos 2019-2020
5-- Maintainer : armandoifsantos@gmail.com
5-- Maintainer : armandoifsantos@gmail.com
6-- Stability : experimental
6-- Stability : experimental
@@ -16,7 +16,7 @@
16--
16--
17-----------------------------------------------------------------------------
17-----------------------------------------------------------------------------
18
18
19−module Dist
19+module LAoP.Dist
20 ( -- | If the sum of the rows of a column matrix
20 ( -- | If the sum of the rows of a column matrix
21 -- is equal to 1 then this stochastic matrix
21 -- is equal to 1 then this stochastic matrix
22 -- can be seen as a probability distribution.
22 -- can be seen as a probability distribution.
@@ -66,4 +66,4 @@ module Dist
66 )
66 )
67where
67where
68
68
69−import Dist.Internal
69+import LAoP.Dist.Internal
src/LAoP/Dist/Internal.hs+3−3
@@ -7,7 +7,7 @@
7{-# LANGUAGE DataKinds #-}
7{-# LANGUAGE DataKinds #-}
8{-# LANGUAGE RankNTypes #-}
8{-# LANGUAGE RankNTypes #-}
9
9
10−module Dist.Internal
10+module LAoP.Dist.Internal
11 (
11 (
12 Dist(..),
12 Dist(..),
13 Prob,
13 Prob,
@@ -32,8 +32,8 @@ module Dist.Internal
32 )
32 )
33 where
33 where
34
34
35−import Matrix.Type
35+import LAoP.Matrix.Type
36−import Utils
36+import LAoP.Utils
37import GHC.TypeLits
37import GHC.TypeLits
38import Data.Proxy
38import Data.Proxy
39import Data.List (sortBy)
39import Data.List (sortBy)
src/LAoP/Matrix/Internal.hs+3−23
@@ -15,7 +15,7 @@
15
15
16-----------------------------------------------------------------------------
16-----------------------------------------------------------------------------
17-- |
17-- |
18−-- Module : Matrix.Internal
18+-- Module : LAoP.Matrix.Internal
19-- Copyright : (c) Armando Santos 2019-2020
19-- Copyright : (c) Armando Santos 2019-2020
20-- Maintainer : armandoifsantos@gmail.com
20-- Maintainer : armandoifsantos@gmail.com
21-- Stability : experimental
21-- Stability : experimental
@@ -34,7 +34,7 @@
34--
34--
35-----------------------------------------------------------------------------
35-----------------------------------------------------------------------------
36
36
37−module Matrix.Internal
37+module LAoP.Matrix.Internal
38 ( -- | This definition makes use of the fact that 'Void' is
38 ( -- | This definition makes use of the fact that 'Void' is
39 -- isomorphic to 0 and '()' to 1 and captures matrix
39 -- isomorphic to 0 and '()' to 1 and captures matrix
40 -- dimensions as stacks of 'Either's.
40 -- dimensions as stacks of 'Either's.
@@ -142,7 +142,7 @@ module Matrix.Internal
142 )
142 )
143 where
143 where
144
144
145−import Utils
145+import LAoP.Utils
146import Data.Bool
146import Data.Bool
147import Data.Kind
147import Data.Kind
148import Data.List
148import Data.List
@@ -155,26 +155,6 @@ import Control.DeepSeq
155import Control.Category
155import Control.Category
156import Prelude hiding ((.))
156import Prelude hiding ((.))
157
157
158−data Zero
159−data Succ n
160−
161−type family Add x y where
162− Add x Zero = x
163− Add x (Succ y) = Succ (Add x y)
164−
165−data Matrix' e cols rows where
166− Empty' :: Matrix' e Zero Zero
167− One' :: e -> Matrix' e (Succ Zero) (Succ Zero)
168− Junc' :: Matrix' e a rows -> Matrix' e b rows -> Matrix' e (Add a b) rows
169− Split' :: Matrix' e cols a -> Matrix' e cols b -> Matrix' e cols (Add a b)
170−
171−abideSJ' :: Matrix' e cols rows -> Matrix' e cols rows
172−abideSJ' (Split' (Junc' a b) (Junc' c d)) = Junc' (Split' (abideSJ' a) (abideSJ' c)) (Split' (abideSJ' b) (abideSJ' d)) -- Split-Junc abide law
173−abideSJ' Empty' = Empty'
174−abideSJ' (One' e) = One' e
175−abideSJ' (Junc' a b) = Junc' (abideSJ' a) (abideSJ' b)
176−abideSJ' (Split' a b) = Split' (abideSJ' a) (abideSJ' b)
177−
178-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
158-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
179data Matrix e cols rows where
159data Matrix e cols rows where
180 Empty :: Matrix e Void Void
160 Empty :: Matrix e Void Void
src/LAoP/Matrix/Nat.hs+3−3
@@ -15,7 +15,7 @@
15
15
16-----------------------------------------------------------------------------
16-----------------------------------------------------------------------------
17-- |
17-- |
18−-- Module : Matrix.Nat
18+-- Module : LAoP.Matrix.Nat
19-- Copyright : (c) Armando Santos 2019-2020
19-- Copyright : (c) Armando Santos 2019-2020
20-- Maintainer : armandoifsantos@gmail.com
20-- Maintainer : armandoifsantos@gmail.com
21-- Stability : experimental
21-- Stability : experimental
@@ -33,7 +33,7 @@
33--
33--
34-----------------------------------------------------------------------------
34-----------------------------------------------------------------------------
35
35
36−module Matrix.Nat
36+module LAoP.Matrix.Nat
37 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
37 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
38 --
38 --
39 -- LAoP generalises relations and functions treating them as
39 -- LAoP generalises relations and functions treating them as
@@ -142,7 +142,7 @@ import Data.Proxy
142import GHC.TypeLits
142import GHC.TypeLits
143import Control.DeepSeq
143import Control.DeepSeq
144import qualified Control.Category as C
144import qualified Control.Category as C
145−import qualified Matrix.Internal as I
145+import qualified LAoP.Matrix.Internal as I
146
146
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
src/LAoP/Matrix/Type.hs+3−3
@@ -15,7 +15,7 @@
15
15
16-----------------------------------------------------------------------------
16-----------------------------------------------------------------------------
17-- |
17-- |
18−-- Module : Matrix.Type
18+-- Module : LAoP.Matrix.Type
19-- Copyright : (c) Armando Santos 2019-2020
19-- Copyright : (c) Armando Santos 2019-2020
20-- Maintainer : armandoifsantos@gmail.com
20-- Maintainer : armandoifsantos@gmail.com
21-- Stability : experimental
21-- Stability : experimental
@@ -36,7 +36,7 @@
36--
36--
37-----------------------------------------------------------------------------
37-----------------------------------------------------------------------------
38
38
39−module Matrix.Type
39+module LAoP.Matrix.Type
40 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
40 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
41 --
41 --
42 -- LAoP generalises relations and functions treating them as
42 -- LAoP generalises relations and functions treating them as
@@ -161,7 +161,7 @@ import Data.Kind
161import GHC.TypeLits
161import GHC.TypeLits
162import Control.DeepSeq
162import Control.DeepSeq
163import qualified Control.Category as C
163import qualified Control.Category as C
164−import qualified Matrix.Internal as I
164+import qualified LAoP.Matrix.Internal as I
165
165
166newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
166newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
167 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
167 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
src/LAoP/Relation.hsnew file+91
@@ -0,0 +1,91 @@
1+-----------------------------------------------------------------------------
2+-- |
3+-- Module : LAoP.Relation
4+-- Copyright : (c) Armando Santos 2019-2020
5+-- Maintainer : armandoifsantos@gmail.com
6+-- Stability : experimental
7+--
8+-- The AoP discipline generalises functions to relations which are
9+-- Boolean matrices.
10+--
11+-- This module offers many of the combinators of the Algebra of
12+-- Programming discipline. It is still under construction and very
13+-- experimental.
14+--
15+-- This is an Internal module and it is no supposed to be imported.
16+--
17+-----------------------------------------------------------------------------
18+
19+module LAoP.Relation
20+ ( -- | This definition makes use of the fact that 'Void' is
21+ -- isomorphic to 0 and '()' to 1 and captures matrix
22+ -- dimensions as stacks of 'Either's.
23+ --
24+ -- There exists two type families that make it easier to write
25+ -- matrix dimensions: 'FromNat' and 'Count'. This approach
26+ -- leads to a very straightforward implementation
27+ -- of LAoP combinators.
28+
29+ -- * Relation data type
30+ Relation (..),
31+ Boolean,
32+
33+ -- * Primitives
34+ empty,
35+ one,
36+ junc,
37+ split,
38+
39+ -- * Auxiliary type families
40+ FromNat,
41+ Count,
42+ Normalize,
43+
44+ -- * Matrix construction and conversion
45+ FromLists,
46+ fromLists,
47+ toLists,
48+ toList,
49+ matrixBuilder,
50+ zeros,
51+ ones,
52+ bang,
53+
54+ -- * Relational operations
55+ conv,
56+ intersection,
57+ union,
58+ sse,
59+ ker,
60+ img,
61+
62+ -- * (Endo-)Relational properties
63+ reflexive,
64+ coreflexive,
65+ transitive,
66+ symmetric,
67+ antiSymmetric,
68+ irreflexive,
69+ connected,
70+ preorder,
71+ partialOrder,
72+ linearOrder,
73+ equivalence,
74+ partialEquivalence,
75+
76+ -- ** McCarthy's Conditional
77+ -- cond,
78+
79+ -- * Relational composition and lifting
80+ identity,
81+ comp,
82+ fromF,
83+ fromF',
84+
85+ -- * Matrix printing
86+ pretty,
87+ prettyPrint
88+ )
89+ where
90+
91+import LAoP.Relation.Internal
src/LAoP/Relation/Internal.hs+34−30
@@ -8,7 +8,7 @@
8
8
9-----------------------------------------------------------------------------
9-----------------------------------------------------------------------------
10-- |
10-- |
11−-- Module : Relation.Internal
11+-- Module : LAoP.Relation.Internal
12-- Copyright : (c) Armando Santos 2019-2020
12-- Copyright : (c) Armando Santos 2019-2020
13-- Maintainer : armandoifsantos@gmail.com
13-- Maintainer : armandoifsantos@gmail.com
14-- Stability : experimental
14-- Stability : experimental
@@ -24,7 +24,7 @@
24--
24--
25-----------------------------------------------------------------------------
25-----------------------------------------------------------------------------
26
26
27−module Relation.Internal
27+module LAoP.Relation.Internal
28 ( -- | This definition makes use of the fact that 'Void' is
28 ( -- | This definition makes use of the fact that 'Void' is
29 -- isomorphic to 0 and '()' to 1 and captures matrix
29 -- isomorphic to 0 and '()' to 1 and captures matrix
30 -- dimensions as stacks of 'Either's.
30 -- dimensions as stacks of 'Either's.
@@ -45,12 +45,12 @@ module Relation.Internal
45 split,
45 split,
46
46
47 -- * Auxiliary type families
47 -- * Auxiliary type families
48− FromNat,
48+ I.FromNat,
49− Count,
49+ I.Count,
50− Normalize,
50+ I.Normalize,
51
51
52 -- * Matrix construction and conversion
52 -- * Matrix construction and conversion
53− FromLists,
53+ I.FromLists,
54 fromLists,
54 fromLists,
55 toLists,
55 toLists,
56 toList,
56 toList,
@@ -97,11 +97,12 @@ module Relation.Internal
97 where
97 where
98
98
99import Data.Void
99import Data.Void
100−import qualified Matrix.Internal as I
100+import qualified LAoP.Matrix.Internal as I
101−import Utils
101+import LAoP.Utils
102import Control.DeepSeq
102import Control.DeepSeq
103import qualified Control.Category as C
103import qualified Control.Category as C
104import Data.Coerce
104import Data.Coerce
105+import Data.Bool
105import GHC.TypeLits
106import GHC.TypeLits
106
107
107-- | Boolean type synonym for working with boolean matrices
108-- | Boolean type synonym for working with boolean matrices
@@ -123,11 +124,14 @@ instance C.Category Relation where
123 (.) = comp
124 (.) = comp
124
125
125instance Num (Relation a b) where
126instance Num (Relation a b) where
126− (R a) + (R b) = R (I.orM a b) --^ Matrix addition becomes Boolean matrix disjunction
127+ -- | Matrix addition becomes Boolean matrix disjunction
128+ (R a) + (R b) = R (I.orM a b)
127
129
128− (R a) - (R b) = R (I.subM a b) --^ Matrix subtraction becomes Relational subtraction
130+ -- | Matrix subtraction becomes Relational subtraction
131+ (R a) - (R b) = R (I.subM a b)
129
132
130− (R a) * (R b) = R (I.andM a b) --^ Matrix multiplication becomes Boolean matrix conjunction
133+ -- | Matrix multiplication becomes Boolean matrix conjunction
134+ (R a) * (R b) = R (I.andM a b)
131
135
132-- Type alias
136-- Type alias
133type Zero = Void
137type Zero = Void
@@ -181,8 +185,8 @@ fromLists = R . I.fromLists
181-- | Matrix builder function. Constructs a matrix provided with
185-- | Matrix builder function. Constructs a matrix provided with
182-- a construction function.
186-- a construction function.
183matrixBuilder ::
187matrixBuilder ::
184− (I.FromLists e (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
188+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
185− ((Int, Int) -> e) ->
189+ ((Int, Int) -> Boolean) ->
186 Relation a b
190 Relation a b
187matrixBuilder = R . I.matrixBuilder
191matrixBuilder = R . I.matrixBuilder
188
192
@@ -221,12 +225,12 @@ fromF' f = R (I.fromFRel' f)
221-- Conversion
225-- Conversion
222
226
223-- | Converts a matrix to a list of lists of elements.
227-- | Converts a matrix to a list of lists of elements.
224−toLists :: Relation a b -> [[e]]
228+toLists :: Relation a b -> [[Boolean]]
225−toLists (R m) = R $ I.toLists m
229+toLists (R m) = I.toLists m
226
230
227-- | Converts a matrix to a list of elements.
231-- | Converts a matrix to a list of elements.
228−toList :: Relation a b -> [e]
232+toList :: Relation a b -> [Boolean]
229−toList (R m) = R $ I.toList m
233+toList (R m) = I.toList m
230
234
231-- Zeros Matrix
235-- Zeros Matrix
232
236
@@ -318,47 +322,47 @@ entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize
318entire = reflexive . ker
322entire = reflexive . ker
319
323
320-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
324-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
321−surjective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
325+surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
322surjective = reflexive . img
326surjective = reflexive . img
323
327
324−-- | A 'Relation' @r@ is transitive iff @r . r `'sse'` r@
328+-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
325−transitive :: Relation a b -> Bool
329+transitive :: Relation a a -> Bool
326−transitive r = r . r `sse` r
330+transitive r = (r `comp` r) `sse` r
327
331
328-- | A 'Relation' @r@ is symmetric iff @r == r@
332-- | A 'Relation' @r@ is symmetric iff @r == r@
329−symmetric :: Relation a b -> Bool
333+symmetric :: Relation a a -> Bool
330symmetric r = r == r
334symmetric r = r == r
331
335
332-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
336-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
333−antiSymmetric :: Relation a b -> Bool
337+antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
334antiSymmetric r = (r `intersection` conv r) `sse` identity
338antiSymmetric r = (r `intersection` conv r) `sse` identity
335
339
336-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
340-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
337−irreflexive :: Relation a b -> Bool
341+irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
338irreflexive r = (r `intersection` identity) == zeros
342irreflexive r = (r `intersection` identity) == zeros
339
343
340-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
344-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
341−connected :: () => Relation a b -> Bool
345+connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
342connected r = (r `union` conv r) == ones
346connected r = (r `union` conv r) == ones
343
347
344-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
348-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
345−preorder :: () => Relation a b -> Bool
349+preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
346preorder r = reflexive r && transitive r
350preorder r = reflexive r && transitive r
347
351
348-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
352-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
349−partialOrder :: () => Relation a b -> Bool
353+partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
350partialOrder r = antiSymmetric r && preorder r
354partialOrder r = antiSymmetric r && preorder r
351
355
352-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
356-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
353−linearOrder :: () => Relation a b -> Bool
357+linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
354linearOrder r = connected r && partialOrder r
358linearOrder r = connected r && partialOrder r
355
359
356-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
360-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
357−equivalence :: () => Relation a b -> Bool
361+equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
358equivalence r = symmetric r && preorder r
362equivalence r = symmetric r && preorder r
359
363
360-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
364-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
361−partialEquivalence :: () => Relation a b -> Bool
365+partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
362partialEquivalence r = partialOrder r && equivalence r
366partialEquivalence r = partialOrder r && equivalence r
363
367
364-- Relation pretty print
368-- Relation pretty print
src/LAoP/Utils.hs+3−3
@@ -1,6 +1,6 @@
1-----------------------------------------------------------------------------
1-----------------------------------------------------------------------------
2-- |
2-- |
3−-- Module : Utils
3+-- Module : LAoP.Utils
4-- Copyright : (c) Armando Santos 2019-2020
4-- Copyright : (c) Armando Santos 2019-2020
5-- Maintainer : armandoifsantos@gmail.com
5-- Maintainer : armandoifsantos@gmail.com
6-- Stability : experimental
6-- Stability : experimental
@@ -15,7 +15,7 @@
15--
15--
16-----------------------------------------------------------------------------
16-----------------------------------------------------------------------------
17
17
18−module Utils
18+module LAoP.Utils
19 ( -- | Utility module that provides the 'Natural' data type.
19 ( -- | Utility module that provides the 'Natural' data type.
20 -- The semantic associated with this data type is that
20 -- The semantic associated with this data type is that
21 -- it's meant to be a restricted 'Int' value. For example
21 -- it's meant to be a restricted 'Int' value. For example
@@ -97,4 +97,4 @@ module Utils
97 )
97 )
98where
98where
99
99
100−import Utils.Internal
100+import LAoP.Utils.Internal
src/LAoP/Utils/Internal.hs+1−1
@@ -5,7 +5,7 @@
5{-# LANGUAGE KindSignatures #-}
5{-# LANGUAGE KindSignatures #-}
6{-# LANGUAGE ScopedTypeVariables #-}
6{-# LANGUAGE ScopedTypeVariables #-}
7
7
8−module Utils.Internal
8+module LAoP.Utils.Internal
9 ( -- | This is an internal module and it is not meant to be imported.
9 ( -- | This is an internal module and it is not meant to be imported.
10 --
10 --
11 -- Utility module that provides the 'Natural' data type.
11 -- Utility module that provides the 'Natural' data type.