{-# LANGUAGE EmptyDataDecls #-}

module Modulo where

data Z
zero :: Z
zero = undefined
data S a

predecessor :: S a -> a
predecessor = undefined

class Nat a where
  toInteger :: a -> Integer

instance Nat Z where
  toInteger _ = 0

instance Nat a => Nat (S a) where
  toInteger = (1 +) . Modulo.toInteger . predecessor

newtype Modulo a b = Modulo (a,b)

instance Eq b => Eq (Modulo a b) where
  Modulo (_,x) == Modulo (_,y) = x == y

instance Show b => Show (Modulo a b) where
  show (Modulo (_,x)) = show x

instance (Nat a, Integral b) => Num (Modulo a b) where
  Modulo (m,x) + Modulo (_,y) = Modulo (m,z)
    where z = (x+y) `mod` fromInteger (Modulo.toInteger m)
  Modulo (m,x) - Modulo (_,y) = Modulo (m,z)
    where z = (x-y) `mod` fromInteger (Modulo.toInteger m)
  Modulo (m,x) * Modulo (_,y) = Modulo (m,z)
    where z = (x*y) `mod` fromInteger (Modulo.toInteger m)
  abs = id
  signum (Modulo (m,x)) = Modulo $ (m,signum x)
  fromInteger n = Modulo (m,z)
    where z = fromInteger (n `mod` Modulo.toInteger m)
          m = undefined :: Nat a => a

type Zero  = Z
type One   = S Zero
type Two   = S One      ; type Modulo2 = Modulo Two Int
type Three = S Two      ; type Modulo3 = Modulo Three Int
type Four  = S Three    ; type Modulo4 = Modulo Four Int
type Five  = S Four     ; type Modulo5 = Modulo Five Int
type Six   = S Five     ; type Modulo6 = Modulo Six Int
type Seven = S Six      ; type Modulo7 = Modulo Seven Int
type Eight = S Seven    ; type Modulo8 = Modulo Eight Int
type Nine  = S Eight    ; type Modulo9 = Modulo Nine Int
type Ten   = S Nine     ; type Modulo10= Modulo Ten Int