Typed callcc in a stack-based language

I have been playing with the idea of adding a call-with-current-continuation primitive (callcc) to the Cat language. The type would be:

  callcc : ('A ('A ('A -> 'B) -> 'B) -> 'B) 

The formal semantics would be:

  [$A [$B] callcc $C] == [$A [$C] $B]

An example usage would be:

  >> define do_twice { dup [apply] dip apply }
  >> define test { 1 [do_twice] callcc inc }
  >> test 
  stack: 3

My questions are: am I doing this right? Does the type look correct? Is it a good idea to add continuations to Cat? Thanks in advance!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Not sure

I'm not sure if I understand the syntax of Cat correctly: would the type of "[apply] swap callcc" be ('A -> 'B)? If so, that would be bad news for your type system.

No it wouldn't, but either

No it wouldn't, but either way I made a mistake, so I'll have to get back to you.

The revised type.

I made an error in the type in the original post, the revised type should be:

  callcc : ('A ('A ('B -> 'C) -> 'B) -> 'B)

Here is how I arrive at the type using the Cat type system (see http://www.cat-language.com/paper.html ). Given an expression of the form:

t0 [t1] callcc t2 

We can assign the types given the type system of Cat :

t0:('A -> 'B)
[t1] callcc : ('B -> 'C) 
t2:('C -> 'D)

We know from the definition of callcc that t1 takes the stack plus the current continuation (the rest of the program) and returns a stack that is compatible with the consumption of t2 so the type must be:

t1 : ('B ('C -> 'D) -> 'C)

Applying the typing rule for quotation:

[t1] : (rho -> rho ('B ('C -> 'D) -> 'C)) 

Because of the rules of composition we know the following:

[t1] callcc : ('B -> 'C)

Composing t0 with [t1] gives us:

t0 [t1] : ('A -> 'B ('B ('C -> 'D) -> 'C))

Finally we can deduce the following:

callcc : ('B ('B ('C -> 'D) -> 'C) -> 'C)

Hopefully this makes some sense?

link

The link doesn't work. Should probably be http://www.cat-language.com/.

Thanks, fixed.

Thanks, fixed.

Can you say something how

Can you say something on how this type relates to the usual ((P->Q)->P)->P type for call/cc?

Good question. I need to

Good question. I need to figure out the type for the correct implementation of callcc, and then I should able to answer this question.

I'll also try to properly show the relationship between regular type notation and the stack-based notation I use.

My answers are

My questions are: am I doing this right?

Probably not. You've just applied a continuation captured by call/cc twice, right? Think about that.

Does the type look correct?

Hard to tell, because I find your notation for types hard to read.

Is it a good idea to add continuations to Cat?

It's always a good idea to add continuations :)

My advice is that it is very hard to give a semantics to continuations without, you know, continuations. Forget your reduction semantics, you (the generic you) almost always go wrong with that sort of first-order, operational reasoning. Write down a simple, compositional higher-order evaluator for Cat (the one Anton keeps alluding to). Defunctionalizing the functional values will give you the first-order one you have in mind (ie, the big-step operational semantics). CPS transforming it will give you continuations. The semantics of call/cc should now be obvious. Defunctionalizing the continuations will give you an abstract machine. Reading the configurations of the machine as "terms" (a la Felleisen and Friedman), you should be able to classify the transitions as ones implementing compatibility rules (where the left and right-hand sides represent the same term) and reduction rules (where they don't). From this, you should be able to obtain the small-step reduction semantics you refer to above (and can use, say, to prove the progress part of type soundness), but still grounded in the intended semantics as embodied in the higher-order interpreter.

Continuations and Evaluators.

Probably not. You've just applied a continuation captured by call/cc twice, right? Think about that.

I see, I made a mistake by interpreting a continuation as "the rest of the function", rather than "the rest of the program". In other words I was implementing the continuation as a "call" instruction instead of a "jmp". I wonder if such a beast have a name, and a known practical use.

Hard to tell, because I find your notation for types hard to read.

Left side of the arrow is the top of the stack before execution, right side of the arrow is the top of the stack after execution. Big letters are type vectors, and little letters are simple types. Does that help? Any suggestions on how I could make the type clearer given that Cat is a stack-based language?

you almost always go wrong with that sort of first-order, operational reasoning

So this is generally considered a poor way to present language semantics? Or is it more that isn't easily extended for formal discourse?

Write down a simple, compositional higher-order evaluator

Like this?

exp0 0 inc -> exp0 -1
exp0 0 dec -> exp0 1
exp0 num0 inc dec -> exp0 num0
exp0 num0 num0 lteq_int -> exp0 true
exp0 num0 num0 succ lteq_int -> exp0 true
exp0 num0 num0 pred lteq_int -> exp0 false
exp0 val0 pop -> exp0
exp0 val0 dup -> exp0 val0 val0
exp0 val0 val1 swap -> exp0 val1 val0
exp0 val0 quote -> exp0 [val0]
exp0 [exp1] [exp2] compose -> exp0 [exp1 exp2]
exp0 [exp1] apply -> exp0 exp1
exp0 val0 [exp1] dip -> exp0 exp1 val0
exp0 true [exp1] [exp2] if -> exp0 exp1
exp0 false [exp1] [exp2] if -> exp0 exp2
exp0 [exp1] [exp2] while -> exp0 exp1 [] [[exp1] [exp2] while] if
t1 -> t1’ => [t1] -> [t1’]
t1 -> t1' => t1 t2 -> t1’ t2
t2 -> t2’ => t1 t2 -> t1 t2’

Thanks for your help!

I see, I made a mistake by

I see, I made a mistake by interpreting a continuation as "the rest of the function", rather than "the rest of the program". In other words I was implementing the continuation as a "call" instruction instead of a "jmp". I wonder if such a beast have a name, and a known practical use.

It is a delimited continuation, with an implicit delimiter around the body of every function. Landin's original control operator, J, behaved this way except that it captured the continuation of the function, not the continuation up to the end of the function.

I sort of like Danvy and Malmkjaer's term, from the reflective tower, which is ``pushy'' vs. the ``jumpy'' continuations captured by call/cc.

So this is generally considered a poor way to present language semantics? Or is it more that isn't easily extended for formal discourse?

I don't think it's generally considered that way. However, there are dozens of language features and effects that are subtly wrong, because they were designed by hacking on an abstract machine or small-step reduction semantics instead of some higher level semantics (ie, big-step operational or denotational).

That's a little like compiling your program and then adding functionality by using a hex editor on the binary image.

Like this?

I'm thinking something more like this:

datatype command = LIT of int | DUP | APPLY | DIP | INC | QUOTE of command list

datatype value = INT of int | FUN of stack -> stack
withtype stack = value list

(*  eval_one : command * stack -> stack *)
fun eval_one (LIT n,    s)               = INT n :: s
  | eval_one (DUP,      v :: s)          = v :: v :: s
  | eval_one (APPLY,    FUN f :: s)      = f s
  | eval_one (DIP,      FUN f :: v :: s) = v :: f s
  | eval_one (INC,      INT n :: s)      = INT (n + 1) :: s
  | eval_one (QUOTE cs, s)               = FUN (fn s' => eval_list (cs, s')) :: s

(*  eval_list : command list * stack -> stack *)
and eval_list (nil,     s) = s
  | eval_list (c :: cs, s) = eval_list (cs, eval_one (c, s))

(*  evaluate : command list -> stack *)
fun evaluate cs = eval_list (cs, nil)

Thank you very much

I appreciate you taking the time and effort to explain these things and providing an example of the higher-level semantics of Cat. Is the form you used denotational semantics or is it big-step operational semantics?

For others following along and who are unaware of the J operator see A Rational Deconstruction of Landin's J Operator by Olivier Danvy and Kevin Millikin.

Is the form you used

Is the form you used denotational semantics or is it big-step operational semantics?

It's an SML implementation of what I imagine the denotational semantics evaluation function would be for your language.

You can defunctionalize the applicable values (FUN). There is one abstraction whose only free variable is a list of commands. Make the following changes:

datatype value = INT of int | FUN of command list

fun eval_one (APPLY,    f :: s)      = apply (f, s)
  | eval_one (DIP,      f :: v :: s) = v :: apply (f, s)
  | eval_one (QUOTE cs, s)           = FUN cs :: s

and add an apply function for applicable values

(*  apply : value * stack -> stack *)
and apply (FUN cs, s')
    = eval_list (cs, s')

This is an SML implementation of what I imagine the big-step operational semantics evaluation function for your language is. You can obviously inline apply but might not want to if there is more than one kind of applicable value (eg, continuations), since it is called (at least) twice.

Indeed

I wonder if such a beast have a name, and a known practical use.

Delimited continuations (see shift/reset in e.g. this page).

Great Link

Great link, thank you.