gistfile1.txt

From ce4b0728b1249163f667f295dbfa55795a3a59a2 Mon Sep 17 00:00:00 2001
From: Edward O'Callaghan <[email protected]>
Date: Fri, 17 Oct 2014 20:57:37 +1100
Subject: [PATCH] Fix incorrectly type-dependence in vectors of VectorSpace
 type-class
Organization: Altera Praxis Pty Ltd.
To: [email protected]

VectorSpace takes two types to construct, a Field and abelian Group
respecively. The second type field was incorrectly typed as the same
as the first.

Signed-off-by: Edward O'Callaghan <[email protected]>
---
 libs/prelude/Prelude/Algebra.idr | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/libs/prelude/Prelude/Algebra.idr b/libs/prelude/Prelude/Algebra.idr
index c73768e..14fe46e 100644
--- a/libs/prelude/Prelude/Algebra.idr
+++ b/libs/prelude/Prelude/Algebra.idr
@@ -6,6 +6,7 @@ import Builtins
 infixl 6 <->
 infixl 6 <+>
 infixl 6 <*>
+infixl 6 <.>
 
 %access public
 
@@ -298,24 +299,25 @@ class (VerifiedRing a, Field a) => VerifiedField a where
   total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
   total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
 
---   vector spaces.
+--   VectorSpaces.
 ||| A Vector Space over a Field can be considered as an additive Abeliean Group
 ||| of Vectors adjoined to the Field structure by distributivity laws relating
 ||| the two operations. Such that we satisfy the following laws:
 |||
-||| + Unity for `<*>`:
-|||     forall a,     a <*> unity     == a
-|||     forall a,     unity <*> a     == a
-||| + Distributivity of `<*>` and `<+>`:
-|||     forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)
-|||     forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)
-class (Field a, AbelianGroup a) => VectorSpace a a where {}
-
-class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where
-  total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l
-  total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r
-  total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)
-  total vectorspaceScalarIsDistributiveWRTFieldAddition  : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)
+||| + Unity for `<.>`:
+|||     forall a,     a <.> unity     == a
+|||     forall a,     unity <.> a     == a
+||| + Distributivity of `<.>` and `<+>`:
+|||     forall a x y, a <.> (x <+> y) == (a <.> x) <+> (a <.> y)
+|||     forall a b x, (a <+> b) <.> x == (a <.> x) <+> (b <.> x)
+class (Field a, AbelianGroup b) => VectorSpace a b where
+  (<.>) : a -> b -> b
+
+class (VerifiedField a, VerifiedAbelianGroup b, VectorSpace a b) => VerifiedVectorSpace a b where
+  total vectorspaceScalarUnityIsUnityL : (l : b) -> flip (<.>) l unity = l
+  total vectorspaceScalarUnityIsUnityR : (r : b) -> (<.>) unity r = r
+  total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : b) -> s <.> (x <+> y) = (s <.> x) <+> (s <.> y)
+  total vectorspaceScalarIsDistributiveWRTFieldAddition  : (s, t : a) -> (x : b) -> (s <+> t) <.> x = (s <.> x) <+> (t <.> x)
 
 
 -- XXX todo:
-- 
2.1.2