Reply: Z_n in Haskell

[Serge D. Mechveliani]

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