"-> ." in pattern matching

Learning
1

The OCaml grammar for patterns includes a case for -> . as the right hand side. I could not find it in the OCaml manual but it seems to be intended for unreachable patterns. Where is this documented and what is the idiomatic use case?

match_case:
    pattern MINUSGREATER seq_expr
      { Exp.case $1 $3 }
  | pattern WHEN seq_expr MINUSGREATER seq_expr
      { Exp.case $1 ~guard:$3 $5 }
  | pattern MINUSGREATER DOT
      { Exp.case $1 (Exp.unreachable ~loc:(make_loc $loc($3)) ()) }
;

Addendum: The reason I did not find it in the manual is that is a language extension that is described in the GADT section and doesn’t have an entry in the table of contents by itself.

2 Likes
2

Refutation cases are documented here .
Briefly, they are useful when fiddling with GADTs to express that a clause is impossible.
For instance if I have a heterogeneous list defined as

type empty = |
type 'a hlist = []: empty hlist | (::): 'a * 'b hlist -> ('a->'b) hlist

then if I have a list with type ('a -> 'b) hlist, I know that the list is non-empty.

let hd (type a b) : (a -> b) hlist -> a = function
  | a :: _ -> a
  | _ -> .

Here | _ -> . express the fact that the remaining case, [], is impossible and that the typechecker should be able to prove it.

However, in this case, the typechecker automatically adds a refutation clause _ -> . if there is only one clause in a pattern matching. Thus, I could have written the previous example as

let hd (type a b): (a -> b) hlist -> a = fun (a :: _) -> a

but handwritten refutation clause are necessary in more complex cases.

10 Likes