Defining an algebra module using a constructive algebra package

Question

The constructive algebra package allows you to define instances of algebraic modules (for example, vector spaces, but using a ring in which a field is required)

This is my attempt to define a module:

{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-} module A where import Algebra.Structures.Module import Algebra.Structures.CommutativeRing import Algebra.Structures.Group newtype A = A [(Integer,String)] instance Group A where (A a) <+> (A b) = A $ a ++ b zero = A [] neg (A a) = A $ [((-k),c) | (k,c) <- a] instance Module Integer A where r *> (A as) = A [(r <*> k,c) | (k,c) <- as] 

Failure:

 A.hs:15:10: Overlapping instances for Group A arising from the superclasses of an instance declaration Matching instances: instance Ring a => Group a -- Defined in Algebra.Structures.Group instance Group A -- Defined at A.hs:9:10-16 In the instance declaration for `Module Integer A' A.hs:15:10: No instance for (Ring A) arising from the superclasses of an instance declaration Possible fix: add an instance declaration for (Ring A) In the instance declaration for `Module Integer A' Failed, modules loaded: none. 

If I comment on an instance of Group , then:

 A.hs:16:10: No instance for (Ring A) arising from the superclasses of an instance declaration Possible fix: add an instance declaration for (Ring A) In the instance declaration for `Module Integer A' Failed, modules loaded: none. 

I read this as requiring an instance of Ring A have Module Integer A , which does not make sense and is not required in the class definition:

 class (CommutativeRing r, AbelianGroup m) => Module rm where -- | Scalar multiplication. (*>) :: r -> m -> m 

Could you explain this?

Answer 1

The package contains

 instance Ring a => Group a where ... 

The instance head a corresponds to each type expression, so any instance with any expression of another type will overlap. This overlap causes an error if such an instance is actually used somewhere. In your module you are using an instance in

 instance Module Integer A where r *> (A as) = A [(r <*> k,c) | (k,c) <- as] 

The Module class has an AbelianGroup constraint for the m parameter. This implies a limitation of the Group . Therefore, for this instance, you must verify the instance of Group a . The compiler finds two matching instances.

This is the first bug recorded.

In the following case, the compiler tries to find an instance of AbelianGroup for a . The only instance the compiler knows about at this point is

 instance (Group a, Ring a) => AbelianGroup a 

so he tries to find instance Ring A where ... but of course he is not.

Instead of commenting on instance Group A where ... you should add

 instance AbelianGroup a 

(even if it is a lie, we just want to compile it at the moment), and also add OverlappingInstances to the {-# LANGUAGE #-} pragma directory.

With OverlappingInstances , the most appropriate instance of the match is selected, so it does what you want here.

¹ By the way, your a not an instance of AbelianGroup and rightfully cannot be, if the order does not matter in the list [(Integer,String)] .

Answer 2

This type checks without unnecessary language extensions.

 {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-} module A where import Algebra.Structures.Module import Algebra.Structures.CommutativeRing import Algebra.Structures.Group newtype A = A [(Integer,String)] instance Ring A where A xs <+> A ys = A (xs ++ ys) neg (A a) = A $ [((-k),c) | (k,c) <- a] A x <*> A y = A [b | a <- x, b <- y ] one = A [] zero = A [] instance Module Integer A where r *> (A as) = A [(r <*> k,c) | (k,c) <- as] 

It is a bit confusing that <+> <*> and neg defined independently in Ring and Group ; they are completely separate characters, but then they are combined into a common instance that makes all Rings Groups , so if Ring defined, Group should not be defined, as it was already said. I'm not sure if this is imposed on the author by how the class class system works. Module requires Ring or rather CommutativeRing . CommutativeRing simply renamed Ring ; nothing further needs to be determined. It is assumed that you transfer what is in Haskell to an uncontrolled statement about commutativity. Therefore, you must “prove the laws of CommutativeRing ” so to speak, outside the module before creating an instance of the Module . Note, however, that these laws are expressed in quickcheck sentences, so you should run quickcheck on propMulComm and propCommutativeRing specialized for this type.

I don’t know what to do with one and zero, but you can get past the order point using a suitable structure, perhaps:

  import qualified Data.Set as S newtype B = B {getBs :: S.Set (Integer,String) } 

But with newtyped, you can also, for example, redefine Eq to A in order to understand this. In fact, you need to run quickcheck suggestions.

---

Edit: here is the version with additional materials needed for QuickCheck http://hpaste.org/68351 along with "Failure" and "OK" quickcheck-statements for various equalizer instances. This package looks pretty reasonable to me; I think you should redefine the module if you do not want to work with Ring and CommutativeRing, because it says that it "considers [s] only the commutative case, instead, you can implement left and right modules". Otherwise, you will not be able to use quickcheck, which, of course, is the main point of the package, now that I see what and what makes it incredibly easy to do. Since this A is exactly what he is trying to rule out using the all-pervasive use of quickcheck, which would certainly be very difficult to fool in this case.