### Re: GHC bug? Let with guards loops

Andreas Abel <andreas.abel <at> ifi.lmu.de>

2013-07-09 18:16:10 GMT

On 09.07.2013 19:56, Dan Doel wrote:
> With pattern guards, it's difficult to say whether it is never 'useful'
> to have things like the following work:
>
> C x | C' y z <- f x = ...
>
> But I'd also shy away from changing the behavior because it causes a lot
> of consistency issues. In
>
> let
> f <vs1> | gs1 = es1
> h <vs2> | gs2 = es2
> ...
>
> we have that f and h are in scope in both gs1 and gs2. Does it make
> sense to call f in gs1? It's easy to loop if you do. So should f not be
> in scope in gs1, but h is, and vice versa for gs2? But they're both in
> scope for es1 and es2?
If f and h are really mutually recursive, then they should not be in
scope in gs1 and gs2.
If the first thing you do in the body of f is calling f (which happens
if f appears in gs1), then you are bound to loop. But of course, if vs
are not just variables but patterns, then the first thing you do is
matching, so using f in gs1 could be fine.
I am getting on muddy grounds here, better retreat. I was thinking only
of non-recursive let.
In the report
http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-440003.12
it says that
let p = e1 in e0 = case e1 of ~p -> e0
where no variable in p appears free in e1
but this applies only for patterns p without guards, and I would have
expected to be true also for patterns with guards.
> And if we leave the above alone, then what about the case where there
> are no <vs>? Is that different? Or is it only left-hand patterns that
> get this treatment?
Yes, it is only about the things defined by the let binding (in this
case, f and g). The variables in vs1 are bound by calling f, but by f's
body.
> Also, it might have some weird consequences for moving code around. Like:
>
> let Just x | x > 0 = Just 1
Non-recursive.
> let Just x | y > 0 = Just 1
> y = x
Recursive.
> let Just x | b = Just 1
> where b = x > 0
Recursive?
> let Just x | b = Just 1
> b = x > 0
Recursive. (Like 2.)
> These all behave the same way now. Which ones should change?
Only the first one? Hard to tell.
> If Haskell had a non-recursive let, that'd probably be a different
> story. But it doesn't.
Definitely agree.
> On Tue, Jul 9, 2013 at 1:12 PM, Andreas Abel <andreas.abel <at> ifi.lmu.de
> <mailto:andreas.abel <at> ifi.lmu.de>> wrote:
>
> Thanks, Dan and Roman, for the explanation. So I have to delete the
> explanation "non-recursive let = single-branch case" from my brain.
>
> I thought the guards in a let are assertations, but in fact it is
> more like an if. Ok.
>
> But then I do not see why the pattern variables are in scope in the
> guards in
>
> let p | g = e
>
> The variables in p are only bound to their values (given by e) if
> the guard g evaluates to True. But how can g evaluate if it has yet
> unbound variables? How can ever a pattern variable of p be ***needed***
> to compute the value of the guard? My conjecture is that it cannot,
> so it does not make sense to consider variables of g bound by p.
> Maybe you can cook up some counterexample.
>
> I think the pattern variables of p should not be in scope in g, and
> shadowing free variables of g by pattern variables of p should be
> forbidden.
>
> Cheers,
> Andreas
>
> On 09.07.2013 17:05, Dan Doel wrote:> The definition
>
> >
> > Just x | x > 0 = Just 1
> >
> > is recursive. It conditionally defines Just x as Just 1 when x >
> 0 (and
> > as bottom otherwise). So it must know the result before it can
> test the
> > guard, but it cannot know the result until the guard is tested.
> Consider
> > an augmented definition:
> >
> > Just x | x > 0 = Just 1
> > | x <= 0 = Just 0
> >
> > What is x?
>
> On 09.07.2013 17:49, Roman Cheplyaka wrote:
>
> As Dan said, this behaviour is correct.
>
> The confusing thing here is that in case expressions guards are
> attached
> to the patterns (i.e. to the lhs), while in let expressions they are
> attached to the rhs.
>
> So, despite the common "Just x | x > 0" part, your examples mean
> rather
> different things.
>
> Here's the translation of 'loops' according to the Report:
>
> loops =
> let Just x =
> case () of
> () | x > 0 -> Just 1
> in x
>
> Here it's obvious that 'x' is used in the rhs of its own definition.
>
> Roman
>
> * Andreas Abel <andreas.abel <at> ifi.lmu.de
> <mailto:andreas.abel <at> ifi.lmu.de>> [2013-07-09 16:42:00+0200]
>
> Hi, is this a known bug or feature of GHC (7.4.1, 7.6.3)?:
>
> I got a looping behavior in one of my programs and could not
> explain
> why. When I rewrote an irrefutable let with guards to use a
> case
> instead, the loop disappeared. Cut-down:
>
> works = case Just 1 of { Just x | x > 0 -> x }
>
> loops = let Just x | x > 0 = Just 1 in x
>
> works returns 1, loops loops. If x is unused on the rhs, the
> non-termination disappears.
>
> works' = let Just x | x > 0 = Just 1 in 42
>
> Is this intended by the Haskell semantics or is this a bug?
> I would
> have assumed that non-recursive let and single-branch case are
> interchangeable, but apparently, not...
>
--
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel <at> ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/