Pattern matching nesting reduction

We have to implement the function classify with the following signature

type Status = Started | NotStarted | Completed
let classify (first: 'a option) (last: 'b option): Status = raise <| NotImplementedException()

A common implementation would be the following:

let classify (first: 't option) (last: 'u option) =
  match first with
  | Some _ ->
    match last with
    | Some _ -> Completed
    | _ -> Started
  | _ -> NotStarted

[classify (Some 0) None; classify None (Some "x"); classify (Some 0) (Some "y")]

However, we can make a trade of nested pattern matching by a more complex data structure and a simpler pattern match:

let classify (first: 't option) (last: 'u option) =
  match first, last with
  | Some _, Some _ -> Completed
  | Some _, _ -> Started 
  | _ -> NotStarted

[classify (Some 0) None; classify None (Some "x"); classify (Some 0) (Some "y")]

The trick can be generalized if the following conditions are true - you have a nested pattern matching - the decision to take one branch or another depends only on pure values (no implicit state can change the decision)

Then what we do is encoding in each branch the precondition necessary to produce each value in the original code. Let's anotate the previous example with such preconditions:

let classify (first: 't option) (last: 'u option) =
  match first with
  | Some _ ->
    match last with
    | Some _ ->
        // precondition: first.IsSome && last.IsSome 
        Completed
    | _ ->
        // precondition: first.IsSome && last.IsNone
        Started
  | _ -> 
    // precondition: first.IsNone
    NotStarted

Now you can see we only use the arrow -> when we match the exact condition that produces a value, and by following that principle we continue by creating a more complex structure to match, but we reduce the nested matches. The inspiration for this trick comes from Dijkstra's Guarded Command Language and Programming: The Derivation of Algorithms.