Reply: Z_n in Haskell
Serge D. Mechveliani
Mon, 1 Apr 2002 10:54:42 +0400
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
> 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"
> 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)))
email@example.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.