FiniteField.hs

{-# LANGUAGE DataKinds, KindSignatures #-}
module FiniteField where
import GHC.TypeLits

data FiniteField (p :: Nat) = MkFF Integer deriving (Eq)

characteristic :: KnownNat p => FiniteField p -> Integer
characteristic = natVal

mkFF :: KnownNat p => Integer -> FiniteField p
mkFF n = let r = MkFF (n `mod` characteristic r) in r

instance KnownNat p => Num (FiniteField p) where
  MkFF x + MkFF y = mkFF (x + y)
  MkFF x - MkFF y = mkFF (x - y)
  negate (MkFF x) = mkFF (- x)
  MkFF x * MkFF y = mkFF (x * y)
  abs = undefined
  signum = undefined
  fromInteger = mkFF

instance KnownNat p => Fractional (FiniteField p) where
  recip a@(MkFF x) | x == 0 = error "divide by zero"
                   | otherwise = let p = characteristic a
                                 in mkFF (x^(p-2))
  fromRational = undefined

instance Show (FiniteField p) where
  show (MkFF n) = show n

Main.hs

{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
import FiniteField
import Data.Reflection
import System.Environment
import Data.Proxy

asFiniteField :: Proxy p -> FiniteField p -> FiniteField p
asFiniteField _ = id

someCalculation :: KnownNat p => Proxy p -> IO ()
someCalculation proxy = print (asFiniteField proxy $ 3 / 7)

isPrime :: Integer -> Bool
isPrime n = and [n `mod` m /= 0 | m <- [2..n-1]]

main :: IO ()
main = do args <- getArgs
          p <- case args of
            a:_ -> readIO a
            _ -> return 11
          if isPrime p
            then putStrLn (show p ++ " is a prime.")
            else putStrLn (show p ++ " is not a prime.")
          reifyNat p someCalculation