deeqSeq proposal

[Andy Adams-Moran]

Simon Marlow wrote:
> 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.

Yes, quite right.  In the standard denotational semantics, we can't even
express deepSeq (the fact that it's not monotonic is a consequence, or a
cause, depending on your PoV :-).  If the semantics of Haskell was
sensitive to sharing, and could distinguish between terms depending upon
their level of sharing (probably not a desirable feature of a Haskell
semantics), then deepSeq would be expressible and probably legit.

The above example points to the fact that we don't won't to allow
speculative use of deepSeq.  However, if the program is hyperstrict in a
term (i.e., demands all parts of the term, like all of the cases wherre
Andy wants to use it), then it's safe to use deepSeq ahead of demand.

Thus deepSeq begins to sound a little like unsafePerformIO: it's okay to
use when you satisfy certain pre-conditions.  At least we're able to
/specify/ the pre-conditions for deepSeq :-)

> The only thing you can do with non-functions is put them in the sin bin:
> 
>   deepSeq :: a -> IO ()

unsafeDeepSeq?

I guess we don't want to expand the unsafe* vocabulary for Haskell'
though ...

A

-- 
Andy Adams-Moran                             Phone: 503.626.6616, x113
Galois Connections Inc.                              Fax: 503.350.0833
12725 SW Millikan Way, Suite #290                http://www.galois.com
Beaverton, OR 97005                             adams-moran at galois.com