[TYPES] normalization and programming languages

[François-Régis Sinot]

On second thought, I think  it is clearer to split Gérard's original
question in two:

1. Is strong normalization useful for programming languages ?
2. Is the proof of SN via type systems applicable for programming
languages ?

In my previous email, I have addressed question 2 (by saying: "not
directly, but I don't really know"), but then I realized that I have a
much more direct contribution to make to question 1.

Indeed strong normalization is useful if you want to be able to choose
an arbitrary strategy without endangering normalization. Why would you
care to do that ? The only reason I see is *efficiency*, but I think
it's indeed a critical issue, in particular for languages which care
about normalization (as shown in the 2005 GHC survey:
http://haskell.org/ghc/survey2005-summary.html ).

For instance, you could perform call-by-value instead of call-by-name,
locally, on a term known to be SN. But you can do even better: you can
safely perform so-called "closed reduction", see
http://www.lix.polytechnique.fr/~frs/papers/sinot-mscs04-cr.ps.gz
(benchmarks on page 37). This strategy uses the fact that on a SN term,
there is no danger in reducing *under* lambdas (1). I agree that this
implies a big change in the mental representation we have of
abstractions, but I claim that, in some cases, it may be worth the
effort, and this claim is supported by the benchmarks.

Now for this, is it really crucial to know that our term is SN ? I would
say that if we don't, we may always try as if, and fall back to the
default case if we fail, following the idea of optimistic evaluation: 
http://research.microsoft.com/Users/simonpj/Papers/optimistic/ 
The results of optimistic evaluation combining call-by-value and
call-by-need are encouraging, why wouldn't they be as well with closed
reduction ? (Future might tell.)

Best wishes,
F-R Sinot.


---
A clarifying remark, but out of the scope of the present discussion:

(1) But note that, somehow counter-intuitively, *not all* reductions are
good to be performed. For instance, reducing the argument to full normal
form before a beta-reduction is *not* a good strategy (this is CBVNF in
the benchmarks p. 37). This makes the issue raised by this paper
considerably less trivial, I think.