{- | Lazy Peano numbers represent natural numbers inclusive infinity. Since they are lazily evaluated, they are optimally for use as number type for 'Data.List.genericLength' et.al. -} module PeanoNumber where import Data.Array (Ix(..)) import Data.Monoid (Monoid, mempty, mappend, ) import Data.List (genericReplicate, ) import Control.Monad.Trans.Writer (Writer, writer, runWriter, tell, ) import qualified Data.List.HT as ListHT data T = Zero | Succ T deriving (Show, Read, Eq) infinity :: T infinity = Succ infinity err :: String -> String -> a err func msg = error ("PeanoNumber."++func++": "++msg) isZero :: T -> Bool isZero Zero = True isZero (Succ _) = False add :: T -> T -> T add Zero y = y add (Succ x) y = Succ (add x y) sub :: T -> T -> T sub x y = let (sign,z) = subNeg x y in if sign then err "sub" "negative difference" else z subNeg :: T -> T -> (Bool, T) subNeg Zero y = (False, y) subNeg x Zero = (True, x) subNeg (Succ x) (Succ y) = subNeg x y {- fails for isAscending (infinity:infinity:[5] :: [T]) isAscending :: [T] -> Bool isAscending [] = True isAscending (x:xs) = if isZero x then isAscending xs else let (signs,residues) = unzip $ map (subNeg x) xs in not (or signs) && isAscending residues -} {- fails for isAscending (3:2:[5..] :: [T]) isAscending :: [T] -> Bool isAscending [] = True isAscending xt@(x:xs) = if isZero x then isAscending xs else not (any isZero xs) && isAscending (map pred xt) -} isAscendingFiniteList :: [T] -> Bool isAscendingFiniteList [] = True isAscendingFiniteList (x:xs) = let decrement (Succ y) = Just y decrement _ = Nothing in case x of Zero -> isAscendingFiniteList xs Succ xd -> case mapM decrement xs of Nothing -> False Just xsd -> isAscendingFiniteList (xd : xsd) {- | This fails for > *PeanoNumber> isAscendingNaive (3:infinity:infinity:4:[] :: [T]) > Interrupted. > *PeanoNumber> isAscending (3:infinity:infinity:4:[] :: [T]) > False -} isAscendingFiniteNumbers :: [T] -> Bool isAscendingFiniteNumbers = ListHT.isAscending {- | In @glue x y == (z,r,b)@ @z@ represents @min x y@, @r@ represents @max x y - min x y@, and @x<=y == b@. Cf. Numeric.NonNegative.Chunky -} glue :: T -> T -> (T, T, Bool) glue Zero ys = (Zero, ys, True) glue xs Zero = (Zero, xs, False) glue (Succ xs) (Succ ys) = let (common, difference, sign) = glue xs ys in (Succ common, difference, sign) compareNeighbors :: [T] -> [(Bool,T)] compareNeighbors = ListHT.mapAdjacent (\x y -> let (costs,_,le) = glue x y in (le,costs)) {- | efficient implementation of @x0 <= x1 && x1 <= x2 ...@ > *PeanoNumber> isAscending (3:2:[5..] :: [T]) > False -} {- Implementation notes: We check all pairs of adjacent numbers for correct order. We obtain a set of booleans, which must all be True. The order of checking these booleans is crucial. Pairs of numbers that are infinitely big or infinitely far in the list must be checked \"last\". Thus we order the booleans according to their computation costs (list position + magnitude of number) using a Cantor diagonalisation. -} isAscending :: [T] -> Bool isAscending = and . concat . foldr (\(le,costs) acc -> addAt [le] costs ([]:acc)) [] . compareNeighbors addAt :: Monoid a => a -> T -> [a] -> [a] addAt x = let recourse n [] = genericReplicate n mempty ++ [x] recourse Zero (y:ys) = mappend x y : ys recourse (Succ n) (y:ys) = y : recourse n ys in recourse {- replicate :: T -> a -> [a] replicate Zero _ = [] replicate (Succ n) x = x : replicate n x -} -- isAscending - use a Writer monad to store the costs -- following an idea of vixy http://moonpatio.com:8080/fastcgi/hpaste.fcgi/view?id=562 newtype Costs = Costs T deriving (Show, Eq, Ord) instance Monoid Costs where mempty = Costs Zero mappend (Costs x) (Costs y) = Costs $ x+y infixr 3 &&~ {- inefficient because of subNeg (&&~) :: Writer Costs Bool -> Writer Costs Bool -> Writer Costs Bool (&&~) (Writer (xb, Costs xc)) (Writer (yb, Costs yc)) = let (zc,zb) = argMinFull (xc,xb) (yc,yb) (wc,wb) = -- for laziness we assign to temporary pair via 'let' if zb then (snd $ subNeg xc yc, xb && yb) else (Zero, zb) in Writer (wb, Costs $ zc+wc) -} {- | Compute '(&&)' with minimal costs. -} (&&~) :: Writer Costs Bool -> Writer Costs Bool -> Writer Costs Bool (&&~) x y = let (xb, Costs xc) = runWriter x (yb, Costs yc) = runWriter y (minc,difc,le) = glue xc yc (bCheap,bExpensive) = if le then (xb,yb) else (yb,xb) in tell (Costs minc) >> writer (if bCheap then (bExpensive, Costs difc) else (False, mempty)) andW :: [Writer Costs Bool] -> Writer Costs Bool andW = foldr (\b acc -> b &&~ (tell (Costs 1) >> acc)) (return True) leW :: T -> T -> Writer Costs Bool leW x y = let (minc,_difc,le) = glue x y in writer (le, Costs minc) {- For this simple function we do not really need the Writer monad, and thus the Monoid instance of Costs. -} isAscendingW :: [T] -> Writer Costs Bool isAscendingW = andW . ListHT.mapAdjacent leW {- test with *Number.Peano> Control.Monad.Writer.runWriter $ isAscendingW [0,infinity,infinity,5] (False,Costs (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))) -} mul :: T -> T -> T mul Zero _ = Zero mul _ Zero = Zero mul (Succ x) y = add y (mul x y) fromPosIntegral :: (Integral a) => a -> T fromPosIntegral 0 = Zero fromPosIntegral n = Succ (fromPosIntegral (pred n)) toIntegral :: (Integral a) => T -> a toIntegral Zero = 0 toIntegral (Succ x) = succ (toIntegral x) instance Num T where (+) = add (-) = flip sub (*) = mul negate Zero = Zero negate (Succ _) = err "negate" "cannot negate positive number" signum Zero = Zero signum (Succ _) = Succ Zero abs = id fromInteger n = if n<0 then err "fromInteger" "Peano numbers are always non-negative" else fromPosIntegral n instance Enum T where pred Zero = err "pred" "Zero has no predecessor" pred (Succ x) = x succ = Succ toEnum n = if n<0 then err "toEnum" "Peano numbers are always non-negative" else fromPosIntegral n fromEnum = toIntegral enumFrom x = iterate Succ x enumFromThen x y = let (sign,d) = subNeg x y in if sign then iterate (sub d) x else iterate (add d) x {- enumFromTo = enumFromThenTo = -} {- The default instance is good for compare, but fails for min and max. -} instance Ord T where compare (Succ x) (Succ y) = compare x y compare Zero (Succ _) = LT compare (Succ _) Zero = GT compare Zero Zero = EQ min (Succ x) (Succ y) = Succ (min x y) min _ _ = Zero max (Succ x) (Succ y) = Succ (max x y) max Zero y = y max x Zero = x {- This special implementation works also for undefined < Zero. Thanks to Peter Divianszky for the hint. -} _ < Zero = False Zero < _ = True Succ n < Succ m = n < m x > y = y < x x <= y = not (y < x) x >= y = not (x < y) {- | cf. How to find the shortest list in a list of lists efficiently, this means, also in the presence of infinite lists. -} argMinFull :: (T,a) -> (T,a) -> (T,a) argMinFull (x0,xv) (y0,yv) = let recourse (Succ x) (Succ y) = let (z,zv) = recourse x y in (Succ z, zv) recourse Zero _ = (Zero,xv) recourse _ _ = (Zero,yv) in recourse x0 y0 {- | On equality the first operand is returned. -} argMin :: (T,a) -> (T,a) -> a argMin x y = snd $ argMinFull x y argMinimum :: [(T,a)] -> a argMinimum = snd . foldl1 argMinFull argMaxFull :: (T,a) -> (T,a) -> (T,a) argMaxFull (x0,xv) (y0,yv) = let recourse (Succ x) (Succ y) = let (z,zv) = recourse x y in (Succ z, zv) recourse x Zero = (x,xv) recourse _ y = (y,yv) in recourse x0 y0 {- | On equality the first operand is returned. -} argMax :: (T,a) -> (T,a) -> a argMax x y = snd $ argMaxFull x y argMaximum :: [(T,a)] -> a argMaximum = snd . foldl1 argMaxFull instance Real T where toRational = toRational . toInteger instance Integral T where rem = div quot = mod quotRem = divMod div x y = fst (divMod x y) mod x y = snd (divMod x y) divMod x y = let (sign,d) = subNeg y x in if sign then (0,x) else let (q,r) = divMod d y in (succ q,r) toInteger = toIntegral instance Ix T where range = uncurry enumFromTo index (lower,_) i = let (sign,offset) = subNeg lower i in if sign then err "index" "index out of range" else toIntegral offset inRange (lower,upper) i = isAscending [lower, i, upper] rangeSize (lower,upper) = toIntegral (sub lower (succ upper)) instance Bounded T where minBound = Zero maxBound = infinity