deeqSeq proposal

Simon Marlow simonmar at
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.
> 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

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 mailing list