Log in

No account? Create an account
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Sep. 23rd, 2008|08:23 pm]
[Tags|, ]

ICFP day two. I have a wretched cold: it is not fun.

The invited talk was again very good. Olivier Danvy is a great, animated speaker. I missed a couple of jokes through the haze of French accent, but there were plenty of zingers left. He talked a lot about some known facts that are apparently quite old, but new to me in their given form, and quite appealing.

The short version is basically this story:

John Reynolds grabs you by the wrist one fine day and shows you a definitional interpreter of the lambda calculus, implemented in a straightforward way in your favorite functional programming language, and asks you, "is this interpreter Call-by-Name or Call-by-Value?". It turns out it's a trick question! Because of the utterly transparent way the interpreter is written*, it's CBN if your favorite language is, and CBV if your favorite language is.

The next neat thing is if you defunctionalize and CPS convert this definitional interpeter, you get a standard stack machine semantics --- actually, one of two rather standard stack machine semantics, depending on whether you take the CBN or CBV version of the CPS transform.

The moral I take away from this is that if you're looking for the ultimate origin of the interesting stuff, the stack machines that actually tell us how to do computation, well, their meaning is hidden away in the CPS and defunctionalization transformations. For the datum that these transformations are applied to, namely the definitional interpreter, has no real meaning unto itself. It basically just says "translate app as app, var as var, lam as lam".

What I want to know is: what does this tell us about HOAS, the epitome, if anything is, of making mountains out of meta-mountains? If we vary the meaning of β-reduction, or of variables, (in some way more drastic than just making them substructral or modal or something) what might this do to our encodings?

* Which was called the "Scott-Tarski interpreter" by Danvy, alluding to Dana Scott because it implements a solution of the domain equation D = D → D, and Tarski because of Girard's habitual complaining about "Mr. Meta-Tarski" defining first-order logic in an equally "transparent" way by saying "|= A v B holds if, you know, either |= A or |= B holds", relying on our natural-language intuitions (or perhaps classicalitions?) of the meaning of disjunction.

From: olivier_danvy
2008-10-08 07:14 am (UTC)



As Bob Harper is fond to say, functions in HOAS are pure and total, so CPS transformation brings nothing new. A long time ago, in "CPS Transformation after Strictness Analysis" (LOPLAS 1993) and in "On the Transformation between Direct and Continuation Semantics" (MFPS 1993), John Hatcliff and I elaborated on this idea by constructing mixed CPS transformations that depended on the lambda-abstractions and applications in the source program being strict / non-strict, or total/ non-total. For example, a total function would be left in direct style, while a non-total function would be CPS-transformed. So a program where all functions are total would be mapped to itself, while a program where all functions are not total would be completely CPS-transformed. A mixed program where some functions are total (eg, because they implement HOAS) and others are not would be transformed into a program where not all functions are in CPS, but others remain in direct style.

So now you know why

fn f => (f 10) + (f 20)

is CPS-transformed into

fn k => k (fn f => fn k => f 10 (fn v1 => f 20 (fn v2 => k (v1 + v2))))

instead of into

fn k => k (fn f => fn k => f 10 (fn v1 => f 20 (fn v2 => plus_c (v1, v2) k)))

where plus_c is the CPS version of +.
The reason is that (ignoring integer overflow) + is total, and therefore can be left in direct style in the residual CPS program without endangering Plotkin's Indifference theorem.

The point is elaborated further in Lasse Nielsen's BRICS Research Report "A Selective CPS Transformation" at
(and while you are at it, you can also peek at BRICS RS 01-29, "A Unifying Approach to Goal-Directed Evaluation", which is fun).


-- Olivier Danvy
(Reply) (Thread)
[User Picture]From: jcreed
2008-10-08 12:52 pm (UTC)


Thanks much for the literature pointers! I had no clue you might be reading this.

The fact that + can be left as direct style by virtue of its totality makes perfect sense --- this reminds me of a point Tom Murphy made to me that the right way to think about pairing from a compiler's point of view is that pair-expressions and pair-values are very different, that a pair expression in the source language should really CPS-convert to an instruction in the CPS language that performs allocation, and then returns the pair value.

But of course (barring running out of memory) this allocation operation is total, so we can if we like more abstractly say that a pair of values just is a value, and avoid the extra allocation steps in the CPS destination language.

In any event, the question I was asking about HOAS was somewhat divorced from CPS --- I was thinking about how various operational semantics for programming languages --- respectively, different CPS translations --- are maybe analogous to a different sort of various interpretations of an intensional function space in HOAS --- and maybe respectively different ways of tranlating them into first-order representation.

For instance, transforming
tm : type.
lam : (tm -> tm) -> tm.
app : tm -> tm -> tm.

into a first-order representation
nat : type. z : nat. s : nat -> nat.
var : nat -> tm.
lam : tm -> tm.
app : tm -> tm -> tm.

seems to me very much unlike a CPS transform, but if it is somehow, I would love to hear the story!
(Reply) (Parent) (Thread)