simonmar at microsoft.com
Wed Apr 5 05:01:42 EDT 2006
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.
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
The only thing you can do with non-functions is put them in the sin bin:
deepSeq :: a -> IO ()
More information about the Haskell-prime