On Fri, Apr 4, 2008 at 7:14 PM, Jake Mcarthur
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.
One thing to notice is that with lazy Nats this code: length [] == length [1..] would terminate, while on 64 bit platform it is "almost bottom" :-) Theoretically it is even worse: genericLength [] == genericLength [1..] :: Integer will never terminate and eat infinite amount of memory along the way, while genericLength [] == genericLength [1..] :: Nat will do just fine. 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. Christopher Skrzętnicki