[TYPES] What's a program? (Seriously)

[Oleg]

Classical and intuitionistic computational interpretations use very
different CH correspondences; in particular, the meaning of ->
differs.  Lots of confusion could be avoided if we used different
symbols for logical connectives, specifically ->. Or wrote modality
explicitly (as Thielecke does). The type of call/cc does look like Peirce's law
-- but the meaning of arrows differs, and so are CH correspondence,
proof (ir)relevance and other properties.

Recall the Peirce's law:
peirce :  ((A->B)->A) -> A

When we talk about logic and the standard CH correspondence, -> in types
is taken as logical implication: as Martin Escardo noted already, A -> B 
means that if you give me an instance (inhabitant) 
of A, I will give you an instance of B -- without fail. (Sorry for
stating the obvious: we shall soon see how it all changes in
computational interpretations of classical logic.) Such interpretation
means that a term of the type A -> \bot witnesses that A is
uninhabited. There are two points to note about such term:
   -- although it can be thought of as a program, such program can
never be run because there are no suitable inputs;
   -- if there are two terms of the type A -> \bot, there are
equivalent as programs: because neither can actually be run, we have no
means to observe their distinction. 

Now lets recall call/cc and see how all the above changes, although
looking superficially the same. The type of call/cc is

call/cc : ((A->B)->A) -> A

It looks identical to the type of peirce, as Matthias said. But only
on the surface. A->B in call/cc does *not* mean a function that takes
an instance of A and returns the instance of B. In call/cc, this
subterm is actually an undelimited continuation, and when called, it
does not return anything because it never returns (think of
exceptions). So, the meaning of arrow is very different from what we
saw in the original and familiar CH. As I said, it would save a lot of
confusion if we use a different arrow sign, or write the modality
explicitly, as shown in

 Hayo Thielecke: Control Effects as a Modality. JFP, 2009.

To see the distinction clearly, let's look at double-negation
elimination -- which can be stated without call/cc and time travel, or
continuation or other exotic. Familiar exceptions suffice. Here it is
in OCaml.

type empty = |   (* empty type *)

let dne: type a. ((a -> empty) -> empty) -> a = fun c ->
    let exception Exc of a in
    match c (fun a -> raise (Exc a)) with
    | exception Exc a -> a
    | _   -> .  (* impossible *)
;;

We see several terms of the type A -> \bot. Now, the existence of such
terms no longer implies that A is uninhabited! (Now, type inhabitation
is no longer directly connected to the truth of propositions.)
Since A may well be inhabited, we can 
run such terms. Different terms of that type can have observable differences
(e.g., raise different exceptions) and are no longer equivalent.


If we use an appropriate semantics -- bubble-up semantics proposed by
Felleisen and Parigot, we can very well normalize under binders. For
example,

        (fun a -> raise (Exc a); raise (Something else))
Here, raise (Exc a) creates a `bubble' containing Exc a. Following the
rule
        (bubble v) ; e -> (bubble v)
that bubble eradicates the second raise. There is no rule for a bubble
to cross an abstraction boundary, so we stop and get the normal form.