Andreas Abel | 9 Jul 16:42 2013
Picon

GHC bug? Let with guards loops

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...

Cheers,
Andreas

--

-- 
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/
(Continue reading)

Dan Doel | 9 Jul 17:05 2013
Picon

Re: GHC bug? Let with guards loops

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 Tue, Jul 9, 2013 at 10:42 AM, Andreas Abel <andreas.abel <at> ifi.lmu.de> wrote:
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...

Cheers,
Andreas

--
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/

_______________________________________________
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
Roman Cheplyaka | 9 Jul 17:49 2013

Re: GHC bug? Let with guards loops

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> [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...
> 
> Cheers,
> Andreas
> 
> -- 
> 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/
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
Andreas Abel | 9 Jul 19:12 2013
Picon

Re: GHC bug? Let with guards loops

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> [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...
>>
>> Cheers,
>> Andreas
>>
>> --
>> 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/
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--

-- 
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/
Felipe Almeida Lessa | 9 Jul 19:23 2013
Picon

Re: GHC bug? Let with guards loops

Well, you could use p's type for something.

  let x | foo (undefined `asTypeOf` x) = 3
      foo _ = True
  in x

Arguably not very useful.  It seems to me that the most compelling
rationale is being consistent with the cases where, instead of being a
data type, p is a function.  Even so most of the time you won't be
recursing on the guard.  But, since you could use something from the
where clause on the guard, and we certainly won't be restricting
recursing on the where clause, it also seems compelling to allow
recursion on the guard.

My 2 centavos, =)

On Tue, Jul 9, 2013 at 2:12 PM, Andreas Abel <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> [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...
>>>
>>> Cheers,
>>> Andreas
>>>
>>> --
>>> 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/
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe <at> haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
>
> --
> 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/
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

--

-- 
Felipe.
Andreas Abel | 9 Jul 19:57 2013
Picon

Re: GHC bug? Let with guards loops

Hi Felipe,  thanks for the centavos.

So you mean that in

   let p | g = e where bs
   in ...

the bindings bs should be in scope in g (and of course the variables of 
p are in scope in bs).  Mmh, the bindings in bs that do not uses the 
pattern variables could be useful in g, but the other bindings will 
still lead to non-termination.  Maybe such an analysis is too 
sophisticated.  My lesson is to use case instead of let.  Only that the 
let syntax is nicer and indentation-friendlier than case, so it would be 
preferable.

The greater evil is that Haskell does not have a non-recursive let. 
This is source of many non-termination bugs, including this one here. 
let should be non-recursive by default, and for recursion we could have 
the good old "let rec".

Cheers,
Andreas

On 09.07.2013 19:23, Felipe Almeida Lessa wrote:
> Well, you could use p's type for something.
>
>    let x | foo (undefined `asTypeOf` x) = 3
>        foo _ = True
>    in x
>
> Arguably not very useful.  It seems to me that the most compelling
> rationale is being consistent with the cases where, instead of being a
> data type, p is a function.  Even so most of the time you won't be
> recursing on the guard.  But, since you could use something from the
> where clause on the guard, and we certainly won't be restricting
> recursing on the where clause, it also seems compelling to allow
> recursion on the guard.
>
> My 2 centavos, =)
>
>
> On Tue, Jul 9, 2013 at 2:12 PM, Andreas Abel <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> [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/
Dan Doel | 9 Jul 19:56 2013
Picon

Re: GHC bug? Let with guards loops

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?

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?

Also, it might have some weird consequences for moving code around. Like:

    let Just x | x > 0 = Just 1

    let Just x | y > 0 = Just 1
        y = x

    let Just x | b = Just 1
          where b = x > 0

    let Just x | b = Just 1
        b = x > 0

These all behave the same way now. Which ones should change?

If Haskell had a non-recursive let, that'd probably be a different story. But it doesn't.



On Tue, Jul 9, 2013 at 1:12 PM, Andreas Abel <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> [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...

Cheers,
Andreas

--
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/

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



--
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/

_______________________________________________
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
Andreas Abel | 9 Jul 20:16 2013
Picon

Re: GHC bug? Let with guards loops

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/

Gmane