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

[Lennart Augustsson]

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 <ryani.spam at gmail.com> 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 <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
> >
> >
>
> _______________________________________________
> 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/9d037304/attachment.htm