On 04 April 2006 19:53, Andy Adams-Moran wrote:
Andy Gill wrote:
let xs' () = 1 : 2 : xs' () let xs2 = xs'
let xs = 1 : 2 : xs
So deepSeq xs2 ==> _|_, but deepSeq xs ==> xs
Yes, and hence deepSeq isn't monotonic. That's bad.
I appeal to the "morally correct reasoning" argument .. If the program terminates, then it is still correct. The deepSeq is an assertion about the ability to represent the result in finite space.
I'm not convinced Simon's argument holds, as I don't think you can use deepSeq to write a Haskell function that will distinguish cyclic structures from infinite ones. If we can't do that, then we haven't really added any new semantic observational capability to the theory, so I think the "morally correct reasoning" argument holds.
Simon?
I think we should be able to rely on a bit more than "moral correctness" :-) Imagine writing a denotational semantics for deepSeq: you can't without talking about representations, and we don't want to talk about representations in denotational semantics, or in the Haskell language definition. The only thing you can do with non-functions is put them in the sin bin: deepSeq :: a -> IO () Cheers, Simon