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