Am I right in saying that all of the continuation forms in racket macro-expand to continuation marks? I don’t see things like dynamic-wind in the “Fully Expanded Racket” section of the reference. It is not immediately obvious to me that continuations marks generalize all of the other forms, but I believe I have heard someone say that to me in person and would be willing to believe it.
@krismicinski no, that’s not right — most of the things you’re describing as “forms” are actually just functions, such as dynamic-wind and call/cc
Ah ok, silly me.
continuation marks certainly don’t generalize call/cc (it’s not clear to me what that would even mean)
Yeah, continuation marks seem to just annotate the stack, so I felt like they were substantively very different.. But for some reason I thought I remembered someone saying this to me.
continuation marks generalize a variety of other stack inspection primitives
thanks for letting me know.
Yeah, this was my impression, I was just surprised to see continuation marks in fully expanded racket without any other continuation forms. Are there any examples of Racket languages that need to instrument / handle continuations specifically?
I’m asking because I’m implementing a little language that handles security-relevant behavior, and calling a continuation is a kind of security-relevant effect.
Typed Racket needs to do a bunch of stuff wrt continuations, see our ESOP 13 paper
great.
but that’s not related to whether w-c-m is a core form
Yes, I understand.
I was just momentarily confused that this might be how these were handled, not sure why since nothing in the reference alludes to this..
I think that’s because the continuation mark semantics is simpler with it as a core form
but you certainly you could replace it with a call-with-continuation-mark form
yeah. I think I was thinking “continuations seem like a core thing, and certainly there are formalisms of continuations that are more general than others, perhaps this one core thing that’s in fully expanded racket is something that’s all-encompassing”
I’ll read this
Sorry if this a digression for #beginners, but we’re currently working on instrumenting racket with faceted values to track secure computations. I think handling continuations is a fundamental problem for this domain anyway, but we’ll certainly need to handle continuations for our language to be sound wrt the information flow semantics..
in general racket (like other languages such as C, Java, and Haskell) has a large number of primitive procedures that fundamentally expand the semantic model of the language even though they don’t change the syntax
thread, call/cc, make-struct-type, set-box! are all good examples
Yeah, Tom Gilray and I put together models for a bunch of these when he taught his compilers class. There were fewer than you’d think, but perhaps more than you’d want. Eventually we’d like to write a “real” static analyzer that handled all of these in some economical way, but Racket is pretty big, so even handling a reasonable subset seems tough (evidenced by Phil Nguyen working hard on it and making great progress but only after a lot of work, I suppose).
This isn’t such a bad thing, though. We’ll probably push on a prototype of this for the scheme workshop, and then throughout the year, some of my undergrad students can investigate many of these vagaries to create a more complete implementation..
Over the years, I’ve worked on 3 different roughly-complete models of Racket (Typed Racket, Pycket, and SCV) — it’s not for the faint of heart.
Okay, this is sage advice. I think in reality we will keep this mostly as a partially-complete language to drive our research, but then not attempt to be as ambitious as any of those projects…
That’s certainly reasonable. I think the way I’d put it is that the simplicity of the core language is a decision about how to factor the complexity of the language (again, one similar to C or Haskell, as opposed to say Scala) rather than an indication of the total complexity of the semantics.
Racket certainly seems more complex than C or Haskell, though, I think: core analyzers for raw STG or core LLVM IR are probably a good bit easier to implement than full Racket, I suspect. (Of course, I have no real empirical data to support this other than having seen some done for STG and x86 and being economical compared to the more elaborate complications of all of Racket.)
My point is that, like with Racket, it is not possible to examine merely the core language and think that that covers the complexity of actual C programs. malloc() and free() are the most obvious counter-examples, but there are many more.
some languages reify the the complexity of the semantic model in the term structure of the language, and some put it in the “standard library” (of course, many things in the “standard library” cannot be implemented as a library, such as malloc or apply)
Yeah, I think my collaborators and I are just much more willing to compromise on being incomplete these days. We spent a long time trying to come up with elaborate ways to model huge system APIs (most recently in Android, where we just resorted to using dynamic traces to stand in for the system model), but they always ended up being very hard to make both sound and precise. Someday maybe we’ll figure out how to attack this problem a bit better…
well, I think a C analysis that ignored malloc would be more than just “incomplete” …
I think that depends on what camp you belong to (bug finding or static analysis), but I certainly agree.. For “big” APIs like the ones we were modeling, being sound and also scalable just proved totally impossible (modeling an API with 100k method calls was just not possible for us). Although I agree something as fundamental as malloc would be something that you would never want to leave out, even if you are ultimately unsound.