[Agda] [TYPES] Progress + Preservation = Evaluation

[Oleg]

Phil Wadler wrote:
> Progress + Preservation = Evaluation.
> From a constructive proof of progress and preservation, we can assemble a
> constructive evaluator which, for any given number n, will either reduce
> the term to a value (in less than n steps) or show that after n steps of
> reduction the term is not a value. [The key word here is *constructive*.
> Once one has proved progress and preservation constructively, one has
> implemented a constructive evaluator for terms.]

> Indeed, in every presentation I can recall the act of proving progress and
> preservation is separated from the act of writing code that can evaluate a
> term, even though the former trivially implies the latter. 

Sorry for being late to the party...

I can cite quite a few cases where to prove progress and
preservation, one first implements an evaluator -- and the type
soundness comes as a `side-effect' of writing it.  To wit: one writes
an evaluator of the signature (in Twelf terms)
             eval : {E:exp T} non-value E  -> exp T -> type.
The signature expresses subject reduction (preservation) property.
Thus it becomes impossible to write cases of eval that do not
have subject reduction -- the typechecker will complain otherwise. Once we
have finished writing all cases of eval (which can then be used immediately
to evaluate terms) we can ask Twelf if `eval' is total. If Twelf agrees,
we get the proof of progress. This is often called `intrinsic
encoding' of DSLs and has been quite popular in Twelf community. 

The following web page from about 10 years ago

        http://okmij.org/ftp/formalizations/index.html#intrinsic

summarizes this techniques and provides the references I could find. It
also shows several less-trivial progress-preservation proofs done in
this style, in particular, calculus with both staging and delimited
control. The eval function was indeed used in practice, to evaluate
sample terms (and run all the examples that are mentioned in our
papers about that calculus). 

The technique is closely related to `tagless-final', as mentioned on
that web page. Writing a tagless-final evaluator indeed includes
essentially proving subject reduction in the process (even if one
actually is interested in running programs rather than doing proofs).