Lambda the Ultimate

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

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?

Thanks, fixed.

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.

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â€TM => [t1] -> [t1â€TM]
t1 -> t1' => t1 t2 -> t1â€TM t2
t2 -> t2â€TM => t1 t2 -> t1 t2â€TM

Thanks for your help!

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)

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

Great link, thank you.