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

[Krzysztof Skrzętnicki]

On Fri, Apr 4, 2008 at 7:14 PM, Jake Mcarthur <jake.mcarthur at gmail.com> 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