git.iko.soy/laop
on master help sign in
Small tweaks and fixes
commitdfbd1d538eeab4938e5270f7326b71c3405cba3d authorArmando Santos <armandoifsantos@gmail.com> dateSun 12 Jan 2020, 15:33 (7 years ago) parent2d10e70
10 files changed+147−72
compare with master
unifiedsplit
app/Main.hs+3−3 src/LAoP/Dist.hs+3−3 src/LAoP/Dist/Internal.hs+3−3 src/LAoP/Matrix/Internal.hs+3−23 src/LAoP/Matrix/Nat.hs+3−3 src/LAoP/Matrix/Type.hs+3−3 src/LAoP/Relation.hs+91 src/LAoP/Relation/Internal.hs+34−30 src/LAoP/Utils.hs+3−3 src/LAoP/Utils/Internal.hs+1−1
app/Main.hs+3−3
@@ -6,9 +6,9 @@
66
77module Main where
88
9−import Matrix.Type
10−import Utils
11−import Dist
9+import LAoP.Matrix.Type
10+import LAoP.Utils
11+import LAoP.Dist
1212import GHC.TypeLits
1313import Data.Coerce
1414import GHC.Generics
src/LAoP/Dist.hs+3−3
@@ -1,6 +1,6 @@
11-----------------------------------------------------------------------------
22-- |
3−-- Module : Dist
3+-- Module : LAoP.Dist
44-- Copyright : (c) Armando Santos 2019-2020
55-- Maintainer : armandoifsantos@gmail.com
66-- Stability : experimental
@@ -16,7 +16,7 @@
1616--
1717-----------------------------------------------------------------------------
1818
19−module Dist
19+module LAoP.Dist
2020 ( -- | If the sum of the rows of a column matrix
2121 -- is equal to 1 then this stochastic matrix
2222 -- can be seen as a probability distribution.
@@ -66,4 +66,4 @@ module Dist
6666 )
6767where
6868
69−import Dist.Internal
69+import LAoP.Dist.Internal
src/LAoP/Dist/Internal.hs+3−3
@@ -7,7 +7,7 @@
77{-# LANGUAGE DataKinds #-}
88{-# LANGUAGE RankNTypes #-}
99
10−module Dist.Internal
10+module LAoP.Dist.Internal
1111 (
1212 Dist(..),
1313 Prob,
@@ -32,8 +32,8 @@ module Dist.Internal
3232 )
3333 where
3434
35−import Matrix.Type
36−import Utils
35+import LAoP.Matrix.Type
36+import LAoP.Utils
3737import GHC.TypeLits
3838import Data.Proxy
3939import Data.List (sortBy)
src/LAoP/Matrix/Internal.hs+3−23
@@ -15,7 +15,7 @@
1515
1616-----------------------------------------------------------------------------
1717-- |
18−-- Module : Matrix.Internal
18+-- Module : LAoP.Matrix.Internal
1919-- Copyright : (c) Armando Santos 2019-2020
2020-- Maintainer : armandoifsantos@gmail.com
2121-- Stability : experimental
@@ -34,7 +34,7 @@
3434--
3535-----------------------------------------------------------------------------
3636
37−module Matrix.Internal
37+module LAoP.Matrix.Internal
3838 ( -- | This definition makes use of the fact that 'Void' is
3939 -- isomorphic to 0 and '()' to 1 and captures matrix
4040 -- dimensions as stacks of 'Either's.
@@ -142,7 +142,7 @@ module Matrix.Internal
142142 )
143143 where
144144
145−import Utils
145+import LAoP.Utils
146146import Data.Bool
147147import Data.Kind
148148import Data.List
@@ -155,26 +155,6 @@ import Control.DeepSeq
155155import Control.Category
156156import Prelude hiding ((.))
157157
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−
178158-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
179159data Matrix e cols rows where
180160 Empty :: Matrix e Void Void
src/LAoP/Matrix/Nat.hs+3−3
@@ -15,7 +15,7 @@
1515
1616-----------------------------------------------------------------------------
1717-- |
18−-- Module : Matrix.Nat
18+-- Module : LAoP.Matrix.Nat
1919-- Copyright : (c) Armando Santos 2019-2020
2020-- Maintainer : armandoifsantos@gmail.com
2121-- Stability : experimental
@@ -33,7 +33,7 @@
3333--
3434-----------------------------------------------------------------------------
3535
36−module Matrix.Nat
36+module LAoP.Matrix.Nat
3737 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
3838 --
3939 -- LAoP generalises relations and functions treating them as
@@ -142,7 +142,7 @@ import Data.Proxy
142142import GHC.TypeLits
143143import Control.DeepSeq
144144import qualified Control.Category as C
145−import qualified Matrix.Internal as I
145+import qualified LAoP.Matrix.Internal as I
146146
147147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148148 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 @@
1515
1616-----------------------------------------------------------------------------
1717-- |
18−-- Module : Matrix.Type
18+-- Module : LAoP.Matrix.Type
1919-- Copyright : (c) Armando Santos 2019-2020
2020-- Maintainer : armandoifsantos@gmail.com
2121-- Stability : experimental
@@ -36,7 +36,7 @@
3636--
3737-----------------------------------------------------------------------------
3838
39−module Matrix.Type
39+module LAoP.Matrix.Type
4040 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
4141 --
4242 -- LAoP generalises relations and functions treating them as
@@ -161,7 +161,7 @@ import Data.Kind
161161import GHC.TypeLits
162162import Control.DeepSeq
163163import qualified Control.Category as C
164−import qualified Matrix.Internal as I
164+import qualified LAoP.Matrix.Internal as I
165165
166166newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
167167 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 @@
88
99-----------------------------------------------------------------------------
1010-- |
11−-- Module : Relation.Internal
11+-- Module : LAoP.Relation.Internal
1212-- Copyright : (c) Armando Santos 2019-2020
1313-- Maintainer : armandoifsantos@gmail.com
1414-- Stability : experimental
@@ -24,7 +24,7 @@
2424--
2525-----------------------------------------------------------------------------
2626
27−module Relation.Internal
27+module LAoP.Relation.Internal
2828 ( -- | This definition makes use of the fact that 'Void' is
2929 -- isomorphic to 0 and '()' to 1 and captures matrix
3030 -- dimensions as stacks of 'Either's.
@@ -45,12 +45,12 @@ module Relation.Internal
4545 split,
4646
4747 -- * Auxiliary type families
48− FromNat,
49− Count,
50− Normalize,
48+ I.FromNat,
49+ I.Count,
50+ I.Normalize,
5151
5252 -- * Matrix construction and conversion
53− FromLists,
53+ I.FromLists,
5454 fromLists,
5555 toLists,
5656 toList,
@@ -97,11 +97,12 @@ module Relation.Internal
9797 where
9898
9999import Data.Void
100−import qualified Matrix.Internal as I
101−import Utils
100+import qualified LAoP.Matrix.Internal as I
101+import LAoP.Utils
102102import Control.DeepSeq
103103import qualified Control.Category as C
104104import Data.Coerce
105+import Data.Bool
105106import GHC.TypeLits
106107
107108-- | Boolean type synonym for working with boolean matrices
@@ -123,11 +124,14 @@ instance C.Category Relation where
123124 (.) = comp
124125
125126instance 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)
127129
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)
129132
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)
131135
132136-- Type alias
133137type Zero = Void
@@ -181,8 +185,8 @@ fromLists = R . I.fromLists
181185-- | Matrix builder function. Constructs a matrix provided with
182186-- a construction function.
183187matrixBuilder ::
184− (I.FromLists e (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
185− ((Int, Int) -> e) ->
188+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
189+ ((Int, Int) -> Boolean) ->
186190 Relation a b
187191matrixBuilder = R . I.matrixBuilder
188192
@@ -221,12 +225,12 @@ fromF' f = R (I.fromFRel' f)
221225-- Conversion
222226
223227-- | Converts a matrix to a list of lists of elements.
224−toLists :: Relation a b -> [[e]]
225−toLists (R m) = R $ I.toLists m
228+toLists :: Relation a b -> [[Boolean]]
229+toLists (R m) = I.toLists m
226230
227231-- | Converts a matrix to a list of elements.
228−toList :: Relation a b -> [e]
229−toList (R m) = R $ I.toList m
232+toList :: Relation a b -> [Boolean]
233+toList (R m) = I.toList m
230234
231235-- Zeros Matrix
232236
@@ -318,47 +322,47 @@ entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize
318322entire = reflexive . ker
319323
320324-- | 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
322326surjective = reflexive . img
323327
324−-- | A 'Relation' @r@ is transitive iff @r . r `'sse'` r@
325−transitive :: Relation a b -> Bool
326−transitive r = r . r `sse` r
328+-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
329+transitive :: Relation a a -> Bool
330+transitive r = (r `comp` r) `sse` r
327331
328332-- | A 'Relation' @r@ is symmetric iff @r == r@
329−symmetric :: Relation a b -> Bool
333+symmetric :: Relation a a -> Bool
330334symmetric r = r == r
331335
332336-- | 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
334338antiSymmetric r = (r `intersection` conv r) `sse` identity
335339
336340-- | 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
338342irreflexive r = (r `intersection` identity) == zeros
339343
340344-- | 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
342346connected r = (r `union` conv r) == ones
343347
344348-- | 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
346350preorder r = reflexive r && transitive r
347351
348352-- | 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
350354partialOrder r = antiSymmetric r && preorder r
351355
352356-- | 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
354358linearOrder r = connected r && partialOrder r
355359
356360-- | 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
358362equivalence r = symmetric r && preorder r
359363
360364-- | 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
362366partialEquivalence r = partialOrder r && equivalence r
363367
364368-- Relation pretty print
src/LAoP/Utils.hs+3−3
@@ -1,6 +1,6 @@
11-----------------------------------------------------------------------------
22-- |
3−-- Module : Utils
3+-- Module : LAoP.Utils
44-- Copyright : (c) Armando Santos 2019-2020
55-- Maintainer : armandoifsantos@gmail.com
66-- Stability : experimental
@@ -15,7 +15,7 @@
1515--
1616-----------------------------------------------------------------------------
1717
18−module Utils
18+module LAoP.Utils
1919 ( -- | Utility module that provides the 'Natural' data type.
2020 -- The semantic associated with this data type is that
2121 -- it's meant to be a restricted 'Int' value. For example
@@ -97,4 +97,4 @@ module Utils
9797 )
9898where
9999
100−import Utils.Internal
100+import LAoP.Utils.Internal
src/LAoP/Utils/Internal.hs+1−1
@@ -5,7 +5,7 @@
55{-# LANGUAGE KindSignatures #-}
66{-# LANGUAGE ScopedTypeVariables #-}
77
8−module Utils.Internal
8+module LAoP.Utils.Internal
99 ( -- | This is an internal module and it is not meant to be imported.
1010 --
1111 -- Utility module that provides the 'Natural' data type.