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

[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 <donn at 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 <<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 at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/