On Thu, Apr 3, 2008 at 10:35 PM, Bryan O'Sullivan wrote:

It's not an infinite list. It's a list of length maxBound::Int, as required by the fact that take's first argument is an Int. The second argument is probably defaulting to Integer.

Right! The first arg of "take" makes the first list into a int list. I did not wait long enough to see the end of the list and I'm so used to represent infinite lists with [0..] that I didn't think it could be limited. Thanks for the explanation! Olivier.

cdsmith:

Bryan O'Sullivan wrote:

...

It's not an infinite list. It's a list of length maxBound::Int, as required by the fact that take's first argument is an Int. The second argument is probably defaulting to Integer.

Which, incidentally, also explains why Don couldn't reproduce it on a 64- bit system. There, instead of hanging for about a minute before printing out the list, it would hang for about 4 billion minutes.

It's also interesting how our 32 bit machines are fast enough now to make Int indices noticeably problematic. And thankfully, 64 bit machines are common enough now that the 32 bit Int issues are less of an issue. length, take, drop and index working on machine-sized Ints by default are really a bit of a wart, aren't they? -- Don

On Thu, Apr 3, 2008 at 11:13 PM, Don Stewart wrote:

length, take, drop and index working on machine-sized Ints by default are really a bit of a wart, aren't they?

-- Don

Agreed, Olivier.

On Fri, Apr 04, 2008 at 12:34:54PM +0100, Neil Mitchell wrote:

...

length, take, drop and index working on machine-sized Ints by default are really a bit of a wart, aren't they?

Yes. Also, having strict Int's by default is a bit ugly, in an otherwise lazy-by-default language. It's a place where Haskell decided to remove mathematical elegance for pragmatic speed...

(Not that it isn't a worthwhile trade off, but it is still loosing something to gain something else)

Personally, I like Ints. -- David Roundy Department of Physics Oregon State University

...

...

Also, having strict Int's by default is a bit ugly, in an otherwise lazy-by-default language.

I meant: (\x (y :: Int) -> x + 1) 1 (1/0 :: Int) <=> _|_ ?

Division by 0 is still an error. What I mean is: length xs == length ys 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. Thanks Neil

Hi

...

...

I meant: (\x (y :: Int) -> x + 1) 1 (1/0 :: Int) <=> _|_ ?

Division by 0 is still an error. What I mean is:

Yes, but this particular one need not be performed. Will it be?

Oh, sorry, I misread that. Even with current Haskell's Int's that is lazy enough to work, and won't crash.

...

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.

Err, really? I mean, could we calculate this equality without reducing length ys to weak head normal form (and then to plain normal form)?

Not without lazy naturals, or some other way of returning the result of length lazily.

What do you mean by "proper Lazy naturals"? Peano ones?

Yes Thanks Neil

On Apr 4, 2008, at 11:31 AM, Loup Vaillant wrote:

I mean, could we calculate this equality without reducing length ys to weak head normal form (and then to plain normal form)?

Yes. Suppose equality over Nat is defined something like: Z == Z = True S x == S y = x == y x == y = False And also suppose the length function actually returns a Nat instead of an Int. Now the expression reduces as: length xs == length ys S (length xs') == S (length ys') Z == S (length ys'') False That would not be possible without lazy Nats. - Jake

Hi

We can however write function like this:

eqLengths [] [] = True eqLengths (x:xs) (y:ys) = eqLengths ys xs eqLengths _ _ = False

which looks just fine for me.

I have this defined function. I also have lenEq1, lenGt1, and a few other variants. It works, but it just doesn't feel elegant. Note: In case anyone gets the wrong impression, I am not suggesting lazy naturals be the standard numeric type in Haskell, just that by not going that way we have paid a cost in terms of elegance. Thanks Neil

On Fri, Apr 4, 2008 at 5:45 PM, Don Stewart wrote:

ndmitchell:

...

Note: In case anyone gets the wrong impression, I am not suggesting lazy naturals be the standard numeric type in Haskell, just that by not going that way we have paid a cost in terms of elegance.

I'd be happy if we had an (unbounded) Nat type in the first place...

The problem with Nat is that we can't comfortably make it an instance of Num. (Well, that's arguably a problem with Num.) -- Dave Menendez http://www.eyrie.org/~zednenem/

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)

On Sun, Apr 06, 2008 at 11:30:20AM -0300, Felipe Lessa wrote:

On Sun, Apr 6, 2008 at 11:12 AM, John Meacham wrote:

...

I implemented this efficient lazy natural class once upon a time. it even has things like lazy multiplication: [...] 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) [...]

May I ask you why the last line above was commented out?

Notice it flips the order of the arguments with each iteration. This allows it to avoid space leaks in some cases, for instance if you have infinity + (space wasting thunk), the space wasting thunk will never be deallocated even though it isn't used. It also means that the strictness properties are more symmetric than they would be otherwise as people expect of (+). John -- John Meacham - ⑆repetae.net⑆john⑈

On Mon, Apr 07, 2008 at 04:45:31AM -0700, David Roundy wrote:

I wonder about the efficiency of this implementation. It seems that for most uses the result is that the size of a Nat n is O(n), which means that in practice you probably can't use it for large numbers.

e.g. it seems like

last [1..n :: Nat]

should use O(n) space, where

last [1..n :: Integer]

should take O(1) space. And I can't help but imagine that there must be scenarios where the memory use goes from O(N) to O(N^2), which seems pretty drastic. I imagine this is an inherent cost in the use of lazy numbers? Which is probably why they're not a reasonable default, since poor space use is often far more devastating then simple inefficiency. And of course it is also not always more efficient than strict numbers.

Oh, yes. I certainly wouldn't recommend them as some sort of default, they were sort of a fun project and might come in handy some day. By efficient, I meant more efficient than the standard lazy number formulation of data Num = Succ Num | Zero not more efficient than strict types, which it very much is not. :) John -- John Meacham - ⑆repetae.net⑆john⑈

"Neil Mitchell" writes:

...

length, take, drop and index working on machine-sized Ints by default are really a bit of a wart, aren't they?

Yes. Also, having strict Int's by default is a bit ugly, [..] (Not that it isn't a worthwhile trade off, but it is still loosing something to gain something else)

Presumably you refer to the latter point - Int strictness - here? I don't think "optimizing" list operations (take, length etc) to Int buys you much performance - traversing the list is going to be far more expensive. (Or so I believe - anybody care to benchmark it?) Unfortunately, the "genericLenght" name is about as clumsy syntactically as Int is semantically, so it's about an even trade-off :-) -k -- If I haven't seen further, it is by standing in the footprints of giants