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

[Ryan Ingram]

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 <stefanor at cox.net> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071204/94eafb4c/attachment.htm