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

[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.

- Jake