Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Defining an algebra module using constructive-algebra package

The package constructive-algebra allows you to define instances of algebraic modules (like vectorial spaces but using a ring where a field was required)

This is my try at defining 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]

It fails by:

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 the Group instance out, 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 to have Module Integer A which doesn't make sense and is not required in the class definition:

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

Could you explain this?

like image 972
user21338 Avatar asked May 10 '12 15:05

user21338


2 Answers

The package contains an

instance Ring a => Group a where ...

The instance head a matches every type expression, so any instance with any other type expression will overlap. That overlap only causes an error if such an instance is actually used somewhere. In your module, you use the instance in

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

The Module class has an AbelianGroup constraint on the m parameter¹. That implies a Group constraint. So for this instance, the Group instance of A must be looked up. The compiler finds two matching instances.

That is the first reported error.

The next is because the compiler tries to find an AbelianGroup instance for A. The only instance the compiler knows about at that point is

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

so it tries to find the instance Ring A where ..., but of course there isn't one.

Instead of commenting out the instance Group A where ..., you should add an

instance AbelianGroup a

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

With OverlappingInstances, the most specific matching instance is chosen, so it does what you want here.

¹ By the way, your A isn't an instance of AbelianGroup and rightfully can't be unless order is irrelevant in the [(Integer,String)] list.

like image 54
Daniel Fischer Avatar answered Sep 19 '22 10:09

Daniel Fischer


This type checks without obnoxious 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 little confusing that <+> <*> and neg are defined independently in Ring and Group; they are completely separate symbols, but then they are brought together in the general instance that makes all Rings Groups, so if Ring is defined, Group mustn't be defined, since it's already spoken for. I'm not sure this is forced on the author by the way the type class system works. Module requires Ring or rather CommutativeRing. CommutativeRing is just basically renaming Ring; nothing further is to be defined. It is supposed to commit you to what is in Haskell an uncheckable assertion of commutativity. So you are supposed to "prove the CommutativeRing laws", so to speak, outside the module before making the Module instance. Note however that these laws are expressed in quickcheck propositions, so you are supposed to run quickcheck on propMulComm and propCommutativeRing specialized to this type.

Don't know what to do about one and zero, but you can get past the point about order by using a suitable structure, maybe:

 import qualified Data.Set as S

 newtype B = B {getBs :: S.Set (Integer,String) }

But having newtyped you can also, e.g., redefine Eq on A's to make sense of it, I suppose. In fact you have to to run the quickcheck propositions.


Edit: Here is a version with added material needed for QuickCheck http://hpaste.org/68351 together with "Failed" and "OK" quickcheck-statements for different Eq instances. This package is seeming pretty reasonable to me; I think you should redefine Module if you don't want the Ring and CommutativeRing business, since he says he "Consider[s] only the commutative case, it would be possible to implement left and right modules instead." Otherwise you won't be able to use quickcheck, which is clearly the principal point of the package, now that I see what's up, and which he has made it incredibly easy to do. As it is A is exactly the kind of thing he is trying to rule out with the all-pervasive use of quickcheck, which it would surely be very hard to trick in this sort of case.

like image 34
applicative Avatar answered Sep 19 '22 10:09

applicative