this past talk about continuations, and the case against call/cc

[Aaron Mansheim <minopret@gmail.com>]

Nice.

I want to note briefly how this past talk about continuations may relate to this discussion about call/cc. I also want to give a summary of the talk before much more time goes by. Finally, I want to suggest some further reading that may be relevant to you and me.

I think in the July presentation "Continuations: Primitive, Practical, and Proof", the objects that I actually constructed were not continuations as such, but perhaps "thunks". I think that continuations are meant to be opaque to their user, whereas the objects that I constructed had a great deal of accessible structure. It was only a convention in my programs that those objects were treated as (more or less) opaque and so as continuations.

Furthermore I was using these objects as the input to and result from a transition function within a loop, which I believe constitutes a trampoline. I think a trampoline delimits the scope of continuations within it. After all, they have no relevance outside of the trampoline.

I just haven't studied enough yet to know the fine distinctions and formalizations for all of these related constructs. I'm looking forward to learning more.

Here is a quick review of what we covered on the evening of July 17, with links to the specific resources from which I drew inspiration and information.

• http://matt.might.net/articles/writing-an-interpreter-substitution-denotational-big-step-small-step/ -- From this article by Matt Might, we discussed parts of the program SmallStepInterpreter.scala and its library file Exp.scala.

  We discussed a data structure in which we hold parsed expressions of the lambda calculus such as (λ s.λ z.s z). We discussed a similar but not identical data structure in which we hold expressions of the lambda calculus in which we have evaluated some but not all subexpressions. We discussed an algorithm to convert one representation to the other.

  That algorithm is a recursive post-order traversal of the _expression_ tree. I showed how we might implement that algorithm in the continuation-passing style, following the example of other subroutines in SmallStepInterpreter.scala. But rather than show that continuation-passing implementation in Scala, I showed it in the language of the Coq proof assistant, in order to introduce the topics of the following note.

• http://www.cis.upenn.edu/~bcpierce/sf/ -- I showed how, using the Coq proof assistant, we can write a formal logical proof that the continuation-passing implementation always achieves the same result as the recursive implementation. I used Coq itself without relying on its substantial standard library. I had learned from Software Foundations how to use Coq.

  The algorithms that we saw in Coq built their operations on booleans, natural numbers (that is, non-negative integers), and user-defined types from two key features of Coq.

  The first feature is typed lambda abstraction. For example the function in Coq that simply applies f to any member of type T is (fun (x : T) => f x). The second feature is universal quantification. For example, the type in Coq of that last function (fun (x : T) => f x)) is (forall x : T, f x).

  We were able to define each of our types by providing names and types for all of their constructors.

  For example, the boolean type has constant (that is, unparametrized) constructors "true" and "false". The natural number type "nat" has a constant constructor O to represent zero and a constructor S with parameter of type "nat" representing the successor of any natural number.

  The proven statements that we saw in Coq were called "theorems". Their proofs were written using "tactics".

  A tactic in Coq may be used to change a goal into one or more subgoals that, if all separately satisfied, are sufficient to achieve the original goal. A tactic in Coq may be used to change one or more facts in evidence into a consequent fact. Each goal or fact is a logical proposition, for example (forall x : T, f x). Through the Curry-Howard correspondence, each proposition is also a type, for example as (forall x : T, f x) is the type of (fun (x : T) => f x). The tactics for each of our completed proofs constructed a function whose outputs are terms having the conclusion types, and whose input terms have the universally quantified types and premise types.

  For example, we had a type named eq with a lone constructor refl_equal of type (forall (X : Type), X -> X -> eq). We had an infix notation using the equals sign "=" for eq and Coq would infer X as the type of values left and right of the equals sign. That is, for any term x in type X, the term (refl_equal X x x) had type (eq) and our notation permitted us to write (refl_equal X x x) as (x = x). In order to prove (forall (x : bool), x = x), we needed only to construct the term (fun (x : bool) =>  refl_equal bool x x), which is the same as (fun (x : bool) => x = x). There is no single correct sequence of tactics that achieves a particular proof. For example, we could write our proof using the "apply" tactic as "apply (fun (x : bool) => x = x)." Or we could just as well write our proof using another sequence of tactics that achieves the same result, for example "intros x. apply (refl_equal bool x x)." We saw that if we use the name of a theorem and ask Coq to print that theorem, then Coq will give us a peek behind the curtain of the Curry-Howard correspondence. Specifically it will print a single relatively complex function between types that itself has the type corresponding to the theorem as logical proposition. This is true even though our tactics usually seem to express many separate and rather intuitive steps of reasoning about propositions, without making us think about constructing one big abstruse function between types.

  The verification of the proofs did not rely directly on the validity of the tactics themselves. Rather, the programming language's type checker took the term that the tactics produced and checked that its type corresponded to the goal proposition.

I emailed Matt Might to ask what I might do to dig further into my interest in the topic of this talk. He graciously replied that I might want to read Olivier Danvy on transformational equivalences between abstract machines. I'm not exactly sure where to start on that, but taking that advice together with this discussion, perhaps I'll see what I can make of this:

http://www.brics.dk/RS/05/Abs/BRICS-RS-05-Abs/BRICS-RS-05-Abs.html#BRICS-RS-05-24#BRICS-RS-05-24
Ma

gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 
An Operational Foundation for Delimited Continuations in the CPS Hierarchy.

Thanks,
Aaron Mansheim


On Wed, 2012-08-22 at 20:55 -0400, Lalish-Menagh, Trevor wrote: 
> Hi all,
>
> I thought that since we are all continuation junkies here, we might
> find this interesting:
> http://okmij.org/ftp/continuations/against-callcc.html
>
> The article argues that call/cc is a bad core feature for a language
> (if you are designing a language), and claims that it is even worse
> that goto.
>
> In any case, it is an interesting read.
>
> Yours,
> Trevor