Re: [Haskell-cafe] Why is this strict in its arguments?

I don't even understand what your notation means. But apart from that, there are good reasons to define strictness denotationally instead of operationally. Remember that _|_ is not only exceptions, but also non-termination. For instance, the following function is strict without using its argument: f x = f x because f _|_ = _|_ -- Lennart On Dec 4, 2007 11:07 PM, Ryan Ingram wrote:

Is there a reason why strictness is defined as

...

f _|_ = _|_

instead of, for example,

...

forall x :: Exception. f (throw x) = throw x where an exception thrown from pure code is observable in IO.

In the second case we need to prove that the argument is evaluated at some point, which is also equivalent to the halting problem but more captures the notion of "f evaluates its argument" rather than "either f evaluates its argument, or f _ is _|_"

I suppose the first case allows us to do more eager evaluation; but are there a lot of cases where that matters?

-- ryan

On 12/4/07, Stefan O'Rear wrote:

...

...

Hello all,

As you might have possibly read in some previous blog posts: http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=10 http://users.ecs.soton.ac.uk/pocm06r/fpsig/?p=11

we (the FPSIG group) defined: data BTree a = Leaf a | Branch (BTree a) a (BTree a)

and a function that returns a list of all the paths (which are lists of node values) where each path element makes the predicate true. findAllPath :: (a -> Bool) -> (BTree a) -> Maybe [[a]] findAllPath pred (Leaf l) | pred l = Just [[l]] | otherwise = Nothing findAllPath pred (Branch lf r rt) | pred r = let lfpaths = findAllPath

On Tue, Dec 04, 2007 at 09:41:36PM +0000, Paulo J. Matos wrote: pred lf

...

rtpaths = findAllPath

pred rt

...

in if isNothing lfpaths && isNothing rtpaths then Nothing else if isNothing

lfpaths

...

then Just (map (r:) $ fromJust rtpaths) else if isNothing

rtpaths

...

then Just (map (r:) $ fromJust lfpaths) else Just (map (r:) $ fromJust rtpaths ++ fromJust lfpaths) | otherwise = Nothing

Later on we noticed that this could be simply written as: findAllPath :: (a -> Bool) -> (BTree a) -> [[a]] findAllPath pred = g where g (Leaf l) | pred l = [[l]] g (Branch lf r rt) | pred r = map (r:) $ (findAllPath pred lf) ++ (findAllPath pred rt) g _ = []

without even using maybe. However, 2 questions remained: 1 - why is the first version strict in its arguments?

Because of the definition of strictness. A function is strict iff f undefined = undefined.

findAllPath pred undefined -> undefined because of the case analysis findAllPath undefined (Leaf _) -> undefined because pred is applied in the guard findAllPath undefined Branch{} -> undefined because pred is applied in the guard

...

2 - if it really is strict in its arguments, is there any automated way to know when a function is strict in its arguments?

No, because this is in general equivalent to the halting problem:

f _ = head [ i | i <- [1,3.], i == sum [ k | k <- [1..i-1], i `mod` k == 0 ] ]

f is strict iff there do not exist odd perfect numbers.

However, fairly good conservative approximations exist, for instance in the GHC optimizer - compile your code with -ddump-simpl to see (among other things) a dump of the strictness properties determined. (use -O, of course)

Stefan

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux)

iD8DBQFHVc/eFBz7OZ2P+dIRAmJKAKCDPQl1P5nYNPBOoR6isw9rAg5XowCgwI1s 02/+pzXto1YRiXSSslZsmjk= =7dDj -----END PGP SIGNATURE-----

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe