[Haskell-cafe] GHC bug? Let with guards loops

[Andreas Abel]

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/