git.iko.soy/Idris-dev
on master help sign in
Split off VectorSpace, Lattice from Algebra module
e7d5ef1BlackBrane
idris.cabal+1
compare with master
unifiedsplit
@@ -114,6 +114,7 @@ Extra-source-files:
114 libs/contrib/Classes/*.idr
114 libs/contrib/Classes/*.idr
115 libs/contrib/Control/*.idr
115 libs/contrib/Control/*.idr
116 libs/contrib/Control/Isomorphism/*.idr
116 libs/contrib/Control/Isomorphism/*.idr
117+ libs/contrib/Control/Algebra/*.idr
117 libs/contrib/Data/*.idr
118 libs/contrib/Data/*.idr
118 libs/contrib/Decidable/*.idr
119 libs/contrib/Decidable/*.idr
119 libs/contrib/Network/*.idr
120 libs/contrib/Network/*.idr
libs/contrib/Classes/Verified.idr+13−10
@@ -1,6 +1,8 @@
1module Classes.Verified
1module Classes.Verified
2
2
3import Control.Algebra
3import Control.Algebra
4+import Control.Algebra.Lattice
5+import Control.Algebra.VectorSpace
4
6
5-- Due to these being basically unused and difficult to implement,
7-- Due to these being basically unused and difficult to implement,
6-- they're in contrib for a bit. Once a design is found that lets them
8-- they're in contrib for a bit. Once a design is found that lets them
@@ -78,6 +80,11 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
78 total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
80 total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
79 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
81 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
80
82
83+class (VerifiedRing a, Field a) => VerifiedField a where
84+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
85+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
86+
87+
81class JoinSemilattice a => VerifiedJoinSemilattice a where
88class JoinSemilattice a => VerifiedJoinSemilattice a where
82 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
89 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
83 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
90 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
@@ -100,15 +107,11 @@ class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice
100
107
101class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
108class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
102
109
103−class (VerifiedRing a, Field a) => VerifiedField a where
104− total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
105− total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
106−
107−-- class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
108−-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
109−-- total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v
110−-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
111−-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
112
110
113−-- class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
111+class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
112+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
113+ total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v
114+ total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
115+ total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
114
116
117+class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
libs/contrib/Control/Algebra.idr+1−152
@@ -1,11 +1,8 @@
1module Control.Algebra
1module Control.Algebra
2
2
3−import Data.Heap
4−
5−-- XXX: change?
6infixl 6 <->
3infixl 6 <->
7infixl 6 <.>
4infixl 6 <.>
8−infixl 5 <#>
5+
9
6
10||| Sets equipped with a single binary operation that is associative, along with
7||| Sets equipped with a single binary operation that is associative, along with
11||| a neutral element for that binary operation and inverses for all elements.
8||| a neutral element for that binary operation and inverses for all elements.
@@ -40,7 +37,6 @@ class Monoid a => Group a where
40||| forall a, inverse a <+> a == neutral
37||| forall a, inverse a <+> a == neutral
41class Group a => AbelianGroup a where { }
38class Group a => AbelianGroup a where { }
42
39
43−
44||| Sets equipped with two binary operations, one associative and commutative
40||| Sets equipped with two binary operations, one associative and commutative
45||| supplied with a neutral element, and the other associative, with
41||| supplied with a neutral element, and the other associative, with
46||| distributivity laws relating the two operations. Must satisfy the following
42||| distributivity laws relating the two operations. Must satisfy the following
@@ -91,133 +87,6 @@ class AbelianGroup a => Ring a where
91class Ring a => RingWithUnity a where
87class Ring a => RingWithUnity a where
92 unity : a
88 unity : a
93
89
94−
95−||| Sets equipped with a binary operation that is commutative, associative and
96−||| idempotent. Must satisfy the following laws:
97−|||
98−||| + Associativity of join:
99−||| forall a b c, join a (join b c) == join (join a b) c
100−||| + Commutativity of join:
101−||| forall a b, join a b == join b a
102−||| + Idempotency of join:
103−||| forall a, join a a == a
104−|||
105−||| Join semilattices capture the notion of sets with a "least upper bound".
106−class JoinSemilattice a where
107− join : a -> a -> a
108−
109−instance JoinSemilattice Nat where
110− join = maximum
111−
112−instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
113− join = merge
114−
115−||| Sets equipped with a binary operation that is commutative, associative and
116−||| idempotent. Must satisfy the following laws:
117−|||
118−||| + Associativity of meet:
119−||| forall a b c, meet a (meet b c) == meet (meet a b) c
120−||| + Commutativity of meet:
121−||| forall a b, meet a b == meet b a
122−||| + Idempotency of meet:
123−||| forall a, meet a a == a
124−|||
125−||| Meet semilattices capture the notion of sets with a "greatest lower bound".
126−class MeetSemilattice a where
127− meet : a -> a -> a
128−
129−instance MeetSemilattice Nat where
130− meet = minimum
131−
132−
133−||| Sets equipped with a binary operation that is commutative, associative and
134−||| idempotent and supplied with a unitary element. Must satisfy the following
135−||| laws:
136−|||
137−||| + Associativity of join:
138−||| forall a b c, join a (join b c) == join (join a b) c
139−||| + Commutativity of join:
140−||| forall a b, join a b == join b a
141−||| + Idempotency of join:
142−||| forall a, join a a == a
143−||| + Bottom (Unitary Element):
144−||| forall a, join a bottom == a
145−|||
146−||| Join semilattices capture the notion of sets with a "least upper bound"
147−||| equipped with a "bottom" element.
148−class JoinSemilattice a => BoundedJoinSemilattice a where
149− bottom : a
150−
151−
152−instance BoundedJoinSemilattice Nat where
153− bottom = Z
154−
155−
156−||| Sets equipped with a binary operation that is commutative, associative and
157−||| idempotent and supplied with a unitary element. Must satisfy the following
158−||| laws:
159−|||
160−||| + Associativity of meet:
161−||| forall a b c, meet a (meet b c) == meet (meet a b) c
162−||| + Commutativity of meet:
163−||| forall a b, meet a b == meet b a
164−||| + Idempotency of meet:
165−||| forall a, meet a a == a
166−||| + Top (Unitary Element):
167−||| forall a, meet a top == a
168−|||
169−||| Meet semilattices capture the notion of sets with a "greatest lower bound"
170−||| equipped with a "top" element.
171−class MeetSemilattice a => BoundedMeetSemilattice a where
172− top : a
173−
174−
175−
176−||| Sets equipped with two binary operations that are both commutative,
177−||| associative and idempotent, along with absorbtion laws for relating the two
178−||| binary operations. Must satisfy the following:
179−|||
180−||| + Associativity of meet and join:
181−||| forall a b c, meet a (meet b c) == meet (meet a b) c
182−||| forall a b c, join a (join b c) == join (join a b) c
183−||| + Commutativity of meet and join:
184−||| forall a b, meet a b == meet b a
185−||| forall a b, join a b == join b a
186−||| + Idempotency of meet and join:
187−||| forall a, meet a a == a
188−||| forall a, join a a == a
189−||| + Absorbtion laws for meet and join:
190−||| forall a b, meet a (join a b) == a
191−||| forall a b, join a (meet a b) == a
192−class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
193−
194−
195−instance Lattice Nat where { }
196−
197−||| Sets equipped with two binary operations that are both commutative,
198−||| associative and idempotent and supplied with neutral elements, along with
199−||| absorbtion laws for relating the two binary operations. Must satisfy the
200−||| following:
201−|||
202−||| + Associativity of meet and join:
203−||| forall a b c, meet a (meet b c) == meet (meet a b) c
204−||| forall a b c, join a (join b c) == join (join a b) c
205−||| + Commutativity of meet and join:
206−||| forall a b, meet a b == meet b a
207−||| forall a b, join a b == join b a
208−||| + Idempotency of meet and join:
209−||| forall a, meet a a == a
210−||| forall a, join a a == a
211−||| + Absorbtion laws for meet and join:
212−||| forall a b, meet a (join a b) == a
213−||| forall a b, join a (meet a b) == a
214−||| + Neutral for meet and join:
215−||| forall a, meet a top == top
216−||| forall a, join a bottom == bottom
217−class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
218−
219−
220−-- Fields.
221||| Sets equipped with two binary operations, both associative and commutative
90||| Sets equipped with two binary operations, both associative and commutative
222||| supplied with a neutral element, with
91||| supplied with a neutral element, with
223||| distributivity laws relating the two operations. Must satisfy the following
92||| distributivity laws relating the two operations. Must satisfy the following
@@ -248,26 +117,6 @@ class RingWithUnity a => Field a where
248 inverseM : a -> a
117 inverseM : a -> a
249
118
250
119
251−||| A module over a ring is an additive abelian group of 'vectors' endowed with a
252−||| scale operation multiplying vectors by ring elements, and distributivity laws
253−||| relating the scale operation to both ring addition and module addition.
254−||| Must satisfy the following laws:
255−|||
256−||| + Compatibility of scalar multiplication with ring multiplication:
257−||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
258−||| + Ring unity is the identity element of scalar multiplication:
259−||| forall v, unity <#> v = v
260−||| + Distributivity of `<#>` and `<+>`:
261−||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
262−||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
263−class (RingWithUnity a, AbelianGroup b) => Module a b where
264− (<#>) : a -> b -> b
265−
266−
267−||| A vector space is a module over a ring that is also a field
268−class (Field a, Module a b) => VectorSpace a b where {}
269−
270−
271-- XXX todo:
120-- XXX todo:
272-- Structures where "abs" make sense.
121-- Structures where "abs" make sense.
273-- Euclidean domains, etc.
122-- Euclidean domains, etc.
libs/contrib/Control/Algebra/Lattice.idrnew file+123
@@ -0,0 +1,123 @@
1+module Control.Algebra.Lattice
2+
3+import Control.Algebra
4+import Data.Heap
5+
6+
7+||| Sets equipped with a binary operation that is commutative, associative and
8+||| idempotent. Must satisfy the following laws:
9+|||
10+||| + Associativity of join:
11+||| forall a b c, join a (join b c) == join (join a b) c
12+||| + Commutativity of join:
13+||| forall a b, join a b == join b a
14+||| + Idempotency of join:
15+||| forall a, join a a == a
16+|||
17+||| Join semilattices capture the notion of sets with a "least upper bound".
18+class JoinSemilattice a where
19+ join : a -> a -> a
20+
21+instance JoinSemilattice Nat where
22+ join = maximum
23+
24+instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
25+ join = merge
26+
27+||| Sets equipped with a binary operation that is commutative, associative and
28+||| idempotent. Must satisfy the following laws:
29+|||
30+||| + Associativity of meet:
31+||| forall a b c, meet a (meet b c) == meet (meet a b) c
32+||| + Commutativity of meet:
33+||| forall a b, meet a b == meet b a
34+||| + Idempotency of meet:
35+||| forall a, meet a a == a
36+|||
37+||| Meet semilattices capture the notion of sets with a "greatest lower bound".
38+class MeetSemilattice a where
39+ meet : a -> a -> a
40+
41+instance MeetSemilattice Nat where
42+ meet = minimum
43+
44+||| Sets equipped with a binary operation that is commutative, associative and
45+||| idempotent and supplied with a unitary element. Must satisfy the following
46+||| laws:
47+|||
48+||| + Associativity of join:
49+||| forall a b c, join a (join b c) == join (join a b) c
50+||| + Commutativity of join:
51+||| forall a b, join a b == join b a
52+||| + Idempotency of join:
53+||| forall a, join a a == a
54+||| + Bottom (Unitary Element):
55+||| forall a, join a bottom == a
56+|||
57+||| Join semilattices capture the notion of sets with a "least upper bound"
58+||| equipped with a "bottom" element.
59+class JoinSemilattice a => BoundedJoinSemilattice a where
60+ bottom : a
61+
62+instance BoundedJoinSemilattice Nat where
63+ bottom = Z
64+
65+||| Sets equipped with a binary operation that is commutative, associative and
66+||| idempotent and supplied with a unitary element. Must satisfy the following
67+||| laws:
68+|||
69+||| + Associativity of meet:
70+||| forall a b c, meet a (meet b c) == meet (meet a b) c
71+||| + Commutativity of meet:
72+||| forall a b, meet a b == meet b a
73+||| + Idempotency of meet:
74+||| forall a, meet a a == a
75+||| + Top (Unitary Element):
76+||| forall a, meet a top == a
77+|||
78+||| Meet semilattices capture the notion of sets with a "greatest lower bound"
79+||| equipped with a "top" element.
80+class MeetSemilattice a => BoundedMeetSemilattice a where
81+ top : a
82+
83+||| Sets equipped with two binary operations that are both commutative,
84+||| associative and idempotent, along with absorbtion laws for relating the two
85+||| binary operations. Must satisfy the following:
86+|||
87+||| + Associativity of meet and join:
88+||| forall a b c, meet a (meet b c) == meet (meet a b) c
89+||| forall a b c, join a (join b c) == join (join a b) c
90+||| + Commutativity of meet and join:
91+||| forall a b, meet a b == meet b a
92+||| forall a b, join a b == join b a
93+||| + Idempotency of meet and join:
94+||| forall a, meet a a == a
95+||| forall a, join a a == a
96+||| + Absorbtion laws for meet and join:
97+||| forall a b, meet a (join a b) == a
98+||| forall a b, join a (meet a b) == a
99+class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
100+
101+instance Lattice Nat where { }
102+
103+||| Sets equipped with two binary operations that are both commutative,
104+||| associative and idempotent and supplied with neutral elements, along with
105+||| absorbtion laws for relating the two binary operations. Must satisfy the
106+||| following:
107+|||
108+||| + Associativity of meet and join:
109+||| forall a b c, meet a (meet b c) == meet (meet a b) c
110+||| forall a b c, join a (join b c) == join (join a b) c
111+||| + Commutativity of meet and join:
112+||| forall a b, meet a b == meet b a
113+||| forall a b, join a b == join b a
114+||| + Idempotency of meet and join:
115+||| forall a, meet a a == a
116+||| forall a, join a a == a
117+||| + Absorbtion laws for meet and join:
118+||| forall a b, meet a (join a b) == a
119+||| forall a b, join a (meet a b) == a
120+||| + Neutral for meet and join:
121+||| forall a, meet a top == top
122+||| forall a, join a bottom == bottom
123+class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
libs/contrib/Control/Algebra/VectorSpace.idrnew file+30
@@ -0,0 +1,30 @@
1+module Control.Algebra.VectorSpace
2+
3+import Control.Algebra
4+
5+infixl 5 <#>
6+infixr 2 <||>
7+
8+
9+||| A module over a ring is an additive abelian group of 'vectors' endowed with a
10+||| scale operation multiplying vectors by ring elements, and distributivity laws
11+||| relating the scale operation to both ring addition and module addition.
12+||| Must satisfy the following laws:
13+|||
14+||| + Compatibility of scalar multiplication with ring multiplication:
15+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
16+||| + Ring unity is the identity element of scalar multiplication:
17+||| forall v, unity <#> v = v
18+||| + Distributivity of `<#>` and `<+>`:
19+||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
20+||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
21+class (RingWithUnity a, AbelianGroup b) => Module a b where
22+ (<#>) : a -> b -> b
23+
24+||| A vector space is a module over a ring that is also a field
25+class (Field a, Module a b) => VectorSpace a b where {}
26+
27+||| An inner product space is a module – or vector space – over a ring, with a binary function
28+||| associating a ring value to each pair of vectors.
29+class Module a b => InnerProductSpace a b where
30+ (<||>) : b -> b -> a
libs/contrib/contrib.ipkg+1
@@ -2,6 +2,7 @@ package contrib
2
2
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
4modules = Control.Algebra,
4modules = Control.Algebra,
5+ Control.Algebra.Lattice, Control.Algebra.VectorSpace,
5 Control.Isomorphism.Primitives,
6 Control.Isomorphism.Primitives,
6 Control.WellFounded,
7 Control.WellFounded,
7 Classes.Verified,
8 Classes.Verified,