Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Donn Cave
quoth Alberto G. Corona,

 Let is recursive because, unlike in the case of other
 languages, variables are not locations for storing values, but the
 expressions on the right side of the equality themselves. And obviously it
 is not possible for a variable-expression to be two expressions at the same
 time. The recursiveness is buildt-in. It comes from its pure nature.

I'm surprised that it would come down to purity.  It looks to me like
simply a question of scope.  I had to write an example program to see
what actually happens, because with me it isn't intuitive at all that
the name bound to an expression would be visible from within the
expression itself.  I suppose this is considered by some to be a feature,
obviously to others it's a bug.

I've gone to some trouble to dig up an nhc98 install (but can't seem to
find one among my computers and GHC 7 won't build the source thanks to
library re-orgs etc.)  Because, I vaguely recall that nhc98's rules
were different here?  Anyone in a position to prove me wrong?

thanks,
Donn

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Ertugrul Söylemez
Donn Cave d...@avvanta.com wrote:

  Let is recursive because, unlike in the case of other languages,
  variables are not locations for storing values, but the expressions
  on the right side of the equality themselves. And obviously it is
  not possible for a variable-expression to be two expressions at the
  same time. The recursiveness is buildt-in. It comes from its pure
  nature.

 I'm surprised that it would come down to purity.  It looks to me like
 simply a question of scope.  I had to write an example program to see
 what actually happens, because with me it isn't intuitive at all
 that the name bound to an expression would be visible from within
 the expression itself.  I suppose this is considered by some to be a
 feature, obviously to others it's a bug.

In a non-strict-by-default language like Haskell it's certainly a
feature.  A sufficiently smart compiler can figure out whether a
definition is recursive or not and apply the proper transformation, so
from a language-theoretic standpoint there is really no reason to have a
non-recursive let.

I think the proper solution is to identify the underlying problem:
general recursion.  Haskell does not enforce totality.  I'd really love
to see some optional totality checking in Haskell.  If Oleg decides not
to use a state monad, he will still have to be careful not to confuse
the numbers, but if he does, then the compiler will reject his code
instead of producing looping code.


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.


signature.asc
Description: PGP signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Andreas Abel

Totality checking will generate a lot of false positives.

One would like an analysis that prints an error message if an expression 
is *definitely* looping in all cases.  While I have studied termination, 
I have not studied non-termination analyses.  It is harder than 
termination.  For termination checking, you can over-approximate the 
control-flows and just scream if you find a *potential* control flow 
that *might* lead to non-termination.  If you do not find such a control 
flow you can be sure things are terminating.  This is how Agda does it.


To be sure that something is definitely non-terminating, you need to 
show it is non-terminating on all *actual* control flows.  But usually 
you cannot statically tell whether in if c then d else e d or e is 
evaluated, so a non-termination analysis without false positives seems 
very restricted.  Still it might be could useful.


Having said this, having a termination analysis is not the proper 
solution to the lack of a non-recursive let, it does not establish 
shadowing behavior I want.


Cheers,
Andreas

On 10.07.13 7:44 PM, Ertugrul Söylemez wrote:

Donn Cave d...@avvanta.com wrote:


Let is recursive because, unlike in the case of other languages,
variables are not locations for storing values, but the expressions
on the right side of the equality themselves. And obviously it is
not possible for a variable-expression to be two expressions at the
same time. The recursiveness is buildt-in. It comes from its pure
nature.


I'm surprised that it would come down to purity.  It looks to me like
simply a question of scope.  I had to write an example program to see
what actually happens, because with me it isn't intuitive at all
that the name bound to an expression would be visible from within
the expression itself.  I suppose this is considered by some to be a
feature, obviously to others it's a bug.


In a non-strict-by-default language like Haskell it's certainly a
feature.  A sufficiently smart compiler can figure out whether a
definition is recursive or not and apply the proper transformation, so
from a language-theoretic standpoint there is really no reason to have a
non-recursive let.

I think the proper solution is to identify the underlying problem:
general recursion.  Haskell does not enforce totality.  I'd really love
to see some optional totality checking in Haskell.  If Oleg decides not
to use a state monad, he will still have to be careful not to confuse
the numbers, but if he does, then the compiler will reject his code
instead of producing looping code.


Greets,
Ertugrul



--
Andreas AbelDu bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Andreas Abel

On 10.07.13 6:00 PM, Donn Cave wrote:

quoth Alberto G. Corona,


Let is recursive because, unlike in the case of other
languages, variables are not locations for storing values, but the
expressions on the right side of the equality themselves. And obviously it
is not possible for a variable-expression to be two expressions at the same
time. The recursiveness is buildt-in. It comes from its pure nature.


@Alberto: you must have misunderstood my proposal.


I'm surprised that it would come down to purity.  It looks to me like
simply a question of scope.  I had to write an example program to see
what actually happens, because with me it isn't intuitive at all that
the name bound to an expression would be visible from within the
expression itself.  I suppose this is considered by some to be a feature,
obviously to others it's a bug.


Value-recursion *is* useful in a lazy language, e.g.

  let xs = 0 : xs

builds an infinite (in fact, circular) list of 0s.  But it is not always 
meaningful, e.g.


  let x = x + 1

simply loops.  I would like to be in the position to tell Haskell what I 
mean, whether I want recursion or not.



I've gone to some trouble to dig up an nhc98 install (but can't seem to
find one among my computers and GHC 7 won't build the source thanks to
library re-orgs etc.)  Because, I vaguely recall that nhc98's rules
were different here?  Anyone in a position to prove me wrong?


I would doubt that nhc98 would interpret  let xs = 0 : xs  differently 
than ghc if it implemented anything close to the Haskell 98 standard. 
But I am not in a position to prove you wrong.


Cheers,
Andreas

--
Andreas AbelDu bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Donn Cave
quoth Andreas Abel andreas.a...@ifi.lmu.de,
...
 I would doubt that nhc98 would interpret  let xs = 0 : xs  differently 
 than ghc if it implemented anything close to the Haskell 98 standard. 

What I (so vaguely) remember was a compile error, for some reuse of
an identifier where GHC permitted it.  I suppose you're right, anyway,
probably something else - maybe unambiguous nested shadowing?

  let x = t + 1 in
  let y = x in
  let x = y + 1 in x

GHC allows this, and of course there's no recursion.

Donn

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Richard A. O'Keefe

On 11/07/2013, at 4:00 AM, Donn Cave wrote:
 I've gone to some trouble to dig up an nhc98 install (but can't seem to
 find one among my computers and GHC 7 won't build the source thanks to
 library re-orgs etc.)  Because, I vaguely recall that nhc98's rules
 were different here?  Anyone in a position to prove me wrong?

I have a copy of nhc98 running (v1.16 of 2003-03-08).
Program:

main = let ones = 1 : ones in print $ take 10 $ ones

Output:

[1,1,1,1,1,1,1,1,1,1]

So no, nhc98's rules were _not_ different.
It would have been no use as a Haskell98 compiler if they had been.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]

2013-07-10 Thread Richard A. O'Keefe

On 11/07/2013, at 11:09 AM, Donn Cave wrote:

 let x = t + 1 in
  let y = x in
  let x = y + 1 in x
 

Still no cigar.
nhc98 v1.16
Program:
main = print $ (let t = 0 in let x = t + 1 in let y = x in let x = y + 1 in x)
Output:
2



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe