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