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

[Neil Mitchell]

Hi

>  > >  I meant:
>  >  >  (\x (y :: Int) -> x + 1) 1 (1/0 :: Int) <=> _|_ ?
>  >
>  >  Division by 0 is still an error. What I mean is:
>
>  Yes, but this particular one need not be performed. Will it be?

Oh, sorry, I misread that. Even with current Haskell's Int's that is
lazy enough to work, and won't crash.

>  >  Where length xs = 1 and ys = 1000. This takes 1000 steps to tell the
>  >  Int's aren't equal, since we don't have proper lazy naturals. If we
>  >  did, it would take 2 steps.
>
>  Err, really? I mean, could we calculate this equality without reducing
>  length ys to weak head normal form (and then to plain normal form)?

Not without lazy naturals, or some other way of returning the result
of length lazily.

>  What do you mean by "proper Lazy naturals"? Peano ones?

Yes

Thanks

Neil