[Agda] Progress + Preservation = Evaluation

[Philip Wadler]

Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.

Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.

Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.

It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.

Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.

Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.

An Agda implementation of Evaluation provides an evaluator for terms:
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
in my draft textbook:

https:plfa.inf.ed.ac.uk

Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P


. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

[Philip Wadler]

My previous question must not have been clear, since I received two answers
from top-notch researchers that missed my point. My question is not about
progress and preservation or step indexing. My question is about the
following observation:

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

Pierce et al's text Software Foundations presents constructive proofs of
progress and preservation. From these, one may immediately derive an
evaluator for terms. But the text does not do so; instead it presents a
separate normalisation tactic. (To be fair, that tactic is given prior to
the proofs of progress and preservation. Nonetheless, after the proofs are
given there is no observation that they might be applied to replace the
normalisation tactic.) I also could not spot this observation in
Harper's Practical Foundations for Programming Languages.

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. (The one
exception is my new textbook. It's located at plfa.inf.ed.ac.uk --- do have
a look!)

To repeat my questions: What sources in the literature should one cite for
this technique? How well-known is it as folklore? Cheers, -- P



. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Post by Philip Wadler
Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/

[Philip Wadler]

Thanks, Oleg! I agree that renaming "progress" to "eval" corresponds to the
same insight, though expressed differently: instead of observing that
progress and preservation give you evaluation, you are observing that
evaluation gives you progress! Were any of the items listed on your page
published (elsewhere than on the page itself)? Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Post by Philip Wadler
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

Post by Philip Wadler
preservation is separated from the act of writing code that can evaluate

a

Post by Philip Wadler
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).

[Neel Krishnaswami]

Hello,

I wrote the following bit of code, to experiment with generic programming.

data _×_ (A B : Set) : Set where
   _,_ : A → B → A × B
data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B
data Poly : Set₁ where
  K : Set → Poly
  _⊗_ : Poly → Poly → Poly
  _⊕_ : Poly → Poly → Poly
  Id : Poly
[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A
data μ (F : Poly) : Set where
  into : [ F ] (μ F) → μ F

and Agda accepted the declaration of μ. I was surprised by this -- did
Agda look at the body of the definition of [_] to decide that every 
recursive occurrence was  positive? If so, how deeply does it look?

[Jesper Cockx]

I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.

-- Jesper

Post by Neel Krishnaswami
Hello,
I wrote the following bit of code, to experiment with generic programming.

data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B
data Poly : Set₁ where
K : Set → Poly
_⊗_ : Poly → Poly → Poly
_⊕_ : Poly → Poly → Poly
Id : Poly
[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A
data Ό (F : Poly) : Set where
into : [ F ] (ÎŒ F) → ÎŒ F

and Agda accepted the declaration of Ό. I was surprised by this -- did
Agda look at the body of the definition of [_] to decide that every
recursive occurrence was positive? If so, how deeply does it look?
--
Neel Krishnaswami
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Neel Krishnaswami]

Hello,

Is there any way to annotate the type signature with positivity
information? It would be helpful for localizing errors, and for doing
ML-style modular programming.

Thanks for your help!

Post by Jesper Cockx
I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.
-- Jesper

Post by Neel Krishnaswami
Hello,
I wrote the following bit of code, to experiment with generic programming.

data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B
data Poly : Set₁ where
K : Set → Poly
_⊗_ : Poly → Poly → Poly
_⊕_ : Poly → Poly → Poly
Id : Poly
[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A
data μ (F : Poly) : Set where
into : [ F ] (μ F) → μ F

and Agda accepted the declaration of μ. I was surprised by this -- did
Agda look at the body of the definition of [_] to decide that every
recursive occurrence was positive? If so, how deeply does it look?
--
Neel Krishnaswami
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Jesper Cockx]

Currently there is no way to do that, (partly) because positivity
information is not stored in the type of a function. There has been talk of
integrating this into the type system, but it's not clear at the moment how
to do this in a nice way.

One special case are the polarity pragma's that can be used to assign a
given polarity to a postulate, see
https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda.

-- Jesper

Post by Neel Krishnaswami
Hello,
Is there any way to annotate the type signature with positivity
information? It would be helpful for localizing errors, and for doing
ML-style modular programming.
Thanks for your help!

Post by Jesper Cockx
I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.
-- Jesper
Hello,

Post by Neel Krishnaswami
I wrote the following bit of code, to experiment with generic programming.
data _×_ (A B : Set) : Set where

_,_ : A → B → A × B
data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B
data Poly : Set₁ where
K : Set → Poly
_⊗_ : Poly → Poly → Poly
_⊕_ : Poly → Poly → Poly
Id : Poly
[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A
data Ό (F : Poly) : Set where
into : [ F ] (ÎŒ F) → ÎŒ F
and Agda accepted the declaration of Ό. I was surprised by this -- did

Agda look at the body of the definition of [_] to decide that every
recursive occurrence was positive? If so, how deeply does it look?
--
Neel Krishnaswami
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Neel Krishnaswami

[Thorsten Altenkirch]

Hi,

I think there should be an alternative to these ad hoc extensions of the type system (including the size mechanism). In general this corresponds to constructing an internal model of type theory.

Incidentally this is related to a grant proposal (on “Template Type Theory”) I am working on just now.

In this case a strictly positive type can be modelled as a container but the overhead of using containers explicitely makes this unfeasible. However, Tamara von Glehn and others have shown that containers form a model of type theory. Maybe this doesn’t yet give you everything you want but I think this can scaled up to enable us to provide the semantics for the judgement that a type or a family of types occurs strictly positively and hence that we can use it in an inductive (or coinductive) definition.

Hence what we are proposing is to turn the model constructions that justify extensions from paper code into agda code which can be used to implement these extensions safely. And using (and extending) type theory in type theory developed with Ambrus Kaposi we have a good handle to talk about type theory internally.

Having said this I am very much in favour of experimentation now but I think in the long run we have to think how to reign in the wild growth of extensions and modifications of type theory.

Thorsten


From: Agda <agda-***@lists.chalmers.se> on behalf of Jesper Cockx <***@sikanda.be>
Date: Friday, 20 July 2018 at 13:37
To: Neel Krishnaswami <***@cl.cam.ac.uk>
Cc: agda list <***@lists.chalmers.se>
Subject: Re: [Agda] Why does this pass the positivity checker?

Currently there is no way to do that, (partly) because positivity information is not stored in the type of a function. There has been talk of integrating this into the type system, but it's not clear at the moment how to do this in a nice way.

One special case are the polarity pragma's that can be used to assign a given polarity to a postulate, see https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda.

-- Jesper

On Fri, Jul 20, 2018 at 2:24 PM, Neel Krishnaswami <***@cl.cam.ac.uk<mailto:***@cl.cam.ac.uk>> wrote:
Hello,

Is there any way to annotate the type signature with positivity information? It would be helpful for localizing errors, and for doing ML-style modular programming.

Thanks for your help!



On 20/07/18 13:06, Jesper Cockx wrote:
I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.

-- Jesper

On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <***@cl.cam.ac.uk<mailto:***@cl.cam.ac.uk>>
wrote:
Hello,

I wrote the following bit of code, to experiment with generic programming.
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B


data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B


data Poly : Set₁ where
K : Set → Poly
_⊗_ : Poly → Poly → Poly
_⊕_ : Poly → Poly → Poly
Id : Poly

[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A

data Ό (F : Poly) : Set where
into : [ F ] (ÎŒ F) → ÎŒ F
and Agda accepted the declaration of Ό. I was surprised by this -- did
Agda look at the body of the definition of [_] to decide that every
recursive occurrence was positive? If so, how deeply does it look?
--
Neel Krishnaswami
***@cl.cam.ac.uk<mailto:***@cl.cam.ac.uk>

_______________________________________________
Agda mailing list
***@lists.chalmers.se<mailto:***@lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda
--
Neel Krishnaswami
***@cl.cam.ac.uk<mailto:***@cl.cam.ac.uk>




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

[Philip Wadler]

Thanks, Pierre and Eelco. I'm well aware of "fuel" as folklore. For
instance, I've heard Conor McBride describe fuel as an argument that,
despite the guarantee that all programs terminate, Agda can effectively
encode every recursive function. But that is different from my question;
please see my second, clarifying email. I had a look at the three
references cited, and I don't believe they exploit constructive proofs of
progress and preservation to define an evaluator. Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Hi,
I think this is now well known as the "fuel" pattern. Ideally n is
very big and computed lazily.
I am not aware of a paper specifically about this trick, it is there
as a very useful folklore I guess.
Note however that Bertot Balaa presented a more "complete" version of
this by refining this trick: the function itself is defined by means
of a proof that there exists a number N of iterations such that any
greater number would give the same result. i.e. that N is a sufficient
fuel to reach the fixpoint. This mechanism is used in the current
implementation of the "Function" command in coq (when given a non
structurally recursive function).
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.
28.601&rep=rep1&type=pdf
Best,
Pierre

[ The Types Forum, http://lists.seas.upenn.edu/

mailman/listinfo/types-list ]

Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Andreas Abel]

Dear Phil,

to me, deriving an evaluator from preservation & progress resembles a
use of the

trampoline : (A -> B + A) -> A -> Delay B

where A would be "well-typed terms" and B "values".

Delay is the coinductive type with coconstructors

now : B -> Delay B
later : Delay B -> Delay B

trampoline is the coiteration principle for Delay.

For Delay, see Venanzio Capretta.

https://doi.org/10.2168/LMCS-1(2:1)2005

I don't have a reference for your specific problem.

Best,
Andreas

Post by Philip Wadler
Thanks, Pierre and Eelco. I'm well aware of "fuel" as folklore. For
instance, I've heard Conor McBride describe fuel as an argument that,
despite the guarantee that all programs terminate, Agda can effectively
encode every recursive function. But that is different from my question;
please see my second, clarifying email. I had a look at the three
references cited, and I don't believe they exploit constructive proofs
of progress and preservation to define an evaluator. Cheers, -- P
.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
Hi,
I think this is now well known as the "fuel" pattern. Ideally n is
very big and computed lazily.
I am not aware of a paper specifically about this trick, it is there
as a very useful folklore I guess.
Note however that Bertot Balaa presented a more "complete" version of
this by refining this trick: the function itself is defined by means
of a proof that there exists a number N of iterations such that any
greater number would give the same result. i.e. that N is a sufficient
fuel to reach the fixpoint. This mechanism is used in the current
implementation of the "Function" command in coq (when given a non
structurally recursive function).
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.601&rep=rep1&type=pdf
<http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.601&rep=rep1&type=pdf>
Best,
Pierre

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list

<http://lists.seas.upenn.edu/mailman/listinfo/types-list> ]

Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus.  Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
   Progress.  If ∅ ⊢ M : A then either M is a value or M —→ N,
   for some term N.
   Preservation.  If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
   Evaluation.  If ∅ ⊢ M : A, then for every natural number n,
   either M —↠ V, where V is a value and the reduction sequence
   has no more than n steps, or M —↠ N, where N is not a value
   and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation,

stopping

early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead).  I have used it
   https:plfa.inf.ed.ac.uk <http://plfa.inf.ed.ac.uk>
Questions: What sources in the literature should one cite for this
technique?  How well-known is it as folklore? Cheers, -- P
.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

<http://homepages.inf.ed.ac.uk/wadler/>

Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Thanks, Sam and Andreas, for the elegant examples of how to encode general
recursion in a language that guarantees termination. Sam, am I right in
thinking Conor's paper does not touch on the idea of combining constructive
proofs of progress and preservation to derive a constructive evaluator?
(But I could apply Conor's technique or a trampoline to express such an
evaluator. Indeed, I considered using Delay for the evaluator in the
textbook, but decided that supplying a step count was simpler, and avoided
the need to explain coinduction.) Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

You should certainly cite Conor McBride's MPC 2015 paper
https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf
Sam

[ The Types Forum, http://lists.seas.upenn.edu/ma
ilman/listinfo/types-list ]
Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Roman]

avoided the need to explain coinduction

Conor uses a constructive free monad. So coinduction is just one
interpretation and you can avoid it and present only the fuel-driven
execution semantics. Though, if it's the only one you need, why
complicate it by using free monads indeed.

There is a very remotely related topic to what you're asking, it's
called Normalization by Completeness. Here are some slides: [1]. In
essence, you can get normalization by composing Soundness with
Completeness which is kinda related, because Progress and Preservation
are forms of Soundness and Completeness (I always forget which one is
which). But there Soundness means Evaluation (to a value in some
model) and Completeness means Reification, so I'm not really sure
whether there is any relation at all.

[1] http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf

Best regards,
Roman

[Nils Anders Danielsson]

Indeed, I considered using Delay for the evaluator in the textbook,
but decided that supplying a step count was simpler, and avoided the
need to explain coinduction.

In "Operational Semantics Using the Partiality Monad"
(https://doi.org/10.1145/2364527.2364546) I defined the semantics of an
untyped language by giving a definitional interpreter, using the delay
monad. Then I proved type soundness for this language as a negative
statement (using a more positive lemma):

[] ⊢ t ∈ σ → ¬ (⟦ t ⟧ [] ≈ fail)

Thus, instead of starting with type soundness and deriving an evaluator,
I started with an evaluator and proved type soundness.

This kind of exercise has also been performed using fuel, see Siek's
"Type Safety in Three Easy Lemmas"
(http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html)
and "Functional Big-Step Semantics" by Owens et al.
(https://doi.org/10.1007/978-3-662-49498-1_23).

[Philip Wadler]

Thanks! I've saved your notes to review before revising the paper.

In "Functional Big-Step Semantics", one of the advantages is that one
immediately obtains an evaluator for terms. They note that sometimes a
small-step semantics also immediately gives an evaluator for terms, and
cite K and Redex as examples---suggesting, again, a lack of recognition
that any constructive proof of progress and preservation immediately gives
rise to an evaluator.

Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Post by Nils Anders Danielsson

Indeed, I considered using Delay for the evaluator in the textbook,
but decided that supplying a step count was simpler, and avoided the
need to explain coinduction.

In "Operational Semantics Using the Partiality Monad"
(https://doi.org/10.1145/2364527.2364546) I defined the semantics of an
untyped language by giving a definitional interpreter, using the delay
monad. Then I proved type soundness for this language as a negative
[] ⊢ t ∈ σ → ¬ (⟩ t ⟧ [] ≈ fail)
Thus, instead of starting with type soundness and deriving an evaluator,
I started with an evaluator and proved type soundness.
This kind of exercise has also been performed using fuel, see Siek's
"Type Safety in Three Easy Lemmas"
(http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html)
and "Functional Big-Step Semantics" by Owens et al.
(https://doi.org/10.1007/978-3-662-49498-1_23).
--
/NAD

[William J. Bowman]

I think the canonical reference for this is Wright Felleisen 1994, https://doi.org/10.1006/inco.1994.1093. They have a history in the introduction showing many prior versions, although most don't talk about evaluation directly.

They call "evaluation" "type soundess", in various forms, where the evaluation
function reprenents the ground truth semantics for the language, and the type
system is a syntactic proof system.
"Type soundness" is meant to indicate that the syntactic semantics (proof) is
sound w.r.t. evaluation semantics (truth).

--
William J. Bowman

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Eelco Visser]

Hi Phil,

The idea of using fuel to model non-termination is pretty well known
and at least used in the following recent papers:

Type Soundness Proofs with Definitional Interpreters. Amin, Rompf
https://popl17.sigplan.org/event/popl-2017-papers-from-f-to-dot-type-soundness-proofs-with-definitional-interpreters

Intrinsically-Typed Definitional Interpreters for Imperative
Languages. Bach Poulsen, Rouvoet, Tolmach, Krebbers, Visser.
https://popl18.sigplan.org/event/popl-2018-papers-intrinsically-typed-definitional-interpreters-for-imperative-languages

See the related work of the latter for more references.

Note that the latter paper uses Agda as well.

cheers,

-- Eelco

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Eelco Visser]

Hi Phil,

The idea of using fuel to model non-termination is pretty well known
and at least used in the following recent papers:

Type Soundness Proofs with Definitional Interpreters. Amin, Rompf
https://popl17.sigplan.org/event/popl-2017-papers-from-f-to-dot-type-soundness-proofs-with-definitional-interpreters

Intrinsically-Typed Definitional Interpreters for Imperative
Languages. Bach Poulsen, Rouvoet, Tolmach, Krebbers, Visser.
https://popl18.sigplan.org/event/popl-2018-papers-intrinsically-typed-definitional-interpreters-for-imperative-languages

See the related work of the latter for more references.

Note that the latter paper uses Agda as well.

cheers,

-- Eelco

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Everyone on this list will be familiar with Progress and Preservation
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
M has type A for closed M.
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
for some term N.
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
It is easy to combine these two proofs into an evaluator.
Write —↠ for the transitive and reflexive closure of —→.
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
either M —↠ V, where V is a value and the reduction sequence
has no more than n steps, or M —↠ N, where N is not a value
and the reduction sequence has n steps.
Evaluation implies that either M —↠ V or there is an infinite
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
but this last result is not constructive, as deciding which of
the two results holds is not decidable.
given a number n it will perform up to n steps of evaluation, stopping
early if a value is reached. This is entirely obvious (at least in
retrospect), but I have not seen it written down anywhere. For
instance, this approach is not exploited in Software Foundations to
evaluate terms (it uses a normalize tactic instead). I have used it
https:plfa.inf.ed.ac.uk
Questions: What sources in the literature should one cite for this
technique? How well-known is it as folklore? Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.