Hello, Hal Daume III <hdaume@ISI.EDU> writes about Z_n in Haskell:
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)))
[..]
oleg@pobox.com responds with | The Z_n problem doesn't seem to be different from the problem of | arrays or bitvectors of a statically-checkable size. | | [..] | | Both implementations work in any Haskell-98 system. Multi-parameter | classes, existential types or other extensions are not needed. Also someone advised to follow up the haskell-cafe list archive containing the proposal, probably, by Dylan Thurston (Spring 2001), to exploit existential types to express the constructs like Z/(n) - residue domain of integers modulo n. This whole subject interests me. After maybe a month, I am going to investigate it and answer what precisely is wrong about the approaches mentioned. My previous impressions are as follows * It is hard to believe that the thing can be done in Haskell without existential types (properly implemented). * Dependent types (Aldor, Cayenne) are the adequate instrument for the above task. * The proposal from haskell-cafe (year ago) does not look practicable. I tried certain simple example of using it to work with Z/(m), and it failed. But I hope, we will return to the subject after a month. ----------------- Serge Mechveliani mechvel@botik.ru