type parametrized modulo arithmetic

modulo.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Main where

import Data.Proxy
import GHC.TypeLits


class Periodic (a :: *) where
  period :: a -> Integer

newtype IntegerModulo (m :: Nat) = IntegerModulo { unIM :: Integer }

instance (KnownNat m) => Show (IntegerModulo m) where
  show a@(IntegerModulo n) = show n ++ " (mod " ++ show (period a) ++ ")"

instance (KnownNat m) => Periodic (IntegerModulo m) where
  period _ = natVal (Proxy :: Proxy m)

_normalize :: (KnownNat m) => IntegerModulo m -> IntegerModulo m
_normalize a@(IntegerModulo ia) = IntegerModulo $ ((ia `mod` p) + p) `mod` p where
  p = period a

_liftIM1 :: (Integer -> Integer) -> IntegerModulo m -> IntegerModulo m
_liftIM1 f a = undefined

_liftIM2 :: KnownNat m => (Integer -> Integer -> Integer) -> IntegerModulo m -> IntegerModulo m -> IntegerModulo m
_liftIM2 f (IntegerModulo a) (IntegerModulo b) = _normalize $ IntegerModulo $ f a b

instance (KnownNat m) => Num (IntegerModulo m) where
  fromInteger n = _normalize $ IntegerModulo n
  abs = _liftIM1 abs
  signum = _liftIM1 signum
  (+) = _liftIM2 (+)
  (*) = _liftIM2 (*)
  (-) = _liftIM2 (-)

instance (KnownNat m) => Eq (IntegerModulo m) where
  a == b = unIM (_normalize a) == unIM (_normalize b)

instance (KnownNat m) => Ord (IntegerModulo m) where
  compare a b = unIM (_normalize a) `compare` unIM (_normalize b) -- TODO

instance (KnownNat m) => Enum (IntegerModulo m) where
  toEnum a = _normalize $ IntegerModulo $ fromIntegral a
  fromEnum (IntegerModulo a) = fromIntegral a

instance (KnownNat m) => Real (IntegerModulo m) where
  toRational (IntegerModulo a) = toRational a

instance (KnownNat m) => Integral (IntegerModulo m) where
  toInteger  = unIM . _normalize
  quotRem (IntegerModulo a) (IntegerModulo b) = (c', r') where
    (c, r) = quotRem a b
    c' = _normalize $ IntegerModulo c
    r' = _normalize $ IntegerModulo r


newtype HoD = HoD { unHoD :: IntegerModulo 24 } deriving (Show, Num)
-- or type HoD = IntegerModulo 24

v1 :: HoD
v1 = 1 + 12 * 3 - 2

main :: IO ()
main = print $ v1

in GHCi

*Main> (1 + 2 + 3 * 5) :: IntegerModulo 10
8 (mod 10)
*Main> (1 + 2 + 3 * 5) :: IntegerModulo 5
3 (mod 5)
*Main> (1 + 2 + 3 * 5) :: IntegerModulo 17
1 (mod 17)
*Main> (1 + 2 + 3 * 5) :: IntegerModulo 100
18 (mod 100)