[Haskell-cafe] type trickery
Luke Palmer
lrpalmer at gmail.com
Thu Dec 20 04:45:43 EST 2007
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
More information about the Haskell-Cafe
mailing list