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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> wrote: > > > On Tue, Dec 04, 2007 at 09:41:36PM +0000, Paulo J. Matos 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 > > 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 > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
