How to: removing exceptions using Choice _, _

Approach 1: lifting all code paths from 'T to Choice<'T, exn>

For example, this function

let dest_type = function 
    | (Tyapp(s, ty)) -> s, ty
    | (Tyvar _) -> failwith "dest_type: type variable not a constructor"

is transformed to

let dest_type = function 
    | (Tyapp(s, ty)) -> Choice.succeed (s, ty)
    | (Tyvar _) -> Choice.failwith "dest_type: type variable not a constructor"

where two possible paths are of type Choice<hol_type, exn> and no exception is raised.

Approach 2: wrapping inner functions inside a try/with block

To illustrate, this function

let rec type_of tm = 
    match tm with
    | Var(_, ty) -> ty
    | Const(_, ty) -> ty
    | Comb(s, _) -> hd(tl(snd(dest_type(type_of s))))
    | Abs(Var(_, ty), t) -> 
        Tyapp("fun", [ty; type_of t])
    | _ -> failwith "type_of: not a type of a term"

is turned into

let type_of tm = 
    let rec type_of tm = 
        match tm with
        | Var(_, ty) -> ty
        | Const(_, ty) -> ty
        | Comb(s, _) -> hd(tl(snd(Choice.get <| dest_type(type_of s))))
        | Abs(Var(_, ty), t) -> 
            Tyapp("fun", [ty; type_of t])
        | _ -> failwith "type_of: not a type of a term"
    try
        Choice.succeed <| type_of tm
    with Failure s ->
        Choice.failwith s

Notice that the original type_of function becomes an inner function and we catch all possible exceptions in outer function. Why should we do so? The reason is that Choice.get, hd and tl functions can throw exceptions. So we have to explicitly handle each of these functions if we would like to avoid using try/with. Remember that this is a quick-and-dirty approach; we should switch to other approaches for better performance.

Approach 3: using choice computation expression

When we do conversion on core modules, we insert Choice.get at call sites. At some point, outer modules will contain full of Choice.get calls. We can use choice computation expression in this scenario.

This example

let alpha v tm = 
    let v0, bod = 
        try 
            Choice.get <| dest_abs tm
        with
        | Failure _ as e ->
            nestedFailwith e "alpha: Not an abstraction"
    if v = v0 then tm
    elif Choice.get <| type_of v = (Choice.get <| type_of v0) && not(vfree_in v bod) then Choice.get <| mk_abs(v, Choice.get <| vsubst [v, v0] bod)
    else failwith "alpha: Invalid new variable"

is transformed to

let alpha v tm = 
    choice {
        let! (v0, bod) = 
            dest_abs tm 
            |> Choice.bindError (fun e -> Choice.nestedFailwith e "alpha: Not an abstraction")
        if v = v0 then return tm
        else
            let! ty = type_of v
            let! ty0 = type_of v0
            if ty = ty0 && not(vfree_in v bod) then 
                let! sub = vsubst [v, v0] bod
                return! mk_abs(v, sub)
            else return! Choice.failwith "alpha: Invalid new variable"
    }

Inside a choice computation expression:

• let! allows us to implicitly get 'T value from Choice<'T, exn>. If an error case is supplied, the code block after this point isn't executed.
• return! allows us to return a Choice<'T, exn> value inside computation expression.
• return is the facility to lift a 'T value to Choice<'T, exn> (as easy as an implicit Choice.succeed call).
• we see that all branches have the same Choice<'T, exn> return type and we get rid of all nasty Choice.get occurrences.