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 \forall x y(x*y=0 \rightarrow x = 0 \lor y = 0). 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 x \neq 0 and y \neq 0 such that x*y = 0 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 \mathbb{Z} 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 \mathbb{Z} is not a field (what is the inverse of 2?). The standard example of a field is instead \mathbb{Q}. With a suitable implementation of \mathbb{Q} 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 \mathbb{Z}[\sqrt{-5}] is a Prüfer domain.


5 Responses to Basic ring theory in Haskell

  1. dan says:

    Why did you choose to use Haskell and not some dependent-typed language?

    • mortberg says:

      It was mostly due to time limitations. I figured that it would be easier to do it in Haskell since formalizing all the proofs would be very time consuming and difficult. But I plan to formalize my Haskell implementation in some dependently typed language at some point in the future. 🙂

  2. danr says:

    I found your blog! How cute!

  3. C. McCann says:

    Have you looked at the “checkers” package?

    Admittedly, the name and short description are unenlightening, but it has QuickCheck properties for some simple algebraic stuff–might save you a bit of time?

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: