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

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 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 <<loop>>ing code.

Greets, Ertugrul

-- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/