On Fri, Apr 4, 2008 at 7:14 PM, Jake Mcarthur <[EMAIL PROTECTED]> wrote: > 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe