The main issue you have to work around is the fact that you shouldn't be allowed to add/multiply/etc. values of FiniteField
under different orders. The solution is pretty straightforward from a type-system perspective: give values of different orders different types.
newtype FieldElem (n :: Nat) = FieldElem Integer
Nat
is a kind (from the GHC.TypeLits module) whose inhabitants are type-level numerical literals like 1
, 2
, 3
, etc.
So now, you have different types:
FieldElem 7 -- the type of an element of a finite field of order 7
FieldElem 11 -- the type of an element of a finite field of order 11
So if you try to add two values of different types, you get a compile error.
> (x :: FieldElem 7) + (y :: FieldElem 11)
Error! You can only use + on two things of the same type!
> (x :: FieldElem 7) + (y :: FieldElem 7)
-- result: something of type FieldElem 7
Now you can implement the Num
instance:
instance Num (FieldElem n) where
(+) = ...
(*) = ...
One issue here is that (+)
needs to know what the order is, and the only information is in the type of FieldElem
. To go around this, we require n
to be an instance of the KnownNat
typeclass (also from GHC.TypeLits), which lets us get its integer value as a value at runtime:
natVal :: KnownNat n => Proxy n -> Integer
so,
> natVal (Proxy :: Proxy 10)
10
> natVal (Proxy :: Proxy 19)
19
And so our final design: (which requires ScopedTypeVariables
to let us use the n
type variable)
instance KnownNat n => Num (FieldElem n) where
FieldElem x + FieldElem y = FieldElem (mod (x + y) n)
where
n = natVal (Proxy :: Proxy n)
etc.!
You can bring in Integer
s into FieldElem
using a smart constructor:
mkFieldElem :: forall n. KnownNat n => Integer -> Maybe (FieldElem n)
mkFieldElem x | isPrime n = Just (FieldElem (mod x n))
| otherwise = Nothing
where
n = natVal (Proxy :: Proxy n)
The nice thing is that you get to use Haskell's type inference to specify the order you want:
> mkFieldElem 10 :: Maybe (FieldElem 23)
Just (FieldElem 10) -- :: Maybe (FieldElem 23)
Instead of manually passing it as a parameter! :)
By using smart constructors (and hiding the actual constructor) you can make sure that the user never has any values of type FieldElem 8
, for instance, so you don't have to worry about fields of bad orders being added together.
Note that, unfortunately, fromInteger :: KnownNat n => Integer -> FieldElem n
will necessarily be partial. It has to reject bad orders. But there are a large number of instances in base with partial implementations of fromInteger
anyway :| But, fromInteger
being in Num
is a bad idea anyways, and Num
is a bad typeclass, so it's Num
's fault :)
EDIT There's a potential way to make fromInteger
not partial/total: we could create a Prime
typeclass and have only instances where the Nat
parameter is prime:
class KnownNat n => Prime (n :: Nat)
Then you could make:
mkFieldElem :: Prime n => Integer -> FieldElem n
mkFieldElem x = FieldElem (mod x n)
where
n = natVal (Proxy :: Proxy n)
And now if you had:
instance Prime n => Num (FieldElem n) where
...
fromInteger = mkFieldElem
fromInteger
would be a total function, because the only instances would be for prime order fields!
However, in order for this to work, you need to get your instances of Prime
in a way that GHC can understand. In theory, this could be done using a GHC type checker extension --- you could write your own type checker extension so that n
is given a Prime
instance if it's prime at compile-time. However, this hasn't been done yet ... the next best thing you can do is offer run-time proofs of prime-ness:
witPrime :: forall n.KnownNat n => Proxy n -> Maybe (Dict (Prime n))
witPrime p | isPrime (natVal p) = Just (unsafeCoerce (Dict :: Dict (KnownNat n))
| otherwise = Nothing
This is using Dict
from the constraints library, which is one way of generating typeclass instances at runtime. If you ever pattern match on the Dict
constructor of a value of type Dict c
, the instance c
is "in scope" in that case statement.
In our case, then, we can do:
case witPrime (Proxy :: Proxy 11) of
Just Dict -> ... -- in this branch, `Prime 11` is an instance we can use
Nothing -> ... -- here, it isn't
Or we can run it in GHCi:
> let x = mkFieldElem 6 :: FieldElem 11
Error: No instance for (Prime 11)
> case witPrime (Proxy :: Proxy 11) of
Just Dict -> let x = mkFieldElem 6 :: FieldElem 11 -- okay, because of Dict constructor match
in print x
FieldElem 6 -- :: FieldElem 11