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