{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, TypeOperators,
FunctionalDependencies, FlexibleContexts, UndecidableInstances,
FlexibleInstances #-}
-- | Integers modulo n parametrised by the n. This also has type-level primality
-- testing used for instantiating integral domain and field type classes. The
-- primality testing is very slow, but it seem to be working fine for relatively
-- small numbers.
module Algebra.Zn (Zn(..)) where
import Data.TypeLevel hiding ((+),(-),(*),mod,Eq,(==))
import Control.Monad (liftM)
import Test.QuickCheck
import Algebra.Structures.Field
import Algebra.Z
-- | The phantom type n represents which modulo to work in.
newtype Zn n = Zn Integer
deriving (Eq,Ord)
instance Show (Zn n) where
show (Zn n) = show n
instance Nat n => Num (Zn n) where
Zn x + Zn y = Zn $ (x+y) `mod` toNum (undefined :: n)
Zn x * Zn y = Zn $ (x*y) `mod` toNum (undefined :: n)
abs (Zn x) = Zn $ abs x
signum (Zn x) = Zn $ signum x
negate (Zn x) = Zn $ negate x `mod` toNum (undefined :: n)
fromInteger x = Zn $ fromInteger $ x `mod` toNum (undefined :: n)
instance Nat n => Arbitrary (Zn n) where
arbitrary = liftM Zn (choose (0,toNum (undefined :: n) - 1))
instance Nat n => Ring (Zn n) where
(<+>) = (+)
zero = Zn 0
one = Zn 1
neg = negate
(<*>) = (*)
instance Nat n => CommutativeRing (Zn n) where
instance (Prime n True, Nat n) => IntegralDomain (Zn n) where
instance (Prime n True, Nat n) => Field (Zn n) where
inv (Zn x) | x == 1 = Zn 1
| p `mod` x == 0 = error "Can't find the inverse of zero!"
| otherwise = Zn $ x <^> (p-2) `mod` p
where p = toNum (undefined :: n)
-- Z6 is not an integral domain and the typechecker will spot it!
-- intDomZ6 = quickCheck (propIntegralDomain :: Z6 -> Z6 -> Z6 -> Property)
-- Tests:
type Z3 = Zn D3
test1 :: Z3
test1 = inv 2
type Z17 = Zn D17
test2 :: Z17
test2 = inv 13
-- Test that all elements of Z17 get correct inverses
test3 :: Prelude.Bool
test3 = all (==1) [ inv x * x | x <- xs ]
where xs :: [Z17] = map fromInteger [1..16]
-----------------------------------------------------------------------
-- Lots of crazy type-level stuff:
class (Nat x, Nat sqrt) => Sqrt x sqrt | x -> sqrt
instance (Nat x, Nat sqrt, Sqrt' x D1 GT sqrt) => Sqrt x sqrt
class Sqrt' x y r sqrt | x y r -> sqrt
instance Sub y D2 y' => Sqrt' x y LT y'
instance Pred y y' => Sqrt' x y EQ y'
instance (ExpBase y D2 square, Succ y y', Trich x square r,
Sqrt' x y' r sqrt) => Sqrt' x y GT sqrt
sqrt :: Sqrt x sqrt => x -> sqrt
sqrt = undefined
class (Nat x, Data.TypeLevel.Bool b) => Prime x b | x -> b
instance (Sqrt x y, Trich y D1 r, Prime' x y r b) => Prime x b
class Data.TypeLevel.Bool b => Prime' x y r b | x y r -> b
instance Prime' x D1 EQ True
instance (Pred y z, Trich z D1 r1, Mod x y rest, IsZero rest b1,
Not b1 b', Prime' x z r1 b2, And b' b2 b3) => Prime' x y GT b3
prime :: Prime x b => x -> b
prime = undefined
class IsZero x r | x -> r
instance IsZero D0 True
instance IsZero D1 False
instance IsZero D2 False
instance IsZero D3 False
instance IsZero D4 False
instance IsZero D5 False
instance IsZero D6 False
instance IsZero D7 False
instance IsZero D8 False
instance IsZero D9 False
instance Pos x => IsZero (x :* d) False