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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
