Basic ring theory in Haskell

Apparently this is the first post on this blog. In it I will speak a little about how to implement the basic algebraic structures of ring theory as Haskell type classes. This is the core of my constructive-algebra library, which I wrote as part of my master thesis. In the thesis I mainly looked at three different structures: Bézout domains, Prüfer domains and polynomial rings. I plan to write about these at some point in the future but now I will focus on the basics.

The natural place to start is of course with rings. A ring is a set together with two operators + (addition) and * (multiplication). There are also two special objects in the ring, one and zero. Every object should also have an additive inverse. This can be represented in Haskell by a type class:

class Ring a where
  (<+>) :: a -> a -> a
  (<*>) :: a -> a -> a
  neg   :: a -> a
  one   :: a
  zero  :: a

But now we run into some peculiarities. The operators and constants are not the only requirements for a ring… A ring also has to satisfy certain axioms. But how should we encode these? In a language with dependent types this would have been possible to do in a satisfactory way as part of the structure, but in Haskell we have to settle with something less fancy. I have chosen to use QuickCheck properties for representing the axioms that rings has to satisfy. For example: in a ring must the multiplication distribute over addition (both from left and right), this can be expressed as:

propLeftDist :: (Ring a, Eq a) => a -> a -> a -> Bool
propLeftDist a b c = a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

The next structure is commutative rings, that is rings in which the multiplication is commutative. This does not introduce any new elements to the structure, so this is just an empty type class:

class Ring a => CommutativeRing a

But now we have another axiom that should hold:

propMulComm :: (CommutativeRing a, Eq a) => a -> a -> Bool
propMulComm a b = a <*> b == b <*> a

The next structure we will look at is integral domains. An integral domain is a commutative ring with no zero-divisors. That is . This can be expressed in the same manner as for commutative rings. But here there is another peculiarity since it can be quite unlikely for QuickCheck to generate two random numbers and such that and thus will the implication almost always be true. So the property should be taken with a grain of salt. The classical example of an integral domain is which is represented by the Integer type in Haskell.

type Z = Integer

instance Ring Z where
  (<+>) = (+)
  (<*>) = (*)
  neg   = negate
  zero  = 0
  one   = 1

instance CommutativeRing Z

instance IntegralDomain Z

We can now test that Z satisfies all axioms for integral domains.

*Algebra.Z> quickCheck (propIntegralDomain :: Z -> Z -> Z -> Property)
+++ OK, passed 100 tests.

The final structure for today is fields, that is integral domains in which all elements (except zero) has a multiplicative inverse. This need some more structure, since now there has to be a function that given an element computes its multiplicative inverse.

class IntegralDomain a => Field a where
  inv :: a -> a

propMulInv :: (Field a, Eq a) => a -> Property
propMulInv a = a /= zero ==> inv a <*> a == one

Of course is not a field (what is the inverse of 2?). The standard example of a field is instead . With a suitable implementation of we can now do:

instance Field Q where
  inv x = 1/x

That’s all for this time. Nothing fancy so far, but this proved to be a good foundation to build more interesting things on. Having runnable axioms for the structures can seem a bit silly for the simple examples presented here but it was in fact quite useful when implementing more complex things, like for example the proof that is a Prüfer domain.