[Haskell-cafe] Re: Shouldn't this loop indefinitely => take (last [0..]) [0..]

[John Meacham]

On Fri, Apr 04, 2008 at 04:46:22PM +0100, Neil Mitchell wrote:
> Where length xs = 1 and ys = 1000. This takes 1000 steps to tell the
> Int's aren't equal, since we don't have proper lazy naturals. If we
> did, it would take 2 steps.
> 
> Read this: http://citeseer.ist.psu.edu/45669.html - it argues the
> point I am trying to make, but much better.

I implemented this efficient lazy natural class once upon a time. it
even has things like lazy multiplication:



-- Copyright (c) 2007 John Meacham (john at repetae dot net)
-- 
-- Permission is hereby granted, free of charge, to any person obtaining a
-- copy of this software and associated documentation files (the
-- "Software"), to deal in the Software without restriction, including
-- without limitation the rights to use, copy, modify, merge, publish,
-- distribute, sublicense, and/or sell copies of the Software, and to
-- permit persons to whom the Software is furnished to do so, subject to
-- the following conditions:
-- 
-- The above copyright notice and this permission notice shall be included
-- in all copies or substantial portions of the Software.
-- 
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
-- OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-- MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-- IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
-- CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
-- TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
-- SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

-- efficient lazy naturals

module Util.LazyNum where

-- Nat data type is eqivalant to a type restricted lazy list that is strict in
-- its elements.
--
-- Invarients: (Sum x _) => x > 0
-- in particular (Sum 0 _) is _not_ valid and must not occur.

data Nat = Sum !Integer Nat | Zero
    deriving(Show)

instance Eq Nat where
    Zero == Zero = True
    Zero == _ = False
    _ == Zero = False
    Sum x nx == Sum y ny = case compare x y of
        EQ -> nx == ny
        LT -> nx == Sum (y - x) ny
        GT -> Sum (x - y) nx == ny


instance Ord Nat where
    Zero <= _ = True
    _ <= Zero = False
    Sum x nx <= Sum y ny = case compare x y of
        EQ -> nx <= ny
        LT -> nx <= Sum (y - x) ny
        GT -> Sum (x - y) nx <= ny

    Zero `compare` Zero = EQ
    Zero `compare` _ = LT
    _    `compare` Zero = GT
    Sum x nx `compare` Sum y ny = case compare x y of
        EQ -> nx `compare` ny
        LT -> nx `compare` Sum (y - x) ny
        GT -> Sum (x - y) nx `compare` ny

    x < y = not (x >= y)
    x >= y = y <= x
    x > y = y < x


instance Num Nat where
    Zero + y = y
    Sum x n1 + y = Sum x (y + n1)
    --x + Zero = x
    --Sum x n1 + Sum y n2 = Sum (x + y) (n1 + n2)

    Zero - _ = zero
    x - Zero = x
    Sum x n1 - Sum y n2 = case compare x y of
        GT -> Sum (x - y) n1 - n2
        EQ -> n1 - n2
        LT -> n1 - Sum (y - x) n2
    negate _ = zero
    abs x = x
    signum Zero = zero
    signum _ = one
    fromInteger x = if x <= 0 then zero else Sum x Zero

    Zero * _ = Zero
    _ * Zero = Zero
    (Sum x nx) * (Sum y ny) = Sum (x*y) ((f x ny) + (nx * (fint y + ny))) where
        f y Zero = Zero
        f y (Sum x n) = Sum (x*y) (f y n)



instance Real Nat where
    toRational n = toRational (toInteger n)

instance Enum Nat where
    succ x = Sum 1 x
    pred Zero = Zero
    pred (Sum n x) = if n == 1 then x else Sum (n - 1) x
    enumFrom x = x:[ Sum n x | n <- [1 ..]]
    enumFromThen x y = x:y:f (y + z) where
        z = y - x
        f x = x:f (x + z)
    toEnum = fromIntegral
    fromEnum = fromIntegral

-- d > 0
doDiv :: Nat -> Integer -> Nat
doDiv n d = f 0 n where
    f _ Zero = 0
    f cm (Sum x nx) = sum d (f m nx) where
        (d,m) = (x + cm) `quotRem` d
        sum 0 x = x
        sum n x = Sum n x

doMod :: Nat -> Integer -> Nat
doMod n d = f 0 n where
    f 0 Zero = Zero
    f r Zero = fint r
    f r (Sum x nx) = f ((r + x) `rem` d) nx

instance Integral Nat where
    _ `div` Zero = infinity
    n1 `div` n2 | n1 < n2 = 0
                 | otherwise = doDiv n1 (toInteger n2)
    n1 `mod` Zero = n1 -- XXX
    n1 `mod` n2 | n1 < n2 = n1
                | otherwise = doMod n1 (toInteger n2)
    n `divMod` Zero = (infinity,n)
    n `divMod` d | n < d = (0,n)
                 | otherwise = let d' = toInteger d in (doDiv n d',doMod n d')
    quotRem = divMod
    quot = div
    rem = mod
    toInteger n = f 0 n where
        f n _ | n `seq` False = undefined
        f n Zero = n
        f n (Sum x n1) = let nx = n + x in nx `seq` f nx n1

-- convert to integer unless it is too big, in which case Nothing is returned

natToInteger :: Integer -> Nat -> Maybe Integer
natToInteger limit n = f 0 n where
    f n _ | n > limit = Nothing
    f n Zero = Just n
    f n (Sum x n1) = let nx = n + x in nx `seq` f nx n1

natShow :: Nat -> String
natShow n = case natToInteger bigNum n of
    Nothing -> "(too big)"
    Just v -> show v

natFoldr :: (Integer -> b -> b) -> b -> Nat -> b
natFoldr cons nil n = f n where
    f Zero = nil
    f (Sum x r) = cons x (f r)

-- some utility routines

natEven :: Nat -> Bool
natEven n = f True n where
    f r Zero = r
    f r (Sum x n) = if even x then f r n else f (not r) n

natOdd :: Nat -> Bool
natOdd n = not (natEven n)

{-# RULES "even/natEven" even = natEven #-}
{-# RULES "odd/natOdd"   odd  = natOdd #-}

zero = Zero
one = Sum 1 Zero
infinity = Sum bigNum infinity
bigNum = 100000000000
fint x = Sum x Zero

-- random testing stuff for ghci

ti op x y = (toInteger $ x `op` y, toInteger x `op` toInteger y)

depth n | n <= 0 = error "depth exceeded"
        | otherwise = Sum n (depth $ n - 1)

depth' n | n <= 0 = Zero
         | otherwise = Sum n (depth' $ n - 1)