[Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jul 10 23:50:06 CEST 2013
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/
More information about the Haskell-Cafe
mailing list