Computing with excluded middle, like in Griffin's "A Formulae As Types Notion of Control"

Translated to OCaml using the double-negation translation of classical to intuitionist logic.

type void = |

type 'a not = 'a -> void
        
type 'a a_or_not_a =
    | A of  'a
    | Not_a of 'a not

let not_not_excluded_middle: type a. a a_or_not_a not not =
    fun k -> k (Not_a (fun (a: a): void -> k (A a)))

let rec loop_forever : unit -> void =
    fun () -> loop_forever ()

let use_excluded_middle: int a_or_not_a -> void = function
    | A a ->
            (* a is 3. We only got out what we put in. And now we have to return void *)
            loop_forever ()
    | Not_a f -> f 3

(* of course, loops forever*)
let _: void = not_not_excluded_middle use_excluded_middle

It's the "Devil's Bargain" from Wadler's "Call-by-Value is Dual to Call-by-Name": an apparently-useless stunt.

But, theoretically, there are several ways of using excluded middle to compute interesting things:

(1) Backtracking– .... no reference found

(2) Using classical affine logic as a high-level language compilable to intuitionist logic. Haven't found programming use cases yet, but there are examples in Shulman's "Affine logic for constructive mathematics". May be related to the other items on this list.

(3) Another angle on usefulness of par is in [cite:@binderGrokkingSequentCalculus2024] (watch out, they use ⊕ differenlty from Shulman). They explain that error-handling with Either/Result is like additive disjunction and that there is an alternative that uses multiplicative disjunction. The example is a bit vague, and iuc doesn't show much more than how to translate between sums and products by passing through a function type:

A function which returns a value of type [sigma par tau] has to be called with two continuations, one for the possibility that the function returns successfully and one for the possibility that the function throws an error. And the function itself decides which continuation to call, so there is no overhead for checking the result of a function call. This is quite similar to how some functions in Javascript are called ...