mheiber · September 17, 2024 10:52 · Sep 17, 2024 · Sep 17, 2024 · Sep 17, 2024
diff --git a/computing with excluded middle.md b/computing with excluded middle.md
@@ -36,5 +36,14 @@ It's the "Devil's Bargain" from Wadler's "Call-by-Value is Dual to Call-by-Name"
 
 But, theoretically, there *are* several ways of using excluded middle to compute interesting things:
 
+(1)
 Backtracking– .... no reference found
-Using classical linear 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"
+
+(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](https://cs.stackexchange.com/questions/139003/is-there-a-relationship-between-visitor-pattern-and-demorgans-law):
+
+
+> 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 ...
diff --git a/computing with excluded middle.md b/computing with excluded middle.md
@@ -7,23 +7,30 @@ Translated to OCaml using the double-negation translation of classical to intuit
 
 ```
 
-let rec loop_forever : unit -> void =
-
-fun () -> loop_forever ()
+type void = |
 
- 
-
-let use_excluded_middle: int a_or_not_a -> void = function
+type 'a not = 'a -> void
+        
+type 'a a_or_not_a =
+    | A of  'a
+    | Not_a of 'a not
 
-| A a ->
+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)))
 
-(* a is 3. We only got out what we put in *)
+let rec loop_forever : unit -> void =
+    fun () -> loop_forever ()
 
-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
 
-| 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.
 

diff --git a/computing with excluded middle.md b/computing with excluded middle.md
@@ -0,0 +1,33 @@
+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.
+
+
+
+```
+
+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 *)
+
+loop_forever ()
+
+| Not_a f -> f 3
+
+ ```
+
+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:
+
+Backtracking– .... no reference found
+Using classical linear 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"
No results found