--------------------------------------------------------------------------|
| Table of contents                                                       |
| - How to decompose the global rule into local rules and toplevel rules? |
| - Is Felleisen's C operator typable of type ~~A -> A?                   |
| - Can Felleisen's C operator be typed of another type than ~~A -> A?    |
| - Is the return type of the continuation variables important?           |
| - Conclusion on how to type Felleisen's C                               |
| - Is the \-K calculus distinct from the \-C calculus ?                  |
---------------------------------------------------------------------------
Written in August 2004, updated in Mars 2007, then April 2014.

How to decompose the global rule into local rules and toplevel rules?
--------------------------------------------------------------------

The original operational reduction rule for C in
Felleisen-Friedman-Kohlbecker-Duba 1986 is

E(C(M)) -> M(\x.A(E(x)))

where A is an abbreviation for \x.C(\k.x)
and E is an evaluation context (call-by-name or call-by-value).

It can be decomposed (in CBV) into lifting rules and toplevel rules

The lifting rules:

C(M) N -> C(\k. M(\f.k(fN))
V C(M) -> C(\k. M(\x.k(Vx))

Remark: Felleisen's original lifting rules are

C(M) N -> C(\k. M(\f.A(k(fN)))
V C(M) -> C(\k. M(\x.A(k(Vx)))

which allows to reduce e.g. C(\k.k(kM))N to C(\k.A(k(A(k(MN))N)) then
to C(\k.A(k(MN))) while C(\k.k(kM)) don't reduce to C(\k.kM) only
using beta and lifting rules. This makes subterms behave differently
when in a non empty context or no, so that the above choice is more
natural. Moreover, combined with the toplevel rules, the insertion of
A in the lifting rules become useless.

The toplevel rule:

C(M) -> M(\x.A(x))    only at toplevel


Is Felleisen's C operator typable of type ~~A -> A?
--------------------------------------------------

Yes and no, it depends on which reduction rules we consider for C.
The lifting rules are consistent with typing C:~~A->A, but the
toplevel rules require the extra condition that the toplevel has type
bot. To solve this mismatch, there are at least two solutions

- Griffin's solution:

Griffin evaluates only terms of the form 

C(\top.M)

where top has type A->bot for an arbitrary A and M has type bot. The
new toplevel rule applies in M only as follows

C(\top.C(M)) -> C(\top.M(\x.A(x))

in which case, M has type ((bot->bot)->bot)

- Krivine's solution:

Remove toplevel rules and add a simplification rule:

C(\k.k M) -> M    (if k is not free in M)

- Murthy's approach:

Introduce two aborts:

A2 is still an abbreviation for \x.C(\k.x), it has type bot->A 
A1 is primitive and has type top->A

- Ariola-Herbelin approach:

Make explicit a toplevel continuation top of type top->bot

C(M) -> M(\x.A(x))

where A is now an abbreviation for \x.C(\k.(top x))

- Alternative solution:

Give C the type ((A->top)->top)->A

- All these solutions (but Krivine which restricts the reduction rules
  so that C(\k.k M) is not reducible to a value if k occurs in M)
  amounts to the same:

  - Griffin adds a toplevel continuation top:top->bot, so that to get
    M of type (bot->bot)->bot, it should be eta-equivalent to some
    term \k.k(...(k(top M'))...) with M' of type top (or of the form
    \k.C(M') with M' recursively of the same form).

  - Murthy adds A1 which can be defined as \x.A2(top x)

  - The alternative solution interprets C(M) as C(\k.(top(Mk))


Can Felleisen's C operator be typed of another type than ~~A -> A ?
-----------------------------------------------------------------

The toplevel reduction rule E(C(M)) -> M(\x.A(E(x))) suggests that a
more appropriate type is ((A->bot)->top)->A where top is the toplevel
type. Especially, A got the type top->A.


Is the return type of the continuation variables important ?
----------------------------------------------------------

A continuation variable is expected to be used in arbitrary contexts
of any type. Its type should then return some arbitrary B, dependent
on the context. This is not possible with simple types, such as ML
types. There are then two possibilities.

- make the continuation variables returns bot with an implicit coercion
bot->A.

- make the continuation variables have some type "A cont" and use an
  explicit operator throw of type "A cont -> A -> B" as in SML.

- make the continuation variables have type "A->top" and use Abort
  (i.e. \x.C(\_.x)) to go from top to an arbitrary B.

  This last possibility has the advantage to scale to the semantics of
  shift: with giving to C of type ((A->top)->top)->A, it can be used
  as a shift or as a C. For shift, just compose continuation variables
  of type A->top. For C, just surround them by an abort.


Conclusion on how to type Felleisen's C
---------------------------------------

According to our analysis, the most appropriate type for Felleisen's
C operator is not ~~A->A but 

  - either ((A->bot)->top)->A with an implicit coercion from bot to B
    (or even an explicit one)

  - or ((A->top)->top)->A in which case, it is convenient to make the
    semantics of C defaults to the semantics of shift. The semantics
    of C is recoverable by inserting an abort around each call to a
    continuation variable.


Since call-cc (i.e. K) corresponds to Peirce's law which does not
enforce ex falso quodlibet (i.e. bot -> A), can we talk about the \-K
calculus as an calculus independent from \-C ?
----------------------------------------------

The answer is yes if we don't consider the toplevel rules, but if we
does, Abort becomes necessary and we recover \C calculus, where
C = \x.K(\k.A(xk)