Hal Daume III hdaume@ISI.EDU
Thu, 28 Mar 2002 13:27:42 -0800 (PST)

```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

```