Home » forums » LtU Forum

Co-continuations: a dual to shift/reset?

Shift/reset allow convenient expression of monadic computations, as a kind of generalized, functional version of do-notation. From the beginning of that link:

Continuations represent the rest of the computation. Manipulation of continuations is a powerful tool to realize complex control flow of programs without spoiling the overall structure of programs. It is a generalization of exception handling, but is far more expressive.

The obvious question is whether there is an analogous construct for comonads. Given that there is a codo-notation I believe there is.

In a concatenative language, shift/reset can be written as:

[F] shift K reset = [K] F reset

The F block observes the future of the computation (delimited by the nearest reset) and may select a new one.

I believe the comonadic dual is:

coreset E [F] coshift = coreset [E] F

The F block observes the past of the computation (delimited by the nearest coreset) and may select a new one.

This leads to a combined operator:

{ E [F] shift K } = { [E] [K] F }.

The F block observes the future and past of the computation (delimited by the nearest braces) and may select new ones. This is first class (co)control flow.

I want to say something like "the dual of continuations is environments", as "environment" is an existing concept that seems conceptually close to "store". Note that on this page, someone posts functions analogous to shift/reset for "codensity" or "store".


          redex
        ---------
    { E [F] shift K }
      ^           ^
  environment continuation

I believe this notation allows the convenient expression of arrows (and monads and comonads) in the same way shift/reset allows expression of monads. Arrows allow decoration of both inputs and outputs, as opposed to only inputs for comonads and only outputs for monads.

This makes sense to me but I'm not totally sure since there's not much information on comonads/codo notation and such. I'd appreciate any comments.

EDIT: I think the correct format is actually


{ E [F] shift K } = [{ E }] [{ K }] F

By xkapastel at 2018-10-07 15:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 3590 reads

Comment viewing options

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

Comonadic state

I have difficulty getting my head around concatenative control structures sometimes. Is there some kind of semantic intuition that could help? Perhaps an SECD machine, or a translation into Haskell?

But this remark stood out:

> I want to say something like "the dual of continuations is environments", as "environment" is an existing concept that seems conceptually close to "store".

The categorical semantics of linear logic can be given as a comonad (for exponentials) over a monoidal closed category. Abramsky and McCusker showed how this structure could model state (Linearity, Sharing and State: A Fully Abstract Game Semantics for Idealized Algol with Active Expressions). The core idea of the paper depends on Reynolds' decomposition of state of a given sort of value into types that represent expressions that can evaluate to the values of that sort (exp[A]), and types representing acceptors that can be given values of a given sort (var[A]); variables can be viewed as having the intersection type exp[A] & var[A], meaning that they can either have their current value read from in an expression, or they can be assigned a value which will update their future behaviour. exp[A] and var[A] might exhibit the duality you are after.

This is really nice stuff. I have not seen any practical uptake of these ideas, and none of the literature seems to have moved far from very abstract semantics, which is a shame.

By Charles Stewart at Mon, 2018-10-08 14:34 | login or register to post comments