Dependent pattern matching syntax in F*

[yiyuan-cao]

Hello, everyone! I just started learning the F* language. Could you please tell me the complete syntax for dependent pattern matching in F*?

[nikswamy]

Pattern matching in F* is dependent, by default, since F* checks the branches in a context that includes equations between the matched term (aka the scrutinee) and the pattern.

That is, you can write:

type t : Type =
  | TB
  | TI

let bool_or_int = function
  | TB -> bool
  | TI -> int
  
let ex (x:t) : bool_or_int x =
  match x with
  | TB -> true
  | TI -> 0

and F* automatically converts from bool or int to bool_or_int x in each branch. To do this conversion, it generates a proof obligation for Z3 to check that the two types are provably equal, i.e., roughly, in the first branch, the goal to Z3 looks like x:t, x==TB |- bool == bool_or_int x, and similarly for the second branch.

Sometimes, however, you may want to avoid this call to Z3 and instead get F* to refine the type of the branches simply by conversion/definitional equality. For this purpose, F* also offers an explicit dependent pattern matching syntax. For example, you can write

let ex2 (x:t) =
  match x as y returns (bool_or_int y) with
  | TB -> true
  | TI -> 0

• The scrutinee x is bound as y in the return type bool_or_int y
• Each branch is checked to have the type obtained by substituting y for that branch's pattern

That is, the first branch is checked to have type bool_or_int TB and the second bool_or_int TI.

Now, the proof obligation that F* generates for the first branch is bool <: bool_or_int TB and the right-hand side of this just reduces and the goal becomes bool <: bool, which is trivial, without needing any Z3 query. Similarly for the second branch.

Note, as a shorthand, when the scrutinee is itself a variable, you don't need the as y part. You can just write:

let ex2 (x:t) =
  match x returns (bool_or_int x) with
  | TB -> true
  | TI -> 0

Further, the return type need not be just a value type, it can also be a computation type, e.g., see examples here https://github.com/FStarLang/FStar/blob/master/tests/micro-benchmarks/Match.Returns.fst

So, in summary, the explicit dependent pattern syntax is a way to control how the types of the branches are refined, enabling proofs that rely more on normalization instead of provable equalities in Z3

A more detailed explanation is due in the book. Thanks for the question!