[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
