Fix off-by-one in e

number.cabal

@@ -28,10 +28,9 @@ library
                      Data.Number.Types,
                      Data.Number.Instances,
                      Data.Number.Internal
-                     Data.Number.Peano
    
   other-extensions:    TypeSynonymInstances, FlexibleInstances
-  build-depends:       base >=4.8 && < 5.0
+  build-depends:       base >=4.8 && < 5.0, natural-numbers
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -O2

src/Data/Number.hs

@@ -1,8 +1,8 @@
 -- | A library for real number arithmetics
 module Data.Number
 ( -- * Classes
-  Continued(..), Number
-, Nat(..), Whole(..)
+  Continued(..)
+, Number, Natural 
   -- * Functions
 , fromList, toList
 , fromNumber, toNumber
@@ -12,8 +12,8 @@ module Data.Number
 , hom, biHom, cut
 ) where
 
+import Data.Natural
 import Data.Number.Types
 import Data.Number.Instances
 import Data.Number.Functions
 import Data.Number.Internal
-import Data.Number.Peano

src/Data/Number/Functions.hs

@@ -4,15 +4,15 @@ module Data.Number.Functions where
 import Data.Number.Types
 import Data.Number.Instances
 import Data.Number.Internal
-import Data.Number.Peano
+import Data.Natural
 import Data.Ratio
 
 -- Various --
 
 -- | Get the precision of a 'Number' (i.e. length)
-precision :: Number -> Nat
-precision E       = Z
-precision (_:|xs) = S (precision xs)
+precision :: Number -> Natural
+precision E       = 0
+precision (_:|xs) = succ (precision xs)
 
 -- | Alternative show function that pretty prints a 'Number'
 -- also doing conversions from Peano numbers
@@ -26,12 +26,12 @@ show' (M (x:|xs)) = '-' : show (toInteger x) ++ " - 1/(" ++ show' xs ++ ")"
 -- Conversion --
 
 -- | Create a 'Number' from a list of naturals
-fromList :: [Nat] -> Number
+fromList :: [Natural] -> Number
 fromList []     = E
 fromList (x:xs) = x :| fromList xs
 
 -- | Convert a 'Number' to a list of naturals (losing the sign)
-toList :: Number -> [Nat]
+toList :: Number -> [Natural]
 toList E = []
 toList (x:|xs) = x : toList xs
 
@@ -61,7 +61,7 @@ toList (x:|xs) = x : toList xs
 --
 -- <<https://i.imgur.com/q1SwKoy.png>>
 e :: Number
-e = fmap a σ where 
+e = 1 + fmap a σ where 
   a n | p == 0    = 2*q
       | otherwise = 1
     where (q, p) = quotRem n 3

src/Data/Number/Instances.hs

@@ -6,7 +6,7 @@ module Data.Number.Instances where
 import Data.Number.Types
 import Data.Number.Internal
 
--- | transform a number applying a function ('Nat' -> 'Nat') to each
+-- | transform a number applying a function ('Natural' -> 'Natural') to each
 -- number preserving the sign.
 instance Functor Continued where
   fmap _ E       = E

src/Data/Number/Internal.hs

@@ -11,15 +11,15 @@ module Data.Number.Internal
 ) where
 
 import Data.Number.Types
-import Data.Number.Peano
+import Data.Natural
 import Data.Ratio
 
 -- | Homographic function coefficients matrix
-type Hom   = (Whole, Whole, Whole, Whole)
+type Hom   = (Integer, Integer, Integer, Integer)
 
 -- | Bihomographic function coefficients matrix
-type BiHom = (Whole, Whole, Whole, Whole,
-              Whole, Whole, Whole, Whole)
+type BiHom = (Integer, Integer, Integer, Integer,
+              Integer, Integer, Integer, Integer)
 
 -- | Homographic function
 --
@@ -35,7 +35,7 @@ type BiHom = (Whole, Whole, Whole, Whole,
 -- explanation.
 hom :: Hom -> Number -> Number
 hom (0, 0, _, _) _ = E
-hom (a, _, c, _) E = toNumber (fromPeano a % fromPeano c)
+hom (a, _, c, _) E = toNumber (a % c)
 hom h x = case maybeEmit h of
   Just d  -> join d (hom (emit h d) x)
   Nothing -> hom (absorb h x0) x'
@@ -44,7 +44,7 @@ hom h x = case maybeEmit h of
 
 -- Homographic helpers --
 
-maybeEmit :: Hom -> Maybe Whole
+maybeEmit :: Hom -> Maybe Integer
 maybeEmit (a, b, c, d) =
   if c /= 0 && d /= 0 && r == s
     then Just r
@@ -53,11 +53,11 @@ maybeEmit (a, b, c, d) =
         s = b // d
 
 
-emit :: Hom -> Whole -> Hom
+emit :: Hom -> Integer -> Hom
 emit (a, b, c, d) x = (c, d, a - c*x, b - d*x)
 
 
-absorb :: Hom -> Whole -> Hom
+absorb :: Hom -> Integer -> Hom
 absorb (a, b, c, d) x = (a*x + b, a, c*x + d, c)
 
 
@@ -86,7 +86,7 @@ biHom h x y = case maybeBiEmit h of
 
 -- Bihomographic helpers
 
-maybeBiEmit :: BiHom -> Maybe Whole
+maybeBiEmit :: BiHom -> Maybe Integer
 maybeBiEmit (a, b, c, d,
              e, f, g, h) =
   if e /= 0 && f /= 0 && g /= 0 && h /= 0 && ratiosAgree
@@ -95,17 +95,17 @@ maybeBiEmit (a, b, c, d,
   where r = quot a e
         ratiosAgree = r == b // f && r == c // g && r == d // h
 
-biEmit :: BiHom -> Whole -> BiHom
+biEmit :: BiHom -> Integer -> BiHom
 biEmit (a, b, c, d,
         e, f, g, h) x = (e,       f,       g,       h,
                          a - e*x, b - f*x, c - g*x, d - h*x)
 
-biAbsorbX :: BiHom -> Whole -> BiHom
+biAbsorbX :: BiHom -> Integer -> BiHom
 biAbsorbX (a, b, c, d,
            e, f, g, h) x = (a*x + b, a, c*x + d, c,
                             e*x + f, e, g*x + h, g)
 
-biAbsorbY :: BiHom -> Whole -> BiHom
+biAbsorbY :: BiHom -> Integer -> BiHom
 biAbsorbY (a, b, c, d,
            e, f, g, h) y = (a*y + c, b*y + d, a, b,
                             e*y + g, f*y + h, e, f)
@@ -121,38 +121,38 @@ fromX (_, b, c, d, _, f, g, h) = abs (g*h*b - g*d*f) < abs (f*h*c - g*d*f)
 toNumber :: RealFrac a => a -> Number
 toNumber 0 = E
 toNumber x
-  | x < 0     = M (toNumber (-x))
+  | x < 0     = M (toNumber (negate x))
   | x' == 0   = x0 :| E
   | otherwise = x0 :| toNumber (recip x')
   where (x0, x') = properFraction x
 
 -- | Truncate a 'Number' to a given length @n@
-cut :: Nat -> Number -> Number
+cut :: Natural -> Number -> Number
 cut _ E          = E
 cut n (M x)      = M (cut n x)
 cut n _ | n <= 0 = E
 cut n (x :| xs)  = x :| cut (n-1) xs
 
 
--- | Split a Number into a 'Whole' (the most significant of the fraction)
+-- | Split a Number into a 'Integer' (the most significant of the fraction)
 -- and the rest of the Number. Equivalent to @(floor x, x - floor x)@
 -- for a floating point.
-split :: Number -> (Whole, Number)
+split :: Number -> (Integer, Number)
 split x = (first x, rest x)
 
 
 -- | Essentially the inverse of split
-join :: Whole -> Number -> Number
-join (Whole x0 Neg) = M . (x0 :|)
-join (Whole x0 Pos) =     (x0 :|)
+join :: Integer -> Number -> Number
+join x0 x | x0 < 0    = M (negate (fromInteger x0) :| x)
+          | otherwise =   (fromInteger x0 :| x)
 
 
--- | Extract the first natural of the fraction as a 'Whole' number
-first :: Number -> Whole
+-- | Extract the first natural of the fraction as a 'Integer' number
+first :: Number -> Integer
 first E          = 0
 first (M E)      = 0
-first (M (x:|_)) = Whole x Neg
-first (x:|_)     = Whole x Pos
+first (M (x:|_)) = negate (toInteger x)
+first (x:|_)     = toInteger x
 
 
 -- | Extract the "tail" of a 'Number' as a new 'Number'
@@ -163,3 +163,8 @@ rest E       = E
 rest (M E)   = E
 rest (M x)   = M (rest x)
 rest (_:|xs) = xs
+
+
+-- | Alias to quot
+(//) :: Integral a => a -> a -> a
+(//) = quot

src/Data/Number/Peano.hs

@@ -1,225 +0,0 @@
--- | Value-level Peano arithmetic.
-module Data.Number.Peano where
-
-import Prelude hiding (foldr)
-import Data.Foldable  (Foldable(foldr))
-import Data.Ratio     ((%))
-
--- | Lazy Peano numbers. Allow calculation with infinite values.
-data Nat = Z -- ^Zero
-           | S Nat -- ^Successor
-   deriving (Show)
-
--- | Sign for whole numbers.
-data Sign = Pos | Neg deriving (Show, Eq, Ord, Enum, Read, Bounded)
-
--- | Whole numbers (Z).
-data Whole = Whole Nat Sign -- ^Construct a whole number out of a magnitue and a sign.
-
--- | The class of Peano-like constructions (i.e. Nat and Whole).
-class Enum a => Peano a where
-   -- | Test for zero.
-   isZero :: a -> Bool
-   -- | An unobservable infinity. For all finite numbers @n@, @n < infinity@ must
-   --  hold, but there need not be a total function that tests whether a number
-   --  is infinite.
-   infinity :: a
-   -- | Converts the number to an Integer.
-   fromPeano :: a -> Integer
-   -- | Reduces the absolute value of the number by 1. If @isZero n@, then
-   --  @decr n = n@ and vice versa.
-   decr :: a -> a
-
--- | Negation of 'isZero'.
-isSucc :: Peano n => n -> Bool
-isSucc = not . isZero
-
--- | Peano class instance
-instance Peano Nat where
-   isZero Z = True
-   isZero _ = False
-   infinity = S infinity
-   fromPeano Z = 0
-   fromPeano (S n) = succ $ fromPeano n
-   decr = pred
-
--- | Peano class instance
--- defines infinity (positive) and other functions handling the sign
-instance Peano Whole where
-   isZero (Whole n _) = isZero n
-   infinity = Whole infinity Pos
-   fromPeano (Whole n Pos) = fromPeano n
-   fromPeano (Whole n Neg) = negate $ fromPeano n
-   decr (Whole n s) = Whole (pred n) s
-
--- | Removes at most 'S' constructors from a Peano number.
---  Outputs the number of removed constructors and the remaining number.
-takeNat :: (Num a, Enum a, Ord a, Peano n) => a -> n -> (a, n)
-takeNat = takeNat' 0
-   where
-      takeNat' c i n | i <= 0    = (c, n)
-                     | isZero n  = (c, n)
-                     | otherwise = takeNat' (succ c) (pred i) (decr n)
-
--- | Extract the 'Nat' value of a 'Whole'
-toNat :: Whole -> Nat
-toNat (Whole n _) = n
-
--- | Alias to quot
-(//) :: Integral a => a -> a -> a
-(//) = quot
-
--- | The lower bound is zero, the upper bound is infinity.
-instance Bounded Nat where
-   minBound = Z
-   maxBound = infinity
-
--- | The bounds are negative and positive infinity.
-instance Bounded Whole where
-   minBound = Whole infinity Neg
-   maxBound = infinity
-
--- | The 'pred' function is bounded at Zero.
-instance Enum Nat where
-   toEnum = fromInteger . fromIntegral
-   fromEnum = fromInteger . fromPeano
-   succ = S
-   pred Z = Z
-   pred (S n) = n
-
--- |'succ' and 'pred' work according to the total
---  order on the whole numbers, i.e. @succ n = n+1@ and @pred n = n-1@.
-instance Enum Whole where
-   toEnum i | i < 0     = Whole (toEnum i) Neg
-            | otherwise = Whole (toEnum i) Pos
-   fromEnum = fromInteger . fromPeano
-   succ (Whole (S n) Neg) = Whole n Neg
-   succ (Whole n Pos) = Whole (S n) Pos
-   succ (Whole Z _) = Whole (S Z) Pos
-   pred (Whole (S n) Pos) = Whole n Pos
-   pred (Whole n Neg) = Whole (S n) Neg
-   pred (Whole Z _) = Whole (S Z) Neg
-
--- | Addition, multiplication, and subtraction are
---  lazy in both arguments, meaning that, in the case of infinite values,
---  they can produce an infinite stream of S-constructors. As long as
---  the callers of these functions only consume a finite amount of these,
---  the program will not hang.
---
---  @fromInteger@ is not injective in case of 'Nat', since negative integers
---  are all converted to zero ('Z').
-instance Num Nat where
-   (+) Z n = n
-   (+) n Z = n
-   (+) (S n) (S m) = S $ S $ (+) n m
-
-   (*) Z n = Z
-   (*) n Z = Z
-   (*) (S n) (S m) = S Z + n + m + (n * m)
-
-   abs = id
-
-   signum _ = S Z
-
-   fromInteger i | i <= 0    = Z
-                 | otherwise = S $ fromInteger $ i - 1
-
-   (-) Z n = Z
-   (-) n Z = n
-   (-) (S n) (S m) = n - m
-
--- | Implements arithmetics for Whole numbers
-instance Num Whole where
-   (+) (Whole n Pos) (Whole m Pos) = Whole (n+m) Pos
-   (+) (Whole n Neg) (Whole m Neg) = Whole (n+m) Neg
-   (+) (Whole n Pos) (Whole m Neg) | n >= m    = Whole (n-m) Pos
-                                   | otherwise = Whole (m-n) Neg
-   (+) (Whole n Neg) (Whole m Pos) = Whole m Pos + Whole n Neg
-
-   (*) (Whole n s) (Whole m t) | s == t    = Whole (n*m) Pos
-                               | otherwise = Whole (n*m) Neg
-
-   (-) n (Whole m Neg) = n + (Whole m Pos)
-   (-) n (Whole m Pos) = n + (Whole m Neg)
-
-   abs (Whole n s) = Whole n Pos
-
-   signum (Whole Z _) = Whole Z Pos
-   signum (Whole _ Pos) = Whole (S Z) Pos
-   signum (Whole _ Neg) = Whole (S Z) Neg
-
-   fromInteger i | i < 0     = Whole (fromInteger $ negate i) Neg
-                 | otherwise = Whole (fromInteger i) Pos
-
-
--- |'==' and '/=' work as long as at least one operand is finite.
-instance Eq Nat where
-   (==) Z Z = True
-   (==) Z (S _) = False
-   (==) (S _) Z = False
-   (==) (S n) (S m) = n == m
-
--- | Positive and negative zero are considered equal.
-instance Eq Whole where
-   (==) (Whole Z _) (Whole Z _) = True
-   (==) (Whole n s) (Whole m t) = s == t && n == m
-
--- | All methods work as long as at least one operand is finite.
-instance Ord Nat where
-   compare Z Z = EQ
-   compare Z (S _) = LT
-   compare (S _) Z = GT
-   compare (S n) (S m) = compare n m
-
--- | The ordering is the standard total order on Z. Positive and negative zero
---  are equal.
-instance Ord Whole where
-   compare (Whole Z _) (Whole Z _) = EQ
-   compare (Whole _ Neg) (Whole _ Pos) = LT
-   compare (Whole _ Pos) (Whole _ Neg) = GT
-   compare (Whole n Pos) (Whole m Pos) = compare n m
-   compare (Whole n Neg) (Whole m Neg) = compare m n
-
--- | Returns the length of a foldable container as 'Nat'. The number is generated
---  lazily and thus, infinitely large containers are supported.
-natLength :: Foldable f => f a -> Nat
-natLength = foldr (const S) Z
-
--- | Since 'toRational' returns a @Ratio Integer@, it WILL NOT terminate on infinities.
-instance Real Nat where
-   toRational = (%1) . fromPeano
-
--- | Since 'toRational' returns a @Ratio Integer@, it WILL NOT terminate on infinities.
-instance Real Whole where
-  toRational = (%1) . fromPeano
-
--- | Since negative numbers are not allowed,
---  @'quot' = 'div'@ and @'rem' = 'mod'@. The methods 'quot', 'rem', 'div', 'mod',
---  'quotRem' and 'divMod' will terminate as long as their first argument is
---  finite. Infinities in their second arguments are permitted and are handled
---  as follows:
---
---  @
---  n `quot` infinity   =   n `div` infinity   =   0
---  n `rem`  infinity   =   n `mod` infinity   =   n@
-instance Integral Nat where
-   quotRem _ Z = error "divide by zero"
-   quotRem n (S m) = quotRem' Z n (S m)
-      where
-         quotRem' q n m | n >= m    = quotRem' (S q) (n-m) m
-                        | otherwise = (q,n)
-
-   divMod = quotRem
-   toInteger = fromPeano
-
--- | Integer conversions and division
-instance Integral Whole where
-  toInteger = fromPeano
-
-  quotRem (Whole a s) (Whole b s') = (Whole q sign, Whole r Pos)
-    where
-      q = quot a b
-      r = a - q * b
-      sign | s == s' && s == Pos = Pos
-           | s == s' && s == Neg = Pos
-           | otherwise           = Neg

src/Data/Number/Types.hs

@@ -1,7 +1,7 @@
 -- | Definition of the continued fraction type
 module Data.Number.Types where
 
-import Data.Number.Peano
+import Data.Natural
 
 infixr 5 :|
 -- | ==Continued fraction type
@@ -27,4 +27,4 @@ data Continued a =
   deriving (Eq, Ord, Show, Read)
 
 -- | Real numbers datatype (a continued fraction of naturals)
-type Number = Continued Nat
+type Number = Continued Natural