Z_n in Haskell

[Hal Daume III]

Suppose I want to define integers modulo n, I could do this something
like:

data Zn = Zn Integer Integer   -- modulus, number

instance Num Zn where
  (Zn m1 n1) + (Zn m2 n2)
    | m1 == m2 = Zn m1 (n1 + n2 `mod` m1)
    | otherwise= error "differing moduli"
  ...etc...

However, I'd really like it if, say, addition on Zn-s of different
"n" values were caught by the typechecker and disallowed.  One solution to
this problem would be to do something like:

class Modulus m where modulus :: T m -> Integer
data Zn m = Zn (T m) Integer

instance Modulus m => Num (Zn m) where
    (Zn m1 n1) + (Zn m2 n2) =
	(Zn m1 ((n1 + n2) `mod` (modulus m1)))

data T a = T

data Mod5
data Mod7

instance Modulus (Mod5) where modulus _ = 5
instance Modulus (Mod7) where modulus _ = 7

then we get:

Modulus> (Zn (T :: T Mod5) 3) + (Zn (T :: T Mod5) 4)
2

but it fails when the moduli are different:

Modulus> (Zn (T :: T Mod5) 3) + (Zn (T :: T Mod7) 4)

Ambiguous type variable(s) `a' in the constraint `Show a'
arising from use of `print' at <No locn>
In a 'do' expression pattern binding: print it

<interactive>:1:
    Couldn't match `Mod7' against `Mod5'
	Expected type: T Mod7
	Inferred type: T Mod5
    In an expression with a type signature: T :: T Mod7
    In the first argument of `Zn', namely `(T :: T Mod7)'

Unfortunately, this solution isn't very pretty.  We have to define a new
datatype for each modulus and make it an instance of Modulus.  Is there a
better way to do this?

 - Hal

--
Hal Daume III

 "Computer science is no more about computers    | hdaume@isi.edu
  than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume