Lambda the Ultimate

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!

Ostensibly, The Lightspeed Automatic Interactive Lighting Preview System by Ragan-Kelly et al. is about graphics, not programming language theory, and the abstract would confirm that opinion:

We present an automated approach for high-quality preview of feature-film rendering during lighting design.

However, I think it is an interesting example of a practical application of partial evaluation and specialization. 3D rendering is a computationally expensive process, but often the work of graphics artists is to make incremental changes rather than rendering fresh images from scratch. Lightspeed performs static dependency analysis of code written in the C-like Renderman shader DSL (RSL). The code is then specialised so that a static part (including a large 'cache' containing a partial computation) runs in the usual way in Renderman shader language on (a virtual SIMD machine on) the CPU, and a dynamic part is generated so as to run on a different architecture: GPGPU. The dynamic part contains the parameters that artists need to update frequently, resulting in fast previewing of results.

PS Note the 'lighting' in rendering-speak can mean any computation performed at a piece of geometry at the point at which you would compute the interaction between light and surface. Often it doesn't actually mean lighting.

(Disclaimer: I'm not an author on this paper but I did have an almost negligible bit of involvement.)