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