--------------------------------------------------------------------------| | 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)