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
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@galois.com
Andy Adams-Moran wrote:
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 ...
What's wrong with deepSeeqIO :: a -> IO () ? Then you can use unsafePerformIO if you want deepSeq :: a -> b -> b -- Lennart
Lennart Augustsson wrote:
Andy Adams-Moran wrote:
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 ...
What's wrong with deepSeeqIO :: a -> IO () ? Then you can use unsafePerformIO if you want deepSeq :: a -> b -> b
Yes, quite right! In the case of deepSeqIO, we do know precisely what the safety condition is (as opposed to generic uses of unsafePerformIO and its cousins), so maybe we want to call that out somehow. 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@galois.com
Am Freitag, 7. April 2006 00:40 schrieb Andy Adams-Moran:
Lennart Augustsson wrote:
Andy Adams-Moran wrote:
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 ...
What's wrong with deepSeeqIO :: a -> IO () ? Then you can use unsafePerformIO if you want deepSeq :: a -> b -> b
Yes, quite right! In the case of deepSeqIO, we do know precisely what the safety condition is (as opposed to generic uses of unsafePerformIO and its cousins), so maybe we want to call that out somehow.
A
And maybe we should switch from seq to seqIO :: a -> IO ()? Best wishes, Wolfgang
participants (4)
-
Andy Adams-Moran -
Lennart Augustsson -
Simon Marlow -
Wolfgang Jeltsch