Created
March 21, 2018 20:34
-
-
Save jozefg/6d06872f31bd793ff071bae2774a39a2 to your computer and use it in GitHub Desktop.
Some exceptional programs in OCaml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Stubs to let us pretend that OCaml is closer to our language *) | |
let free (x : 'a ref) = print_endline "Deallocating...." | |
let fork (f : unit -> 'a) : 'unit = f (); () | |
(** Example 1: A finally combinator. Ensuring that a thunk is evaluated | |
* after another thunk regardless of the exceptions it raises | |
*) | |
let finally f g = | |
match f () with | |
| _ -> g () | |
| exception e -> g (); raise e | |
(* In this case, we wish to show that if [f] is known to not leak, | |
* then this program will never leak regardless of the exception | |
* behavior of [f] | |
*) | |
let fold_list_imperatively f seed xs = | |
let value = ref seed in | |
let rec go = function | |
| [] -> () | |
| x :: xs -> value := f (!value) x; go xs in | |
finally | |
(fun () -> go xs) | |
(fun () -> let result = !value in free value; result) | |
(** Example 2. A bracketing combinator encapsulating the acquire, use, | |
* release, pattern. | |
*) | |
let bracket get dispose use = | |
let r = get () in | |
(* Not quite finally, we return the result of use, not dispose *) | |
match use r with | |
| result -> dispose r; result | |
| exception e -> dispose r; raise e | |
(* The examples I can write down for this are a little more nebulous since | |
* we don't have any have resources besides memory, but we can imagine | |
* modelling more abstract resources using emit/consume | |
*) | |
let rec wait_on r = match !r with | |
| None -> wait_on r | |
| Some x -> x | |
(* Would like to show that this cannot leak *) | |
let memory_safe_par f g = | |
bracket (fun () -> ref None) free (fun r -> | |
let () = fork (fun () -> r := Some (f ())) in | |
let x = g () in | |
(wait_on r, x)) | |
(** Example 3. A more subtle notion of exception safety that often occurs | |
* in the C++ standard library: maintaining invariants when exceptions may | |
* occur. C++ has two notions of exception safety, "basic" and "strong". | |
* "basic" exception safety is the guarantee that in the event of an | |
* exception, there will be no leaks. "strong" exception safety states that | |
* if an operation fails due to an exception, there is no change to any data; | |
* no "partially done operations" should be visible. For instance, an | |
* exception safe map over a linked list. | |
*) | |
(* A representation of linked list closer to what would be found in C++ | |
* where the indirection is made explicit through a ref. | |
*) | |
type 'a cell = Nil | Cons of 'a * 'a linked_list | |
and 'a linked_list = 'a cell ref | |
let rec destroy_cell = function | |
| Cons (_, tail) -> destroy_cell (!tail); free tail | |
| Nil -> () | |
(* Prevents a partially updated linked list by constructing a new linked | |
* list and then swapping. | |
*) | |
let exception_safe_map f linked_list = | |
let rec go linked_list = | |
match !linked_list with | |
| Nil -> Nil | |
| Cons (h, t) -> | |
let t' = go t in | |
let h' = try f h with e -> (destroy_cell t'; raise e) in | |
Cons (h', ref t') in | |
let new_cells = go linked_list in | |
destroy_cell (!linked_list); | |
linked_list := new_cells |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment