Modular arithmetic using poor man’s dependent types

In this post I will speak about how one can implement \mathbb{Z}_n (\mathbb{Z} / n \mathbb{Z} 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 \mathbb{Z}_n 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 \mathbb{Z}\rightarrow\mathbb{Z}_n 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

So \mathbb{Z}_6 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 \mathbb{Z}_6 and thus it has zero divisors. In fact \mathbb{Z}_n 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 \mathbb{Z}_n .

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

So if n is a prime number then \mathbb{Z}_n is an integral domain. Using this we can try to make ghc believe that \mathbb{Z}_6 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 \mathbb{Z}_p ) we have that x ^{p-1} \equiv 1 \  mod \  p . So by computing x ^{p-2} we find an element y such that xy = 1 in \mathbb{Z}_p .

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

*Algebra.Zn> 13 * 4 :: Z17

*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.


One Response to Modular arithmetic using poor man’s dependent types

  1. mjsottile says:

    Very interesting posts! Looking forward to more.

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: