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

[Jeremy Shaw]

Hello,

Sadly, as others have pointed out, [0..] is not an infinite list in
that context, so nothing too exciting is happening. You can making
something almost exciting happen if you define some Peano numbers:

> data P = Z | S P

> inf = S Z

[bunch of class instances skipped]

> main = print $ genericTake (inf :: P) [0..]

you still can not get output from:

> main = print $ genericTake (last [0..] :: P) [0..]  -- wont produce output

because the compiler won't recognize that (last [0..]) is equalivent
to 'inf'. You could add a rewrite rule which turned:

 last [0..] -> inf

however, I think that would be a bit bogus, because, in Haskell, the
value returned isn't really the same:

 last [0..] === _|_
 inf = S S S S S S S S S ...

I think this is a bit of an interesting case to consider. As
proponents of declarative programming, we often talk about how
declarative languages free you from having to tell the machine how to
do everything (as compared to imperative languages). So, I think it is
interesting to note that even in declarative languages, there is a
still a degree of describing how to do a computation.

I wonder if there are any dependently types languages where:

  last [0..] === inf

Assuming that statement is true, of course. It seems like it ought to
be provable, but my proof skills are weak. (I suppose in a strict
language, you might consider them to both be _|_, but that is the less
exciting case).

j.

ps. I have attached a working demo. I did not finish all the instance
declarations, only enough to run the example.

-------------- next part --------------
import Data.List

main = do -- print $ genericTake (last [0..] :: P) [0..]  -- wont produce output
          print $ genericTake (inf :: P) [0..]  -- will produce output

inf :: P
inf = S inf

data P = Z | S P

instance Show P where
    show Z = "Z"
    show (S n) = "S " ++ show n

instance Enum P where
    toEnum 0 = Z
    toEnum n = S (toEnum (n - 1))
    fromEnum Z = 0
    fromEnum (S p) = 1 + (fromEnum p)

instance Ord P where
    (S x) > Z = True
    Z > Z = False
    (S x) > (S y) = x > y
    Z <= _ = True
    _ <= Z = False
    (S x) <= (S y) = x <= y

instance Eq P where
    Z == Z         = True
    (S x) == Z     = False
    x == (S y)     = False
    (S x) == (S y) = x == y
    

instance Num P where
    Z + y = Z
    (S x) + y = S (x + y)
    x - Z = x
    Z - _ = error "negative numbers not supported."
    (S x) - (S y) = x - y
    fromInteger n | n < 0 = error "negative numbers not supported."
    fromInteger 0 = Z
    fromInteger n = S (fromInteger (n - 1))

instance Real P
instance Integral P where
-------------- next part --------------


At Thu, 3 Apr 2008 22:27:17 +0100,
Olivier Boudry wrote:
> 
> [1  <multipart/alternative (7bit)>]
> [1.1  <text/plain; UTF-8 (7bit)>]
> Hi all,
> 
> If you compile and run this:
> 
>     main = do
>       putStrLn $ show $ take (last [0..]) [0..]
> 
> or simply run:
> 
>     take (last [0..]) [0..]
> 
> in ghci, it first hang for about one minute and then starts to generate an
> infinite list. I was expecting "last [0..]" to never produce a value and the
> "take" function to never take from the [0..] list.
> 
> I found that line of code in a friend's "Skype Message", lauched it in ghci
> and forgot it. When I came back to my ghci window a couple minutes later it
> was listing numbers, which was really unexpected.
> 
> If I just run "last [0..]" it doesn't return a value and my computer will
> quickly start to paginate to death. Am I missing something? Some laziness
> magic? Rewrite rules?
> 
> Thanks,
> 
> Olivier.
> [1.2  <text/html; UTF-8 (7bit)>]
> 
> [2  <text/plain; us-ascii (7bit)>]
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe