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

[Guillaume Munch-Maccagnoni]

Le 21/05/2021 à 16:01, Oleg a écrit :
> 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.

    # let c (f : (int -> int) -> empty) =
         let g _x = match f (fun n -> n) with _ -> . in
         f g;;
    val c : ((int -> int) -> empty) -> empty = <fun>
    # let h = dne c;;
    val h : int -> int = <fun>
    # h 3;;
    Exception: Exc _.

This interpretation misses what makes continuation semantics 
constructive, and should be seen as mere analogy.

This is an example of mismatch between proof and program, different from 
the one that inhabits `empty` with a non-terminating function.



-- 
Guillaume Munch-Maccagnoni
Researcher at Inria Bretagne Atlantique
Team Gallinette, Nantes