Constructing fields of fractions using Haskell

This time I will write about a way to construct fields from integral domains using Haskell. It will use the structures from my previous post. But first a comment on that post. When discussing integral domains I said that it was hard to test the property that there should be no zero divisors. A friend of mine asked me why I did not test the contrapositive instead. That is, I should use to convert into which should be easier to test…

Now let’s consider how to turn integral domains into fields. This construction is called field of fractions and is denoted by where A is an integral domain. It is a generalization of the construction of from . An element of is a pair with and . This pair should be interpreted as . This could be represented straight forwardly in Haskell as a pair. But I want to work with reduced expressions, that is I want the extra constraint that . To guarantee this I need to consider a more specialised structure than integral domains called GCD domains. This is a structure in which any pair of nonzero elements has a greatest common divisor. This is represented as:

class IntegralDomain a => GCDDomain a where
  gcd' :: a -> a -> (a,a,a)

Here gcd’ take nonzero and and compute such that , and . That is, it computes the greatest common divisor of and plus witnesses that it actually divides both and . This can be specified as:

propGCD :: (GCDDomain a, Eq a) => a -> a -> Property
propGCD a b = a /= zero && b /= zero ==> a == g <*> x && b == g <*> y
  where
  (g,x,y) = gcd' a b

Now we are ready to represent the field of fractions over a GCD domain:

newtype GCDDomain a => FieldOfFractions a = F (a,a)

Now can be embedded in by

toFieldOfFractions :: GCDDomain a => a -> FieldOfFractions a
toFieldOfFractions a = F (a,one)

Since we are working over a GCD domain we can compute reduced expressions:

reduce :: (GCDDomain a, Eq a) 
       => FieldOfFractions a -> FieldOfFractions a
reduce (F (a,b)) | b == zero = error "reduce: Division by 0"
                 | a == zero = F (zero,one)
                 | otherwise = F (x,y)
  where
  (g,x,y) = gcd' a b

Using this we can define a function from to A.

fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a
fromFieldOfFractions x 
  | b' == one = a'
  | otherwise = error "fromFieldOfFractions: Denominator is not 1"
    where F (a',b') = reduce x 

To test equality the underlying ring need to have decidable equality (i.e. it should be discrete). and are equal iff which give:

instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a) where
  (F (a,b)) == (F (c,d)) = a <*> d == b <*> c

We can also implement all the operations needed for showing that the constructed field of fractions is in fact a field.

instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a) where
  (F (a,b)) <+> (F (c,d)) = reduce (F (a <*> d <+> c <*> b,b <*> d))
  (F (a,b)) <*> (F (c,d)) = reduce (F (a <*> c,b <*> d))
  neg (F (a,b))           = reduce (F (neg a,b))
  one                     = toFieldOfFractions one
  zero                    = toFieldOfFractions zero

instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)
instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)

instance (GCDDomain a, Eq a) => Field (FieldOfFractions a) where
  inv (F (a,b)) | a == zero = error "inv: Can't invert 0"
                | b == zero = error "inv: Division by 0"
                | otherwise = reduce $ F (b,a)

Finally we can construct from by just writing:

type Q = FieldOfFractions Z

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

*Algebra.Q> 3*(1/2)^3 :: Q
3/8

Where the last computation is possible by adding suitable Num, Fractional and Show instances. I really like this way of constructing fields. For instance I used this to implement the field of rational functions using my implementation of polynomials.

Of course I don’t need the GCDDomain constraint for any function except fromFieldOfFractions, so it would be very easy to generalize this for any integral domain. But it proved useful when implementing a proof for constructing interesting Prüfer domains, so I added the constraint everywhere. It also look more appealing with reduced expressions and I have only had to consider and the field of rational functions so far.

Finally I would like to write a little about GCD domains. It is possible to prove that they are non-Noetherian analogues of unique factorization domains (UFDs), that is, one gets UFDs by taking GCD domains and adding the ascending chain condition on ideals. The reason for not having Noetheriannity is that it gives constructive versions of classical notions. So instead of UFDs we get GCD domains and instead of PIDs we get Bézout domains in constructive mathematics. The problem with Noetheriannity is quite intricate and I have not fully grasped it yet. As far as I know there is no consensus about what a constructive version should be. I plan to write more about this in some upcoming posts.

Modular arithmetic using poor man’s dependent types

In this post I will speak about how one can implement ( or the integers modulo n) using fake dependent types in Haskell. What I want to do is to represent the modulus that characterizes the ring we are working over at the type level. To do this I use the type-level library which contains an implementation of tons of type level numbers and operations on them. The type of can be represented using a phantom type which denote the modulus:

newtype Zn n = Zn Integer
  deriving (Eq,Ord)

It is easy to implement a Show instance:

instance Pos n => Show (Zn n) where
  show (Zn n) = show n

Here Pos denote positive natural numbers. The Num instance is a bit more interesting:

instance Pos n => Num (Zn n) where
  Zn x + Zn y   = Zn $ (x+y) `mod` toNum (undefined :: n)
  Zn x * Zn y   = Zn $ (x*y) `mod` toNum (undefined :: n)
  negate (Zn x) = Zn $ negate x `mod` toNum (undefined :: n)
  fromInteger x = Zn $ fromInteger $ x `mod` toNum (undefined :: n)

I have left abs and signum out since I don’t know what they mean in this setting (does anyone have an idea?). Anyway, toNum is a function that only depend on its type. What I mean is that toNum for D3 (digit 3) always return 3 regardless of input, so all computations are done modulo the number encoded in the type. fromInteger is quite interesting also, it is the canonical homomorphism or natural map which takes an element and send it to its congruence class modulo n.

In fact this fit very well in the algebraic hierarchy that I discussed in my previous post.

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

instance Pos n => CommutativeRing (Zn n) where

We can now check that we haven’t done anything stupid so far.

type Z6 = Zn D6

test = quickCheck (propCommutativeRing :: Z6 -> Z6 -> Z6 -> Property)

*Algebra.Zn> test
+++ OK, passed 100 tests.

*Algebra.Zn> 2 + 2 * 4 :: Z6
4

So is a commutative ring and the basic operations seem to be working fine. But what about making it an instance of integral domain? This should not be possible since 2*3=0 in and thus it has zero divisors. In fact is an integral domain only if n is prime, but how do we test this on the type level? There is no type level primality test in the library, so I decided to hack one up myself. The only problem was that I don’t really know functional dependencies that well, but I looked at the code in the library and read some tutorials and this is what I came up with:

class (Pos x, Pos sqrt) => Sqrt x sqrt | x -> sqrt
instance (Pos x, Pos sqrt, Sqrt' x D1 GT sqrt) => Sqrt x sqrt

class Sqrt' x y r sqrt | x y r -> sqrt
instance Sub y D2 y' => Sqrt' x y LT y'
instance Pred y y'   => Sqrt' x y EQ y'
instance (ExpBase y D2 square, Succ y y', Trich x square r, 
          Sqrt' x y' r sqrt) => Sqrt' x y GT sqrt

sqrt :: Sqrt x sqrt => x -> sqrt
sqrt = undefined

class (Pos x, Data.TypeLevel.Bool b) => Prime x b | x -> b
instance (Sqrt x y, Trich y D1 r, Prime' x y r b) => Prime x b

class Data.TypeLevel.Bool b => Prime' x y r b | x y r -> b
instance Prime' x D1 EQ True
instance (Pred y z, Trich z D1 r1, Mod x y rest, IsZero rest b1, 
          Not b1 b', Prime' x z r1 b2, And b' b2 b3) => Prime' x y GT b3

prime :: Prime x b => x -> b
prime = undefined

It looks like a lot of mumbo jumbo and maybe it is, but it seems to work. The main problem though is that it is horribly slow and that it believes that 1 is a prime number… If anyone know fundeps (or type families) and sees how this can be improved, please let me know. Anyway, now I can implement the integral domain instance for .

instance (Prime n True, Pos n) => IntegralDomain (Zn n) where

So if n is a prime number then is an integral domain. Using this we can try to make ghc believe that an integral domain:

*Algebra.Zn> quickCheck (propIntegralDomain :: Z6 -> Z6 -> Z6 -> Property)
Top level:
    Couldn't match expected type `True' against inferred type `False'
    ...

Woho, ghc can correct us automagically! What about giving a field instance? To do it we need to be able to compute the inverse of any nonzero element. Here Fermat’s little theorem comes in handy, it says that for any prime p and natural number x coprime to p (which in our case is any element of ) we have that . So by computing we find an element y such that xy = 1 in .

instance (Prime n True, Pos n) => Field (Zn n) where
  inv (Zn x) | x == 1         = Zn 1
             | p `mod` x == 0 = error "Can't invert zero!"
             | otherwise      = Zn $ x <^> (p-2) `mod` p
    where p = toNum (undefined :: n)

Now we can try this out on a prime number, for instance 17.

type Z17 = Zn D17

*Algebra.Zn> inv 13 :: Z17
4

*Algebra.Zn> 13 * 4 :: Z17
1

*Algebra.Zn> quickCheck (propField :: Z17 -> Z17 -> Z17 -> Property)
+++ OK, passed 100 tests.

Everything seem to be working fine, but sadly it is not useful for something “real” since the typechecking is so slow for primality testing. But I think it is quite cool that you can do these things in Haskell, but of course it would be even nicer to do it in a language with real dependent types.

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.