[[
wikihub
]]
Search
⌘K
Explore
People
For Agents
Sign in
Explore
People
For Agents
Sign in
@jemoka / Jemoka Knowledge Base / wiki/concepts/continuation.md
Suggest edit
Cancel
Submit suggestion
Title
Name
Note
--- title: "continuation" type: concept source: https://www.jemoka.com/posts/kbhcontinuation/ confidence: high status: active --- Consider: we can consider this as two parts the computation of x = e1 and the continuation e2 it essentially create statement labels: such that: \(k_0 = \lambda w . k_1 e\) \(k_1 = \lambda x . k_2 e’\) \(k_2 = \lambda y . k_3 (x+y)\) \(k_3 = \lambda z . z\) why we can make the order of evaluatinos explicit we give a name to each intermediate value we name every step of the computation it is important in language implementation (where ever intermediate result is named); but we can also make continuation available as program value. implementation: gotos \begin{equation} e \to \qty(x \mid \lambda x . e \mid e e \mid i \mid e + e \mid (call / cc) \lambda k.e \mid \text{resume}\ k\ e) \end{equation} specifically, we add two new cases which is translated as follows: \(C(call / cc\ \lambda x.e, k) = \qty(\lambda x . C(e,k))k\) \(C(resume\ k e, k’) = C(e,k)\) as in: call/cc - give the program access to the current continuation; it simply passes the program the current continuation \(k\) into the function provided to call/cc resume - instead of continuing at the intended continuation, continue at the given continuation instead this allows early returns, and other nice non-local control operations—exceptions, backtracking, jmp, co-routines discussion a software architecture device—event driven systems (events are basically continuations) makes program control first class values - which is nice when control flow is really really hard turns programs “inside-out”—this is contagious, which means it will affect the structure of the entire program CPS transformation Let \(C(e,k)\) to be the translation of \(e\) with continuation \(k\) into CPS. Meaning, we create a program \(C(e,k) = k e\), but we want \(e\) to also be in CPS: \(C(i,k) = ki\) for integers \(i\) \(C(x,k)\) for variable \(x\) sum Parse continuations in the order in which you would evaluate things. \begin{equation} C(e + e’, k) = C(e, \lambda v . C(e’, \lambda v’ . k (v + v’))) \end{equation} abstractions \begin{equation} C(\lambda x . e, k) \end{equation} challenge: we don’t evaluate under lambdas; its passed around until its called, then we need to CPS and evaluate it. That is, where \(e\) returns to (the continuation of \(e\)) is not \(k\)! Because we don’t know when the function is called. idea: we therefore split the continuation into two points, first \(k\) when function is used, and \(k’\) where functions are called. \begin{equation} C(\lambda x . e, k) = k (\lambda k’ . \lambda x . C( e, k’)) \end{equation} notice where the function is called, \(k’\) is a continuation you will have to pass the function for it to work. application \begin{equation} C(e e’, k) = C(e, \lambda f . C(e’ , \lambda v . f k v)) \end{equation} typically, we translate the function first—notice how we are passing the function the output continuation first, and then run the function on \(e’\) (named \(v\)). Complete Program The initial continuation is the identity function \(I\) (that is, \(\lambda x. x\)).