(call/cc call/cc) and friends

We can write a simple function to compute the behavior of a tree of calls to call/cc:

data CallCCTree = CallCC | Application CallCCTree CallCCTree
data Behavior = CallCC | Extract | Loop

reduce :: CallCCTree -> Behavior

Implementing this function is a simple encoding of the table of rules.

reduce CallCC = CallCC
reduce (Application CallCC CallCC) = Extract
reduce (Application CallCC _) = reduce _
reduce (Application _ CallCC) = reduce _
reduce (Application _ _) = Loop

We’ve discovered that this set of three behaviors has a (kind-of) natural binary operator. Perhaps this operator satisfies some interesting properties?

It is commutative, as is evident from the table.

It is not associative, since ((call/cc call/cc) (call/cc call/cc)) and (call/cc (call/cc (call/cc call/cc))) are different.

It does not have an identity, because the operator never returns C.

It does have a zero, looping.

So it this operator doesn't seem to form a nice mathematical structure, which is a pity. But then, aren't delimited continuations the one true continuation operator?

Edit: Thank you James Wilcox! noloop had a subtle bug. The order of two cases was swapped, and didn't properly handle (* *).

Edit: Previous versions of this post distinguished a “self-application” and an “extraction” behavior. They were in fact the same behavior.

Edit: Siyuan Chen clarified how the a@ annotation at the beginning of this section behaves.