[Haskell-cafe] type trickery

[Luke Palmer]

On Dec 20, 2007 9:34 AM, Adrian Neumann <aneumann at inf.fu-berlin.de> wrote:
> Hello haskell-cafe!
>
> After making "data Number = Zero | Succ Number" an instance of
> Integral, I wondered how I could do the same with galois fields. So
> starting with Z mod p, I figured I'd need something like this
>
> data GF = GF Integer Integer
>
> so that each element of the finite field would remember p. However I
> can't think of a way to use the typesystem to ensure that p is always
> the same. I think that would need an infinite number of different
> types, but the type hackers here probably know something better.

Yes, you can have some fun by taking your Number definition to the type level:

data Zero    -- phantom type, no implementation
data Succ a  -- same

class Runtimify a where
    runtimify :: a -> Integer

instance Runtimify Zero where
    runtimify _ = 0

instance (Runtimify a) => Runtimify (Succ a) where
    runtimify _ = 1 + runtimify (undefined :: a)

data GF p = GF Integer

instance (Runtimify p) => Num (GF p) where
    -- you fill in the rest :-)

Note that p is encoded in only a type variable, so you'll
have to use "runtimify" (sorry for the silly name) to get
it out.

Luke