[Haskell-cafe] Re: Shouldn't this loop indefinitely => take (last
gtener at gmail.com
Fri Apr 4 17:36:16 EDT 2008
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'')
> 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.
More information about the Haskell-Cafe