{-# LANGUAGE ScopedTypeVariables, EmptyDataDecls #-}

module Data.ProxN.Peano where

data Zero
data Succ n

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five
type Seven = Succ Six
type Eight = Succ Seven
type Nine = Succ Eight
type Ten = Succ Nine

class Peano p where
  fromPeano :: p -> Int

instance Peano Zero where
  fromPeano _ = 0

instance (Peano p) => Peano (Succ p) where
  fromPeano _ = 1 + (fromPeano (undefined :: p))

class (Peano p) => Logarithm p where
  logarithm :: p -> Double -> Double
  logarithm _ a = log a / log (fromIntegral (fromPeano (undefined :: p)))

instance Logarithm Zero

instance (Peano a) => Logarithm (Succ a)