On Mon, Sep 24, 2007 at 06:28:59PM +0200, apfelmus wrote:

I mean, Haskell does not magically detect that the 32(64)-bit integer (10 + length [11..]) :: Int is bigger than 10 :: Int .

That's partly because it's not true. There are arbitrarily large finite lists for which the equivalent is false, e.g. on a 32bit machine: Prelude> 10 + length (replicate maxBound 'a') -2147483639 Thanks Ian

Jonathan Cast wrote:

On Mon, 2007-09-24 at 17:35 +0100, Andrew Coppin wrote:

...

...

In an ideal world, yes.

In this world, use "length (take 11 [1..]) > 10"...

not (null (drop 10 [1..])) is surely faster (not tested...)

Faster? There might be a few microseconds in it. Clearer? Possibly... ;-)

Neil Mitchell wrote:

Hi

lengthNat [1..] > 10

Couldn't be clearer, and can be made to work perfectly. If anyone does want to pick up the lazy naturals work, I can send over the code (or write it yourself - its not hard!)

Um... isn't a lazy natural just a list with no data, where the list length encodes a number?

Neil Mitchell wrote:

Hi

...

Um... isn't a lazy natural just a list with no data, where the list length encodes a number?

Pretty much, yes.

So I just need to write newtype LazyNatural = LazyNatural [()] and then add some suitable instances. ;-) (Woah... that's one bizzare-looking type there!) Hey, the "length" function would then just be ln_length :: [x] -> LazyNatural ln_length = LazyNatural . map (const ()) Ooo, that's hard.

Neil Mitchell wrote:

Hi

...

...

Pretty much, yes.

So I just need to write

newtype LazyNatural = LazyNatural [()]

or

data Nat = Zero | Succ Nat

it's your choice really.

I'm guessing there's going to be fairly minimal performance difference. (Or maybe there is. My way uses a few additional pointers. But it also allows me to elegantly recycle existing Prelude list functions, so...)

...

and then add some suitable instances. ;-)

Yes. Lots of them. Lots of instances and lots of methods.

...

Hey, the "length" function would then just be

ln_length :: [x] -> LazyNatural ln_length = LazyNatural . map (const ())

Ooo, that's hard.

Nope, its really easy. Its just quite a bit of work filling in all the instances. I bet you can't do it and upload the results to hackage within 24 hours :-)

*ALL* the instances? No. A small handful of them? Sure. How about this... module LazyNatural (LazyNatural ()) where import Data.List newtype LazyNatural = LN [()] instance Show LazyNatural where show (LN x) = "LN " ++ show (length x) instance Eq LazyNatural where (LN x) == (LN y) = x == y instance Ord LazyNatural where compare (LN x) (LN y) = raw_compare x y raw_compare ([]) (_:_) = LT raw_compare ([]) ([]) = EQ raw_compare (_:_) ([]) = GT raw_compare (_:x) (_:y) = raw_compare x y instance Num LazyNatural where (LN x) + (LN y) = LN (x ++ y) (LN x) - (LN y) = LN (raw_minus x y) (LN x) * (LN y) = LN (concatMap (const x) y) negate _ = error "negate is not defined for LazyNatural" abs = id signum (LN []) = LN [] signum (LN _) = LN [()] fromInteger = LN . flip genericReplicate () raw_minus (_:a) (_:b) = raw_minus a b raw_minus (a) ([]) = a raw_minus _ _ = error "negative result from subtraction"

Since natural numbers are trivial to implement (inefficiently) I took 15 minutes and added them to my numbers package in Hackage. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numbers-2007.9.24 -- Lennart On 9/24/07, Andrew Coppin wrote:

Neil Mitchell wrote:

...

Hi

...

...

Pretty much, yes.

So I just need to write

newtype LazyNatural = LazyNatural [()]

or

data Nat = Zero | Succ Nat

it's your choice really.

I'm guessing there's going to be fairly minimal performance difference. (Or maybe there is. My way uses a few additional pointers. But it also allows me to elegantly recycle existing Prelude list functions, so...)

...

...

and then add some suitable instances. ;-)

Yes. Lots of them. Lots of instances and lots of methods.

...

Hey, the "length" function would then just be

ln_length :: [x] -> LazyNatural ln_length = LazyNatural . map (const ())

Ooo, that's hard.

Nope, its really easy. Its just quite a bit of work filling in all the instances. I bet you can't do it and upload the results to hackage within 24 hours :-)

*ALL* the instances? No.

A small handful of them? Sure. How about this...

module LazyNatural (LazyNatural ()) where

import Data.List

newtype LazyNatural = LN [()]

instance Show LazyNatural where show (LN x) = "LN " ++ show (length x)

instance Eq LazyNatural where (LN x) == (LN y) = x == y

instance Ord LazyNatural where compare (LN x) (LN y) = raw_compare x y

raw_compare ([]) (_:_) = LT raw_compare ([]) ([]) = EQ raw_compare (_:_) ([]) = GT raw_compare (_:x) (_:y) = raw_compare x y

instance Num LazyNatural where (LN x) + (LN y) = LN (x ++ y) (LN x) - (LN y) = LN (raw_minus x y) (LN x) * (LN y) = LN (concatMap (const x) y) negate _ = error "negate is not defined for LazyNatural" abs = id signum (LN []) = LN [] signum (LN _) = LN [()] fromInteger = LN . flip genericReplicate ()

raw_minus (_:a) (_:b) = raw_minus a b raw_minus (a) ([]) = a raw_minus _ _ = error "negative result from subtraction"

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 2007-09-24, Andrew Coppin wrote:

Neil Mitchell wrote:

...

Hi

lengthNat [1..] > 10

Couldn't be clearer, and can be made to work perfectly. If anyone does want to pick up the lazy naturals work, I can send over the code (or write it yourself - its not hard!)

Um... isn't a lazy natural just a list with no data, where the list length encodes a number?

That's one particularly simple representation, yes. "Lazy Unary". One can also construct other representations that may be more efficient in certain situations. -- Aaron Denney -><-

On Mon, 24 Sep 2007, Vimal wrote:

Wow, half an hour, about 7 replies :) I dont know which one to quote!

Okay. So, why is GHC finding it difficult to conclude that length is always > 0? Suppose I define length like:

length [] = 0 length (x:xs) = 1 + length xs

Hmm, well, I think the fact that we, as humans, expecting GHC to infer length (any list) > 0 is pretty unfair :)

What I had in mind was, when GHC was able to do so many things like pattern matching, data type inference, why not this!

Pattern matching is much easier than you might think. If you'll let me handwave at you a little, all pattern matches can be translated into a series of case statements where each pattern consists of either a variable or a constructor with variables to bind each of the constructor's parameters to. This isn't actually much more complicated than an old-fashioned switch statement! Type inference is a little more complicated, but largely revolves around a process similar to (but more powerful than) pattern-matching called unification. There's no magic involved, just sufficiently advanced technology. That part applies especially to lazy evaluation! Every time a pattern-match is done, evaluation proceeds far enough to find the constructor involved in order to select the right branch. Conceptually, the Int type looks like data Int = 1 | 2 | 3 | ... which means that an Int is either fully evaluated or completely unevaluated - if you try to evaluate "just enough to know it's > 0" then you'll still fully evaluate it. A good rule of thumb is to never expect (or perhaps, never require) GHC to do anything that requires it to prove something you're not extremely sure you've already written an explicit proof for in the code. -- flippa@flippac.org The task of the academic is not to scale great intellectual mountains, but to flatten them.

From the wiki: If you write it, you force Haskell to create all list nodes. ...

Alright. Now, lets look at the definition again:

length [] = 0 length (x:xs) = 1 + length xs

We see that the value of *x* isnt needed at all. So, why does GHC allocate so much memory creating all those *x*s? because, if we have: length [1..] = 1 + length [2...] = 1 + 1 + length [3...] This should go on, into an infinite loop. GHC doesnt need to create all nodes! The wiki also claims that *x* isnt evaluated. So, why allocate space for it when its not evaluated?