headers
Adrian Neumann | 20 Dec 10:33
Favicon

type trickery

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.

Adrian

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Luke Palmer | 20 Dec 10:45

Re: type trickery

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
(Continue reading)

Permalink | Reply |
headers
oleg | 20 Dec 11:54

Re: type trickery


Adrian Neumann wrote:

> 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. 

You might like:

	Vectro: Haskell library for "statically typed linear algebra"
	http://ofb.net/~frederik/stla/

which marks each element of a vector space with its dimension. The
type system makes sure that you can only add vectors of the same
dimension (the type system does even more: it computes the dimension
of a result of multiplying a vector by a non-square matrix, for
example).

> I think that would need an infinite number of different types,
You think correctly. Haskell already has the infinite number of different
types (e.g., the infinite number of function types).
Permalink | Reply |

Gmane